aboutsummaryrefslogtreecommitdiff
path: root/Category
diff options
context:
space:
mode:
Diffstat (limited to 'Category')
-rw-r--r--Category/BinaryBiproducts.agda166
1 files changed, 166 insertions, 0 deletions
diff --git a/Category/BinaryBiproducts.agda b/Category/BinaryBiproducts.agda
new file mode 100644
index 0000000..c96d3bf
--- /dev/null
+++ b/Category/BinaryBiproducts.agda
@@ -0,0 +1,166 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Level using (Level; levelOfTerm)
+open import Level using (_βŠ”_)
+
+module Category.BinaryBiproducts {o β„“ e : Level} (π’ž : Category o β„“ e) where
+
+import Categories.Morphism.Reasoning as β‡’-Reasoning
+
+open import Categories.Category.BinaryCoproducts π’ž using (BinaryCoproducts)
+open import Categories.Category.BinaryProducts π’ž using (BinaryProducts)
+open import Morphism.Zero using (IsZero⇒)
+open import Object.Biproduct π’ž using (Biproduct; Biproductβ‡’Product; Biproductβ‡’Coproduct)
+
+record BinaryBiproducts : Set (levelOfTerm π’ž) where
+
+ infixr 7 _βŠ•_
+
+ field
+ biproduct : βˆ€ {A B} β†’ Biproduct A B
+
+ open Category π’ž
+
+ private
+ module biproduct {A} {B} = Biproduct (biproduct {A} {B})
+
+ open biproduct using (Ο€β‚βˆ˜iβ‚β‰ˆid; Ο€β‚‚βˆ˜iβ‚‚β‰ˆid; permute; πŸŽβ‡’; πŸŽβ‡; Ο€β‚βˆ˜iβ‚‚-isZero; Ο€β‚‚βˆ˜i₁-isZero; ⟨⟩-unique; []-unique) public
+
+ _βŠ•_ : Obj β†’ Obj β†’ Obj
+ A βŠ• B = Biproduct.AβŠ•B (biproduct {A} {B})
+
+ module _ where
+ binaryProducts : BinaryProducts
+ binaryProducts = record { product = Biproduct⇒Product biproduct }
+ open BinaryProducts binaryProducts public
+ hiding (_Γ—_)
+ renaming (_×₁_ to infixr 10 _×₁_; Γ—-comm to βŠ•-comm; Γ—-assoc to βŠ•-assoc)
+
+ module _ where
+ binaryCoproducts : BinaryCoproducts
+ binaryCoproducts = record { coproduct = Biproduct⇒Coproduct biproduct }
+ open BinaryCoproducts binaryCoproducts public
+ hiding (_+_)
+ renaming (_+₁_ to infixr 10 _+₁_; +-comm to βŠ•-commβ€²; +-assoc to βŠ•-assocβ€²)
+
+ private
+ module Ο€β‚‚i₁ {A} {B} = IsZeroβ‡’ (Ο€β‚‚βˆ˜i₁-isZero {A} {B})
+ module π₁iβ‚‚ {A} {B} = IsZeroβ‡’ (Ο€β‚βˆ˜iβ‚‚-isZero {A} {B})
+
+ open β‡’-Reasoning π’ž
+ open HomReasoning
+
+ π₁iβ‚‚β‰ˆΟ€β‚‚i₁ : {A B : Obj} β†’ π₁ ∘ iβ‚‚ β‰ˆ Ο€β‚‚Β {A} {B} ∘ i₁
+ π₁iβ‚‚β‰ˆΟ€β‚‚i₁ {A} {B} = begin
+ π₁ ∘ iβ‚‚ β‰ˆβŸ¨ identityΚ³ ⟨
+ (π₁ ∘ iβ‚‚) ∘ id β‰ˆβŸ¨ π₁iβ‚‚.constant id ((π₁ ∘ iβ‚‚) ∘ (Ο€β‚‚ ∘ i₁)) ⟩
+ (π₁ ∘ iβ‚‚) ∘ ((π₁ ∘ iβ‚‚) ∘ (Ο€β‚‚ ∘ i₁)) β‰ˆβŸ¨ sym-assoc ⟩
+ ((π₁ ∘ iβ‚‚) ∘ (π₁ ∘ iβ‚‚)) ∘ (Ο€β‚‚ ∘ i₁) β‰ˆβŸ¨ Ο€β‚‚i₁.coconstant ((π₁ ∘ iβ‚‚) ∘ (π₁ ∘ iβ‚‚)) id ⟩
+ id ∘ Ο€β‚‚ ∘ i₁ β‰ˆβŸ¨ pullΛ‘ identityΛ‘ ⟩
+ Ο€β‚‚ ∘ i₁ ∎
+
+ module _ {A B C : Obj} where
+
+ π₁iβ‚‚-absorbΛ‘ : (f : A β‡’ C) β†’ f ∘ πŸŽβ‡ {A} {B} β‰ˆ πŸŽβ‡
+ π₁iβ‚‚-absorbΛ‘ f = begin
+ f ∘ πŸŽβ‡ β‰ˆβŸ¨ π₁iβ‚‚.coconstant f (πŸŽβ‡ ∘ πŸŽβ‡’) ⟩
+ (πŸŽβ‡ ∘ πŸŽβ‡’) ∘ πŸŽβ‡ β‰ˆβŸ¨ assoc ⟩
+ πŸŽβ‡ ∘ (πŸŽβ‡’ ∘ πŸŽβ‡) β‰ˆβŸ¨ π₁iβ‚‚.constant (πŸŽβ‡’ ∘ πŸŽβ‡) id ⟩
+ πŸŽβ‡ ∘ id β‰ˆβŸ¨ identityΚ³ ⟩
+ πŸŽβ‡ ∎
+
+ π₁iβ‚‚-absorbΚ³ : (f : C β‡’ B) β†’ πŸŽβ‡ {A} {B} ∘ f β‰ˆ πŸŽβ‡
+ π₁iβ‚‚-absorbΚ³ f = begin
+ πŸŽβ‡ ∘ f β‰ˆβŸ¨ π₁iβ‚‚.constant f (πŸŽβ‡’ ∘ πŸŽβ‡) ⟩
+ πŸŽβ‡ ∘ πŸŽβ‡’ ∘ πŸŽβ‡ β‰ˆβŸ¨ sym-assoc ⟩
+ (πŸŽβ‡ ∘ πŸŽβ‡’) ∘ πŸŽβ‡ β‰ˆβŸ¨ π₁iβ‚‚.coconstant (πŸŽβ‡ ∘ πŸŽβ‡’) id ⟩
+ id ∘ πŸŽβ‡ β‰ˆβŸ¨ identityΛ‘ ⟩
+ πŸŽβ‡ ∎
+
+ Ο€β‚‚i₁-absorbΛ‘ : (f : B β‡’ C) β†’ f ∘ πŸŽβ‡’ {A} {B} β‰ˆ πŸŽβ‡’
+ Ο€β‚‚i₁-absorbΛ‘ f = begin
+ f ∘ πŸŽβ‡’ β‰ˆβŸ¨ Ο€β‚‚i₁.coconstant f (πŸŽβ‡’ ∘ πŸŽβ‡) ⟩
+ (πŸŽβ‡’ ∘ πŸŽβ‡) ∘ πŸŽβ‡’ β‰ˆβŸ¨ assoc ⟩
+ πŸŽβ‡’ ∘ (πŸŽβ‡ ∘ πŸŽβ‡’) β‰ˆβŸ¨ Ο€β‚‚i₁.constant (πŸŽβ‡ ∘ πŸŽβ‡’) id ⟩
+ πŸŽβ‡’ ∘ id β‰ˆβŸ¨ identityΚ³ ⟩
+ πŸŽβ‡’ ∎
+
+ Ο€β‚‚i₁-absorbΚ³ : (f : C β‡’ A) β†’ πŸŽβ‡’ {A} {B} ∘ f β‰ˆ πŸŽβ‡’
+ Ο€β‚‚i₁-absorbΚ³ f = begin
+ πŸŽβ‡’ ∘ f β‰ˆβŸ¨ Ο€β‚‚i₁.constant f (πŸŽβ‡ ∘ πŸŽβ‡’) ⟩
+ πŸŽβ‡’ ∘ πŸŽβ‡ ∘ πŸŽβ‡’ β‰ˆβŸ¨ sym-assoc ⟩
+ (πŸŽβ‡’ ∘ πŸŽβ‡) ∘ πŸŽβ‡’ β‰ˆβŸ¨ Ο€β‚‚i₁.coconstant (πŸŽβ‡’ ∘ πŸŽβ‡) id ⟩
+ id ∘ πŸŽβ‡’ β‰ˆβŸ¨ identityΛ‘ ⟩
+ πŸŽβ‡’ ∎
+
+ module _ {A B : Obj} (f g : A β‡’ B) where
+
+ Ο€β‚βˆ˜+₁ : π₁ ∘ f +₁ g β‰ˆ f ∘ π₁
+ Ο€β‚βˆ˜+₁ = begin
+ π₁ ∘ [ i₁ ∘ f , iβ‚‚ ∘ g ] β‰ˆβŸ¨ ∘[] ⟩
+ [ π₁ ∘ i₁ ∘ f , π₁ ∘ iβ‚‚ ∘ g ] β‰ˆβŸ¨ []-congΛ‘ sym-assoc ⟩
+ [ π₁ ∘ i₁ ∘ f , (π₁ ∘ iβ‚‚) ∘ g ] β‰ˆβŸ¨ []-congβ‚‚ (cancelΛ‘ Ο€β‚βˆ˜iβ‚β‰ˆid) (π₁iβ‚‚-absorbΚ³ g) ⟩
+ [ f , π₁ ∘ iβ‚‚ ] β‰ˆβŸ¨ []-congβ‚‚ (insertΚ³ Ο€β‚βˆ˜iβ‚β‰ˆid) (Equiv.sym (π₁iβ‚‚-absorbΛ‘ f)) ⟩
+ [ (f ∘ π₁) ∘ i₁ , f ∘ π₁ ∘ iβ‚‚ ] β‰ˆβŸ¨ []-congΛ‘ sym-assoc ⟩
+ [ (f ∘ π₁) ∘ i₁ , (f ∘ π₁) ∘ iβ‚‚ ] β‰ˆβŸ¨ +-g-Ξ· ⟩
+ f ∘ π₁ ∎
+
+ Ο€β‚‚βˆ˜+₁ : Ο€β‚‚ ∘ f +₁ g β‰ˆ g ∘ Ο€β‚‚
+ Ο€β‚‚βˆ˜+₁ = begin
+ Ο€β‚‚ ∘ [ i₁ ∘ f , iβ‚‚ ∘ g ] β‰ˆβŸ¨ ∘[] ⟩
+ [ Ο€β‚‚ ∘ i₁ ∘ f , Ο€β‚‚ ∘ iβ‚‚ ∘ g ] β‰ˆβŸ¨ []-congΚ³ sym-assoc ⟩
+ [ (Ο€β‚‚ ∘ i₁) ∘ f , Ο€β‚‚ ∘ iβ‚‚ ∘ g ] β‰ˆβŸ¨ []-congβ‚‚ (Ο€β‚‚i₁-absorbΚ³ f) (cancelΛ‘ Ο€β‚‚βˆ˜iβ‚‚β‰ˆid) ⟩
+ [ Ο€β‚‚ ∘ i₁ , g ] β‰ˆβŸ¨ []-congβ‚‚ (Equiv.sym (Ο€β‚‚i₁-absorbΛ‘ g)) (insertΚ³ Ο€β‚‚βˆ˜iβ‚‚β‰ˆid) ⟩
+ [ g ∘ Ο€β‚‚ ∘ i₁ , (g ∘ Ο€β‚‚) ∘ iβ‚‚ ] β‰ˆβŸ¨ []-congΚ³ sym-assoc ⟩
+ [ (g ∘ Ο€β‚‚) ∘ i₁ , (g ∘ Ο€β‚‚) ∘ iβ‚‚ ] β‰ˆβŸ¨ +-g-Ξ· ⟩
+ g ∘ Ο€β‚‚ ∎
+
+ ×₁-+₁ : f ×₁ g β‰ˆ f +₁ g
+ ×₁-+₁ = ⟨⟩-unique Ο€β‚βˆ˜+₁ Ο€β‚‚βˆ˜+₁
+
+ βˆ‡-assoc : {A : Obj} β†’ βˆ‡ {A} ∘ βˆ‡ +₁ id β‰ˆ βˆ‡ ∘ id +₁ βˆ‡ ∘ +-assocΛ‘
+ βˆ‡-assoc = begin
+ βˆ‡ ∘ βˆ‡ +₁ id β‰ˆβŸ¨ βˆ‡βˆ˜+₁ ⟩
+ [ βˆ‡ , id ] β‰ˆβŸ¨ []∘+-assocΚ³ ⟨
+ [ id , βˆ‡ ] ∘ +-assocΛ‘ β‰ˆβŸ¨ pushΛ‘ (Equiv.sym βˆ‡βˆ˜+₁) ⟩
+ βˆ‡ ∘ id +₁ βˆ‡ ∘ +-assocΛ‘ ∎
+
+ Ξ”-assoc : {A : Obj} β†’ id ×₁ Ξ” ∘ Ξ” {A} β‰ˆ assocΛ‘ ∘ Ξ” ×₁ id ∘ Ξ”
+ Ξ”-assoc = begin
+ id ×₁ Ξ” ∘ Ξ” β‰ˆβŸ¨ Γ—β‚βˆ˜Ξ” ⟩
+ ⟨ id , Ξ” ⟩ β‰ˆβŸ¨ assocˑ∘⟨⟩ ⟨
+ assocΛ‘ ∘ ⟨ Ξ” , id ⟩ β‰ˆβŸ¨ refl⟩∘⟨ Γ—β‚βˆ˜Ξ” ⟨
+ assocΛ‘ ∘ Ξ” ×₁ id ∘ Ξ” ∎
+
+ module _ {A : Obj} where
+
+ βˆ‡-identityΛ‘ : βˆ‡ ∘ iβ‚‚ β‰ˆ id {A}
+ βˆ‡-identityΛ‘ = injectβ‚‚
+
+ βˆ‡-identityΚ³ : βˆ‡ ∘ i₁ β‰ˆ id {A}
+ βˆ‡-identityΚ³ = inject₁
+
+ Ξ”-identityΛ‘ : Ο€β‚‚ ∘ Ξ” β‰ˆ id {A}
+ Ξ”-identityΛ‘ = projectβ‚‚
+
+ Ξ”-identityΚ³ : π₁ ∘ Ξ” β‰ˆ id {A}
+ Ξ”-identityΚ³ = project₁
+
+ βˆ‡-comm : {A : Obj} β†’ βˆ‡ {A} ∘ +-swap β‰ˆ βˆ‡
+ βˆ‡-comm = []∘+-swap
+
+ Ξ”-comm : {A : Obj} β†’ swap ∘ Ξ” {A} β‰ˆ Ξ”
+ Ξ”-comm = swap∘⟨⟩
+
+ β‡’βˆ‡ : {A B : Obj} {f : A β‡’ B} β†’ f ∘ βˆ‡ β‰ˆ βˆ‡ ∘ f +₁ f
+ β‡’βˆ‡ {f = f} = begin
+ f ∘ βˆ‡ β‰ˆβŸ¨ βˆ˜βˆ‡ ⟩
+ [ f , f ] β‰ˆβŸ¨ βˆ‡βˆ˜+₁ ⟨
+ βˆ‡ ∘ f +₁ f ∎
+
+ β‡’Ξ” : {A B : Obj} {f : A β‡’ B} β†’ Ξ” ∘ f β‰ˆ f ×₁ f ∘ Ξ”
+ β‡’Ξ” {A} {B} {f} = begin
+ Ξ” ∘ f β‰ˆβŸ¨ Ξ”βˆ˜Β βŸ©
+ ⟨ f , f ⟩ β‰ˆβŸ¨ Γ—β‚βˆ˜Ξ” ⟨
+ f ×₁ f ∘ Ξ” ∎
generated by cgit v1.2.3 (git 2.39.1) at 2026-07-21 18:22:02 +0000