diff options
Diffstat (limited to 'Category')
| -rw-r--r-- | Category/BinaryBiproducts.agda | 16 | ||||
| -rw-r--r-- | Category/Semiadditive.agda | 19 |
2 files changed, 29 insertions, 6 deletions
diff --git a/Category/BinaryBiproducts.agda b/Category/BinaryBiproducts.agda index c975d18..81a23cf 100644 --- a/Category/BinaryBiproducts.agda +++ b/Category/BinaryBiproducts.agda @@ -31,13 +31,11 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where _⊕_ : Obj → Obj → Obj A ⊕ B = Biproduct.A⊕B (biproduct {A} {B}) - private - - binaryProducts : BinaryProducts - binaryProducts = record { product = Biproduct⇒Product biproduct } + binaryProducts : BinaryProducts + binaryProducts = record { product = Biproduct⇒Product biproduct } - binaryCoproducts : BinaryCoproducts - binaryCoproducts = record { coproduct = Biproduct⇒Coproduct biproduct } + binaryCoproducts : BinaryCoproducts + binaryCoproducts = record { coproduct = Biproduct⇒Coproduct biproduct } open BinaryProducts binaryProducts public hiding (_×_) @@ -276,6 +274,12 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where ∇ ∘ f +₁ f ≈⟨ refl⟩∘⟨ ×₁-+₁ f f ⟨ ∇ ∘ f ×₁ f ∎ + ∇∘×₁ : {A B C : Obj} {f : A ⇒ C} {g : B ⇒ C} → ∇ ∘ f ×₁ g ≈ [ f , g ] + ∇∘×₁ {f = f} {g} = begin + ∇ ∘ f ×₁ g ≈⟨ refl⟩∘⟨ ×₁-+₁ f g ⟩ + ∇ ∘ f +₁ g ≈⟨ ∇∘+₁ ⟩ + [ f , g ] ∎ + ×₁∘first : {A B C D E : Obj} {f : B ⇒ C} {g : D ⇒ E} {h : A ⇒ B} → (f ×₁ g) ∘ first h ≈ (f ∘ h) ×₁ g ×₁∘first = ×₁∘×₁ ○ ×₁-cong₂ Equiv.refl identityʳ 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 |