diff options
Diffstat (limited to 'Category/Semiadditive.agda')
| -rw-r--r-- | Category/Semiadditive.agda | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda index 05ce264..86b5585 100644 --- a/Category/Semiadditive.agda +++ b/Category/Semiadditive.agda @@ -13,6 +13,7 @@ open import Categories.Category.CMonoidEnriched using (CM-Category) open import Categories.Category.Cartesian 𝒞 using (Cartesian) open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) open import Categories.Category.Cocartesian 𝒞 using (Cocartesian) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) open import Categories.Object.Zero 𝒞 using (Zero) open import Category.BinaryBiproducts 𝒞 using (BinaryBiproducts) open import Data.Product using (_,_) @@ -176,6 +177,3 @@ record Semiadditive : Set (levelOfTerm 𝒞) where { initial = initial ; coproducts = binaryCoproducts } - - open CartesianMonoidal cartesian using (monoidal) public - open CartesianSymmetricMonoidal cartesian using (symmetric) public |