{-# OPTIONS --without-K --safe #-} open import Level using (Level; levelOfTerm) 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.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) open import Categories.Object.Zero π’ž using (Zero) open import Category.BinaryBiproducts π’ž using (BinaryBiproducts) open import Data.Product using (_,_) private module π’ž = Category π’ž variable A B C D : π’ž.Obj -- A semiadditive category has all finite biproducts record Semiadditive : Set (levelOfTerm π’ž) where field zero : Zero biproducts : BinaryBiproducts open Zero zero public open BinaryBiproducts biproducts public open π’ž infix 8 _+_ field 𝟎 : A β‡’ B 𝟎-resp-∘ : {h : A β‡’ B} {k : C β‡’ D} β†’ k ∘ 𝟎 ∘ h β‰ˆ 𝟎 _+_ : A β‡’ B β†’ A β‡’ B β†’ A β‡’ B +-resp-β‰ˆ : {x y u v : A β‡’ B} β†’ x β‰ˆ y β†’ u β‰ˆ v β†’ x + u β‰ˆ y + v +-resp-∘ : {f g : B β‡’ C} {h : A β‡’ B} {k : C β‡’ D} β†’ k ∘ (f + g) ∘ h β‰ˆ k ∘ f ∘ h + k ∘ g ∘ h +-identityΛ‘ : (f : A β‡’ B) β†’ 𝟎 + f β‰ˆ f +-identityΚ³ : (f : A β‡’ B) β†’ f + 𝟎 β‰ˆ f open HomReasoning open β‡’-Reasoning +-cong : {x y u v : A β‡’ B} β†’ x β‰ˆ y β†’ u β‰ˆ v β†’ x + u β‰ˆ y + v +-cong = +-resp-β‰ˆ +-resp-∘ˑ : {A B C : Obj} {f g : A β‡’ B} {k : B β‡’ C} β†’ k ∘ (f + g) β‰ˆ k ∘ f + k ∘ g +-resp-∘ˑ {f = f} {g} {h} = begin h ∘ (f + g) β‰ˆβŸ¨ refl⟩∘⟨ identityΚ³ ⟨ h ∘ (f + g) ∘ id β‰ˆβŸ¨ +-resp-∘ ⟩ h ∘ f ∘ id + h ∘ g ∘ id β‰ˆβŸ¨ +-resp-β‰ˆ (refl⟩∘⟨ identityΚ³) (refl⟩∘⟨ identityΚ³) ⟩ h ∘ f + h ∘ g ∎ 𝟎-resp-∘ˑ : {A B C : Obj} {f : B β‡’ C} β†’ f ∘ 𝟎 {A} {B} β‰ˆ 𝟎 𝟎-resp-∘ˑ {f = f} = begin f ∘ 𝟎 β‰ˆβŸ¨ refl⟩∘⟨ identityΚ³ ⟨ f ∘ 𝟎 ∘ id β‰ˆβŸ¨ 𝟎-resp-∘ ⟩ 𝟎 ∎ module _ {A B : Obj} where Ο€β‚βˆ˜iβ‚‚β‰ˆ0 : π₁ {A} {B} ∘ iβ‚‚ β‰ˆ zeroβ‡’ Ο€β‚βˆ˜iβ‚‚β‰ˆ0 = begin π₁ ∘ iβ‚‚ β‰ˆβŸ¨ π₁iβ‚‚-absorbΛ‘ zeroβ‡’ ⟨ zeroβ‡’ {A} ∘ π₁ ∘ iβ‚‚ β‰ˆβŸ¨ zero-∘ʳ (π₁ ∘ iβ‚‚) ⟩ zeroβ‡’ ∎ Ο€β‚‚βˆ˜iβ‚β‰ˆ0 : Ο€β‚‚ {A} {B} ∘ i₁ β‰ˆ zeroβ‡’ Ο€β‚‚βˆ˜iβ‚β‰ˆ0 = begin Ο€β‚‚ ∘ i₁ β‰ˆβŸ¨ Ο€β‚‚i₁-absorbΛ‘ zeroβ‡’ ⟨ zeroβ‡’ {A} ∘ Ο€β‚‚ ∘ i₁ β‰ˆβŸ¨ zero-∘ʳ (Ο€β‚‚ ∘ i₁) ⟩ zeroβ‡’ ∎ πŸŽβ‰ˆzeroβ‡’ : 𝟎 {A} {B} β‰ˆ zeroβ‡’ πŸŽβ‰ˆzeroβ‡’ = begin 𝟎 β‰ˆβŸ¨ 𝟎-resp-∘ˑ ⟨ zeroβ‡’ ∘ 𝟎 β‰ˆβŸ¨ zero-∘ʳ {A} {B} 𝟎 ⟩ zeroβ‡’ ∎ module _ {A B : Obj} where +-βˆ‡βˆ˜βŸ¨βŸ© : {f g : A β‡’ B} β†’ f + g β‰ˆ βˆ‡ ∘ ⟨ f , g ⟩ +-βˆ‡βˆ˜βŸ¨βŸ© {f} {g} = begin f + g β‰ˆβŸ¨ +-resp-β‰ˆ (insertΛ‘ inject₁) (insertΛ‘ injectβ‚‚) ⟩ βˆ‡ ∘ i₁ ∘ f + βˆ‡ ∘ iβ‚‚ ∘ g β‰ˆβŸ¨ +-resp-∘ˑ ⟨ βˆ‡ ∘ (i₁ ∘ f + iβ‚‚ ∘ g) β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-unique left right ⟨ βˆ‡ ∘ ⟨ f , g ⟩ ∎ where left : π₁ ∘ (i₁ ∘ f + iβ‚‚ ∘ g) β‰ˆ f left = begin π₁ ∘ (i₁ ∘ f + iβ‚‚ ∘ g) β‰ˆβŸ¨ +-resp-∘ˑ ⟩ π₁ ∘ i₁ ∘ f + π₁ ∘ iβ‚‚ ∘ g β‰ˆβŸ¨ +-resp-β‰ˆ (cancelΛ‘ Ο€β‚βˆ˜iβ‚β‰ˆid) (pullΛ‘ Ο€β‚βˆ˜iβ‚‚β‰ˆ0) ⟩ f + zeroβ‡’ ∘ g β‰ˆβŸ¨ +-resp-β‰ˆ Equiv.refl (zero-∘ʳ g) ⟩ f + zeroβ‡’ β‰ˆβŸ¨ +-resp-β‰ˆ Equiv.refl πŸŽβ‰ˆzeroβ‡’Β βŸ¨ f + 𝟎 β‰ˆβŸ¨ +-identityΚ³ f ⟩ f ∎ right : Ο€β‚‚ ∘ (i₁ ∘ f + iβ‚‚ ∘ g) β‰ˆ g right = begin Ο€β‚‚ ∘ (i₁ ∘ f + iβ‚‚ ∘ g) β‰ˆβŸ¨ +-resp-∘ˑ ⟩ Ο€β‚‚ ∘ i₁ ∘ f + Ο€β‚‚ ∘ iβ‚‚ ∘ g β‰ˆβŸ¨ +-resp-β‰ˆ (pullΛ‘ Ο€β‚‚βˆ˜iβ‚β‰ˆ0) (cancelΛ‘ Ο€β‚‚βˆ˜iβ‚‚β‰ˆid) ⟩ zeroβ‡’ ∘ f + g β‰ˆβŸ¨ +-resp-β‰ˆ (zero-∘ʳ f) Equiv.refl ⟩ zeroβ‡’ + g β‰ˆβŸ¨ +-resp-β‰ˆ πŸŽβ‰ˆzeroβ‡’ Equiv.refl ⟨ 𝟎 + g β‰ˆβŸ¨ +-identityΛ‘ g ⟩ g ∎ Ξ”-βŠ• : {X Y : Obj} β†’ Ξ” {X βŠ• Y} β‰ˆ σ₂₃ ∘ Ξ” ×₁ Ξ” Ξ”-βŠ• {X} {Y} = begin ⟨ id , id ⟩ β‰ˆβŸ¨ ⟨⟩-congβ‚‚ id×₁id id×₁id ⟨ ⟨ id ×₁ id , id ×₁ id ⟩ β‰ˆβŸ¨ ⟨⟩-congβ‚‚ (×₁-congβ‚‚ project₁ project₁) (×₁-congβ‚‚ projectβ‚‚ projectβ‚‚) ⟨ ⟨ (π₁ ∘ Ξ”) ×₁ (π₁ ∘ Ξ”) , (Ο€β‚‚ ∘ Ξ”) ×₁ (Ο€β‚‚ ∘ Ξ”) ⟩ β‰ˆβŸ¨ ⟨⟩-congβ‚‚ Γ—β‚βˆ˜Γ—β‚ Γ—β‚βˆ˜Γ—β‚ ⟨ ⟨ π₁ ×₁ π₁ ∘ Ξ” ×₁ Ξ” , Ο€β‚‚ ×₁ Ο€β‚‚ ∘ Ξ” ×₁ Ξ” ⟩ β‰ˆβŸ¨ ⟨⟩∘ ⟨ σ₂₃ ∘ Ξ” ×₁ Ξ” ∎ βˆ‡-βŠ• : {X Y : Obj} β†’ βˆ‡ {X βŠ• Y} β‰ˆ βˆ‡ ×₁ βˆ‡ ∘ σ₂₃ βˆ‡-βŠ• {X} {Y} = begin [ id , id ] β‰ˆβŸ¨ []-congβ‚‚ id×₁id id×₁id ⟨ [ id ×₁ id , id ×₁ id ] β‰ˆβŸ¨ []-congβ‚‚ (×₁-congβ‚‚ inject₁ inject₁) (×₁-congβ‚‚ injectβ‚‚ injectβ‚‚) ⟨ [ (βˆ‡ ∘ i₁) ×₁ (βˆ‡ ∘ i₁) , (βˆ‡ ∘ iβ‚‚) ×₁ (βˆ‡ ∘ iβ‚‚) ] β‰ˆβŸ¨ []-congβ‚‚ Γ—β‚βˆ˜Γ—β‚ Γ—β‚βˆ˜Γ—β‚ ⟨ [ βˆ‡ ×₁ βˆ‡ ∘ i₁ ×₁ i₁ , βˆ‡ ×₁ βˆ‡ ∘ iβ‚‚ ×₁ iβ‚‚ ] β‰ˆβŸ¨ ∘[] ⟨ βˆ‡ ×₁ βˆ‡ ∘ [ i₁ ×₁ i₁ , iβ‚‚ ×₁ iβ‚‚ ] β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-unique (∘[] β—‹ []-congβ‚‚ Ο€β‚βˆ˜Γ—β‚ Ο€β‚βˆ˜Γ—β‚) (∘[] β—‹ []-congβ‚‚ Ο€β‚‚βˆ˜Γ—β‚ Ο€β‚‚βˆ˜Γ—β‚) ⟨ βˆ‡ ×₁ βˆ‡ ∘ ⟨ π₁ +₁ π₁ , Ο€β‚‚ +₁ Ο€β‚‚ ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ (×₁-+₁ π₁ π₁) (×₁-+₁ Ο€β‚‚ Ο€β‚‚) ⟨ βˆ‡ ×₁ βˆ‡ ∘ σ₂₃ ∎ module _ {A B : Obj} where +-assoc : (x y z : A β‡’ B) β†’ (x + y) + z β‰ˆ x + (y + z) +-assoc x y z = begin (x + y) + z β‰ˆβŸ¨ +-βˆ‡βˆ˜βŸ¨βŸ© ⟩ βˆ‡ ∘ ⟨ x + y , z ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congΚ³ +-βˆ‡βˆ˜βŸ¨βŸ© ⟩ βˆ‡ ∘ ⟨ βˆ‡ ∘ ⟨ x , y ⟩ , z ⟩ β‰ˆβŸ¨ refl⟩∘⟨ first∘⟨⟩ ⟨ βˆ‡ ∘ βˆ‡ ×₁ id ∘ ⟨ ⟨ x , y ⟩ , z ⟩ β‰ˆβŸ¨ extendΚ³ βˆ‡-assoc-×₁ ⟩ βˆ‡ ∘ (id ×₁ βˆ‡ ∘ assocΛ‘) ∘ ⟨ ⟨ x , y ⟩ , z ⟩ β‰ˆβŸ¨ refl⟩∘⟨ pullΚ³ assocˑ∘⟨⟩ ⟩ βˆ‡ ∘ id ×₁ βˆ‡ ∘ ⟨ x , ⟨ y , z ⟩ ⟩ β‰ˆβŸ¨ refl⟩∘⟨ second∘⟨⟩ ⟩ βˆ‡ ∘ ⟨ x , βˆ‡ ∘ ⟨ y , z ⟩ ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congΛ‘ +-βˆ‡βˆ˜βŸ¨βŸ© ⟨ βˆ‡ ∘ ⟨ x , y + z ⟩ β‰ˆβŸ¨ +-βˆ‡βˆ˜βŸ¨βŸ© ⟨ x + (y + z) ∎ βˆ‡βˆ˜+-swap : {A : Obj} β†’ βˆ‡ ∘ +-swap {A} β‰ˆ βˆ‡ βˆ‡βˆ˜+-swap = begin βˆ‡ ∘ [ iβ‚‚ , i₁ ] β‰ˆβŸ¨ ∘[] ⟩ [ βˆ‡ ∘ iβ‚‚ , βˆ‡ ∘ i₁ ] β‰ˆβŸ¨ []-congβ‚‚ injectβ‚‚ inject₁ ⟩ [ id , id ] ∎ swapβˆ˜Ξ” : {A : Obj} β†’ swap {A} ∘ Ξ” β‰ˆ Ξ” swapβˆ˜Ξ” = begin ⟨ Ο€β‚‚ , π₁ ⟩ ∘ Ξ” β‰ˆβŸ¨ ⟨⟩∘ ⟩ ⟨ Ο€β‚‚ ∘ Ξ” , π₁ ∘ Ξ” ⟩ β‰ˆβŸ¨ ⟨⟩-congβ‚‚ projectβ‚‚ project₁ ⟩ ⟨ id , id ⟩ ∎ +-comm : (x y : A β‡’ B) β†’ x + y β‰ˆ y + x +-comm x y = begin x + y β‰ˆβŸ¨ +-βˆ‡βˆ˜βŸ¨βŸ© ⟩ βˆ‡ ∘ ⟨ x , y ⟩ β‰ˆβŸ¨ refl⟩∘⟨ swap∘⟨⟩ ⟨ βˆ‡ ∘ swap ∘ ⟨ y , x ⟩ β‰ˆβŸ¨ refl⟩∘⟨ swapβ‰ˆ+-swap ⟩∘⟨refl ⟩ βˆ‡ ∘ +-swap ∘ ⟨ y , x ⟩ β‰ˆβŸ¨ pullΛ‘ βˆ‡βˆ˜+-swap ⟩ βˆ‡ ∘ ⟨ y , x ⟩ β‰ˆβŸ¨ +-βˆ‡βˆ˜βŸ¨βŸ© ⟨ y + x ∎ isCM : IsCommutativeMonoid (_β‰ˆ_ {A} {B}) _+_ 𝟎 isCM = record { isMonoid = record { isSemigroup = record { isMagma = record { isEquivalence = equiv ; βˆ™-cong = +-resp-β‰ˆ } ; assoc = +-assoc } ; identity = +-identityΛ‘ , +-identityΚ³ } ; comm = +-comm } hom : Obj β†’ Obj β†’ CommutativeMonoid β„“ e hom A B = record { Carrier = A β‡’ B ; _β‰ˆ_ = _β‰ˆ_ ; _βˆ™_ = _+_ ; Ξ΅ = 𝟎 ; isCommutativeMonoid = isCM } cm-category : CM-Category o β„“ e cm-category = record { π’ž ; Hom = hom ; +-resp-∘ = +-resp-∘ ; 0-resp-∘ = 𝟎-resp-∘ } cartesian : Cartesian cartesian = record { terminal = terminal ; products = binaryProducts } cocartesian : Cocartesian cocartesian = record { initial = initial ; coproducts = binaryCoproducts } record SemiadditiveHelper : Set (levelOfTerm π’ž) where field zero : Zero biproducts : BinaryBiproducts open Zero zero open BinaryBiproducts biproducts open π’ž open HomReasoning open β‡’-Reasoning module _ {A B : Obj} where Ο€β‚βˆ˜iβ‚‚β‰ˆ0 : π₁ {A} {B} ∘ iβ‚‚ β‰ˆ zeroβ‡’ Ο€β‚βˆ˜iβ‚‚β‰ˆ0 = begin π₁ ∘ iβ‚‚ β‰ˆβŸ¨ π₁iβ‚‚-absorbΛ‘ zeroβ‡’ ⟨ zeroβ‡’ {A} ∘ π₁ ∘ iβ‚‚ β‰ˆβŸ¨ zero-∘ʳ (π₁ ∘ iβ‚‚) ⟩ zeroβ‡’ ∎ Ο€β‚‚βˆ˜iβ‚β‰ˆ0 : Ο€β‚‚ {A} {B} ∘ i₁ β‰ˆ zeroβ‡’ Ο€β‚‚βˆ˜iβ‚β‰ˆ0 = begin Ο€β‚‚ ∘ i₁ β‰ˆβŸ¨ Ο€β‚‚i₁-absorbΛ‘ zeroβ‡’ ⟨ zeroβ‡’ {A} ∘ Ο€β‚‚ ∘ i₁ β‰ˆβŸ¨ zero-∘ʳ (Ο€β‚‚ ∘ i₁) ⟩ zeroβ‡’ ∎ -- Construct hom-set addition from biproduct semiadditveHelper : SemiadditiveHelper β†’ Semiadditive semiadditveHelper sh = record { zero = zero ; biproducts = biproducts ; 𝟎 = zeroβ‡’ ; 𝟎-resp-∘ = 𝟎-resp-∘ ; _+_ = _+_ ; +-resp-β‰ˆ = +-cong ; +-resp-∘ = +-resp-∘ ; +-identityΛ‘ = +-identityΛ‘ ; +-identityΚ³ = +-identityΚ³ } where open SemiadditiveHelper sh open Zero zero open BinaryBiproducts biproducts open π’ž open HomReasoning open β‡’-Reasoning 𝟎-resp-∘ : {A B C D : Obj} {h : A β‡’ B} {k : C β‡’ D} β†’ k ∘ zeroβ‡’ ∘ h β‰ˆ zeroβ‡’ 𝟎-resp-∘ {h = h} {k} = begin k ∘ zeroβ‡’ ∘ h β‰ˆβŸ¨ pullΛ‘ (zero-∘ˑ k) ⟩ zeroβ‡’ ∘ h β‰ˆβŸ¨ zero-∘ʳ h ⟩ zeroβ‡’ ∎ infix 8 _+_ _+_ : A β‡’ B β†’ A β‡’ B β†’ A β‡’ B f + g = βˆ‡ ∘ ⟨ f , g ⟩ +-cong : {x y u v : A β‡’ B} β†’ x β‰ˆ y β†’ u β‰ˆ v β†’ x + u β‰ˆ y + v +-cong eq₁ eqβ‚‚ = refl⟩∘⟨ ⟨⟩-congβ‚‚ eq₁ eqβ‚‚ +-resp-∘ : {A B C D : Obj} {f g : B β‡’ C} {h : A β‡’ B} {k : C β‡’ D} β†’ k ∘ (f + g) ∘ h β‰ˆ k ∘ f ∘ h + k ∘ g ∘ h +-resp-∘ {f = f} {g} {h} {k} = begin k ∘ (βˆ‡ ∘ ⟨ f , g ⟩) ∘ h β‰ˆβŸ¨ refl⟩∘⟨ pullΚ³ ⟨⟩∘ ⟩ k ∘ βˆ‡ ∘ ⟨ f ∘ h , g ∘ h ⟩ β‰ˆβŸ¨ extendΚ³ β‡’βˆ‡-×₁ ⟩ βˆ‡ ∘ k ×₁ k ∘ ⟨ f ∘ h , g ∘ h ⟩ β‰ˆβŸ¨ refl⟩∘⟨ Γ—β‚βˆ˜βŸ¨βŸ© ⟩ βˆ‡ ∘ ⟨ k ∘ f ∘ h , k ∘ g ∘ h ⟩ ∎ +-identityΛ‘ : (x : A β‡’ B) β†’ zeroβ‡’ + x β‰ˆ x +-identityΛ‘ x = begin βˆ‡ ∘ ⟨ zeroβ‡’ , x ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ (zero-∘ʳ x) identityΛ‘ ⟨ βˆ‡ ∘ ⟨ zeroβ‡’ ∘ x , id ∘ x ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩∘ ⟨ βˆ‡ ∘ ⟨ zeroβ‡’ , id ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ Ο€β‚βˆ˜iβ‚‚β‰ˆ0 Ο€β‚‚βˆ˜iβ‚‚β‰ˆid ⟩∘⟨refl ⟨ βˆ‡ ∘ ⟨ π₁ ∘ iβ‚‚ , Ο€β‚‚ ∘ iβ‚‚ ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ g-Ξ· ⟩∘⟨refl ⟩ βˆ‡ ∘ iβ‚‚ ∘ x β‰ˆβŸ¨ cancelΛ‘ βˆ‡-identityΛ‘ ⟩ x ∎ +-identityΚ³ : (x : A β‡’ B) β†’ x + zeroβ‡’ β‰ˆ x +-identityΚ³ x = begin βˆ‡ ∘ ⟨ x , zeroβ‡’ ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ identityΛ‘ (zero-∘ʳ x) ⟨ βˆ‡ ∘ ⟨ id ∘ x , zeroβ‡’ ∘ x ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩∘ ⟨ βˆ‡ ∘ ⟨ id , zeroβ‡’ ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ Ο€β‚βˆ˜iβ‚β‰ˆid Ο€β‚‚βˆ˜iβ‚β‰ˆ0 ⟩∘⟨refl ⟨ βˆ‡ ∘ ⟨ π₁ ∘ i₁ , Ο€β‚‚ ∘ i₁ ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ g-Ξ· ⟩∘⟨refl ⟩ βˆ‡ ∘ i₁ ∘ x β‰ˆβŸ¨ cancelΛ‘ βˆ‡-identityΚ³ ⟩ x ∎