From 7093fb4fa137b63ae7f2b8a00269ef63da9d70ee Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 17 Jul 2026 17:16:37 -0700 Subject: Add categories with all binary biproducts --- Category/BinaryBiproducts.agda | 166 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 166 insertions(+) create mode 100644 Category/BinaryBiproducts.agda (limited to 'Category') 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 ∘ Ξ” ∎ -- cgit v1.2.3