diff options
Diffstat (limited to 'Category/Semiadditive.agda')
| -rw-r--r-- | Category/Semiadditive.agda | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda index 9bbc9c7..05ce264 100644 --- a/Category/Semiadditive.agda +++ b/Category/Semiadditive.agda @@ -6,9 +6,13 @@ open import Categories.Category using (Category) module Category.Semiadditive {o ℓ e : Level} (𝒞 : Category o ℓ e) where import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning +import Categories.Category.Cartesian.SymmetricMonoidal 𝒞 as CartesianSymmetricMonoidal open import Algebra using (IsCommutativeMonoid; CommutativeMonoid) 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.Object.Zero 𝒞 using (Zero) open import Category.BinaryBiproducts 𝒞 using (BinaryBiproducts) open import Data.Product using (_,_) @@ -160,3 +164,18 @@ record Semiadditive : Set (levelOfTerm 𝒞) where ; +-resp-∘ = +-resp-∘ ; 0-resp-∘ = 0-resp-∘ } + + cartesian : Cartesian + cartesian = record + { terminal = terminal + ; products = binaryProducts + } + + cocartesian : Cocartesian + cocartesian = record + { initial = initial + ; coproducts = binaryCoproducts + } + + open CartesianMonoidal cartesian using (monoidal) public + open CartesianSymmetricMonoidal cartesian using (symmetric) public |