From ae16aea8b4b9c3a3ae601951d6bed9caaeea1677 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sun, 30 Jul 2023 17:47:06 +0200 Subject: [PATCH] Added distributive and extensive category definitions, added coproduct definitions --- Coproduct.agda | 47 +++++++++++++++++++ Distributive/Bundle.agda | 4 +- Distributive/Core.agda | 47 +++++++++++++++---- ElgotAlgebra.agda | 7 +-- ElgotAlgebras.agda | 59 ++++++++++++------------ Extensive/Bundle.agda | 31 +++++++++++++ Extensive/Core.agda | 99 ++++++++++++++++++++++++++++++++++++++++ bsc.agda-lib | 2 +- 8 files changed, 252 insertions(+), 44 deletions(-) create mode 100644 Coproduct.agda create mode 100644 Extensive/Bundle.agda create mode 100644 Extensive/Core.agda diff --git a/Coproduct.agda b/Coproduct.agda new file mode 100644 index 0000000..e5fe3e5 --- /dev/null +++ b/Coproduct.agda @@ -0,0 +1,47 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category hiding (_[_,_]) +open import Level +open import Function using (_$_) + +module Coproduct {o ℓ e} (𝒞 : Category o ℓ e) where + +open Category 𝒞 + +open import Categories.Morphism.Reasoning 𝒞 +open import Categories.Morphism 𝒞 + +open HomReasoning +open import Categories.Object.Coproduct + +private + variable + A B C D : Obj + f g h : A ⇒ B + +module _ {A B : Obj} where + open Coproduct {𝒞 = 𝒞} {A = A} {B = B} renaming ([_,_] to _[_,_]) + + repack : (p₁ p₂ : Coproduct 𝒞 A B) → A+B p₁ ⇒ A+B p₂ + repack p₁ p₂ = p₁ [ i₁ p₂ , i₂ p₂ ] + + repack∘ : (p₁ p₂ p₃ : Coproduct 𝒞 A B) → repack p₂ p₃ ∘ repack p₁ p₂ ≈ repack p₁ p₃ + repack∘ p₁ p₂ p₃ = ⟺ $ unique p₁ + (glueTrianglesˡ (inject₁ p₂) (inject₁ p₁)) + (glueTrianglesˡ (inject₂ p₂) (inject₂ p₁)) + + repack≡id : (p : Coproduct 𝒞 A B) → repack p p ≈ id + repack≡id = η + + repack-cancel : (p₁ p₂ : Coproduct 𝒞 A B) → repack p₁ p₂ ∘ repack p₂ p₁ ≈ id + repack-cancel p₁ p₂ = repack∘ p₂ p₁ p₂ ○ repack≡id p₂ + +up-to-iso : ∀ (p₁ p₂ : Coproduct 𝒞 A B) → Coproduct.A+B p₁ ≅ Coproduct.A+B p₂ +up-to-iso p₁ p₂ = record + { from = repack p₁ p₂ + ; to = repack p₂ p₁ + ; iso = record + { isoˡ = repack-cancel p₂ p₁ + ; isoʳ = repack-cancel p₁ p₂ + } + } \ No newline at end of file diff --git a/Distributive/Bundle.agda b/Distributive/Bundle.agda index 5ed63e9..7521fd4 100644 --- a/Distributive/Bundle.agda +++ b/Distributive/Bundle.agda @@ -14,7 +14,9 @@ open import Level record DistributiveCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where field U : Category o ℓ e - distributive : Distributive U + cartesian : Cartesian U + cocartesian : Cocartesian U + distributive : Distributive U cartesian cocartesian open Category U public open Distributive distributive public \ No newline at end of file diff --git a/Distributive/Core.agda b/Distributive/Core.agda index 6675e9c..0deac8d 100644 --- a/Distributive/Core.agda +++ b/Distributive/Core.agda @@ -5,6 +5,7 @@ open import Categories.Category.Cartesian open import Categories.Category.BinaryProducts open import Categories.Category.Cocartesian import Categories.Morphism as M +import Categories.Morphism.Reasoning as MR module Distributive.Core {o ℓ e} (𝒞 : Category o ℓ e) where @@ -12,17 +13,45 @@ open import Level open Category 𝒞 open M 𝒞 -record Distributive : Set (levelOfTerm 𝒞) where - field - cartesian : Cartesian 𝒞 - cocartesian : Cocartesian 𝒞 - +private + variable + A B C : Obj + +record Distributive (cartesian : Cartesian 𝒞) (cocartesian : Cocartesian 𝒞) : Set (levelOfTerm 𝒞) where open Cartesian cartesian open BinaryProducts products open Cocartesian cocartesian - distribute : ∀ {A B C} → (A × B + A × C) ⇒ (A × (B + C)) - distribute = [ id ⁂ i₁ , id ⁂ i₂ ] - field - iso : ∀ {A B C} → IsIso (distribute {A} {B} {C}) + distributeˡ : (A × B + A × C) ≅ (A × (B + C)) + + distributeʳ : ∀ {A B C : Obj} → (B × A + C × A) ≅ (B + C) × A + distributeʳ {A} {B} {C} = record + { from = (swap ∘ from) ∘ (swap +₁ swap) + ; to = ((swap +₁ swap) ∘ to) ∘ swap + ; iso = record + { isoˡ = begin + (((swap +₁ swap) ∘ to) ∘ swap) ∘ (swap ∘ from) ∘ (swap +₁ swap) ≈⟨ pullˡ (pullˡ (pullʳ swap∘swap)) ⟩ + ((((swap +₁ swap) ∘ to) ∘ id) ∘ from) ∘ (swap +₁ swap) ≈⟨ identityʳ ⟩∘⟨refl ⟩∘⟨refl ⟩ + (((swap +₁ swap) ∘ to) ∘ from) ∘ (swap +₁ swap) ≈⟨ pullʳ isoˡ ⟩∘⟨refl ⟩ + ((swap +₁ swap) ∘ id) ∘ (swap +₁ swap) ≈⟨ identityʳ ⟩∘⟨refl ⟩ + (swap +₁ swap) ∘ (swap +₁ swap) ≈⟨ +₁∘+₁ ⟩ + ((swap ∘ swap) +₁ (swap ∘ swap)) ≈⟨ +₁-cong₂ swap∘swap swap∘swap ⟩ + (id +₁ id) ≈⟨ +-unique id-comm-sym id-comm-sym ⟩ + id ∎ + ; isoʳ = begin + ((swap ∘ from) ∘ (swap +₁ swap)) ∘ ((swap +₁ swap) ∘ to) ∘ swap ≈⟨ pullˡ (pullˡ (pullʳ +₁∘+₁)) ⟩ + (((swap ∘ from) ∘ ((swap ∘ swap) +₁ (swap ∘ swap))) ∘ to) ∘ swap ≈⟨ (((refl⟩∘⟨ +₁-cong₂ swap∘swap swap∘swap) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ + (((swap ∘ from) ∘ (id +₁ id)) ∘ to) ∘ swap ≈⟨ (((refl⟩∘⟨ +-unique id-comm-sym id-comm-sym) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ + (((swap ∘ from) ∘ id) ∘ to) ∘ swap ≈⟨ ((identityʳ ⟩∘⟨refl) ⟩∘⟨refl) ⟩ + ((swap ∘ from) ∘ to) ∘ swap ≈⟨ (pullʳ isoʳ ⟩∘⟨refl) ⟩ + (swap ∘ id) ∘ swap ≈⟨ (identityʳ ⟩∘⟨refl) ⟩ + swap ∘ swap ≈⟨ swap∘swap ⟩ + id ∎ + } + } + where + open _≅_ (distributeˡ {A} {B} {C}) + open HomReasoning + open Equiv + open MR 𝒞 diff --git a/ElgotAlgebra.agda b/ElgotAlgebra.agda index b133b48..a2b2d8a 100644 --- a/ElgotAlgebra.agda +++ b/ElgotAlgebra.agda @@ -8,19 +8,20 @@ open import Categories.Functor.Algebra open import Categories.Object.Product open import Categories.Object.Coproduct open import Categories.Category -open import Distributive.Bundle open import Distributive.Core open import Categories.Category.Cartesian open import Categories.Category.BinaryProducts open import Categories.Category.Cocartesian +open import Extensive.Bundle +open import Extensive.Core private variable o ℓ e : Level -module _ (D : DistributiveCategory o ℓ e) where - open DistributiveCategory D renaming (U to C; id to idC) +module _ (D : ExtensiveDistributiveCategory o ℓ e) where + open ExtensiveDistributiveCategory D renaming (U to C; id to idC) open Cocartesian cocartesian open Cartesian cartesian diff --git a/ElgotAlgebras.agda b/ElgotAlgebras.agda index d47712e..50b1c2b 100644 --- a/ElgotAlgebras.agda +++ b/ElgotAlgebras.agda @@ -16,6 +16,9 @@ open import Categories.Category open import ElgotAlgebra open import Distributive.Bundle open import Distributive.Core +open import Extensive.Bundle +open import Extensive.Core +open import Categories.Morphism module ElgotAlgebras where @@ -23,15 +26,11 @@ private variable o ℓ e : Level -module _ (D : DistributiveCategory o ℓ e) where - open DistributiveCategory D renaming (U to C; id to idC) +module _ (D : ExtensiveDistributiveCategory o ℓ e) where + open ExtensiveDistributiveCategory D renaming (U to C; id to idC) open Cocartesian cocartesian - - CC : CocartesianCategory o ℓ e - CC = record - { U = C - ; cocartesian = cocartesian - } + open Cartesian cartesian + open BinaryProducts products --* -- let's define the category of elgot-algebras @@ -116,15 +115,15 @@ module _ (D : DistributiveCategory o ℓ e) where open Equiv -- if the carriers of the algebra form a product, so do the algebras - A×B-Helper : ∀ {EA EB : Elgot-Algebra D} → Product C (Elgot-Algebra.A EA) (Elgot-Algebra.A EB) → Elgot-Algebra D - A×B-Helper {EA} {EB} p = record - { A = A×B + A×B-Helper : ∀ {EA EB : Elgot-Algebra D} → Elgot-Algebra D + A×B-Helper {EA} {EB} = record + { A = A × B ; _# = λ {X : Obj} (h : X ⇒ A×B + X) → ⟨ ((π₁ +₁ idC) ∘ h)#ᵃ , ((π₂ +₁ idC) ∘ h)#ᵇ ⟩ ; #-Fixpoint = λ {X} {f} → begin ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩ ⟨ [ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ ((π₁ +₁ idC) ∘ f) , [ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ ((π₂ +₁ idC) ∘ f) ⟩ ≈⟨ ⟨⟩-cong₂ sym-assoc sym-assoc ⟩ ⟨ ([ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ (π₁ +₁ idC)) ∘ f , ([ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ (π₂ +₁ idC)) ∘ f ⟩ ≈⟨ ⟨⟩-cong₂ (∘-resp-≈ˡ []∘+₁) (∘-resp-≈ˡ []∘+₁) ⟩ - ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩ ≈⟨ sym ∘-distribʳ-⟨⟩ ⟩ + ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩ ≈⟨ sym ⟨⟩∘ ⟩ (⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f) ≈⟨ ∘-resp-≈ˡ (unique′ (begin π₁ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₁ ⟩ @@ -183,8 +182,8 @@ module _ (D : DistributiveCategory o ℓ e) where where open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈) open Elgot-Algebra EB using () renaming (A to B; _# to _#ᵇ; #-Fixpoint to #ᵇ-Fixpoint; #-Uniformity to #ᵇ-Uniformity; #-Folding to #ᵇ-Folding; #-resp-≈ to #ᵇ-resp-≈) - open Product C p open HomReasoning + -- open Product (product {A} {B}) open Equiv foldingˡ : ∀ {X} {Y} {f} {h} → (((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ) ≈ ((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ foldingˡ {X} {Y} {f} {h} = begin @@ -213,9 +212,9 @@ module _ (D : DistributiveCategory o ℓ e) where (([ (π₂ +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π₂ +₁ idC) ∘ i₂ ∘ h ])#ᵇ) ≈⟨ sym (#ᵇ-resp-≈ ∘[]) ⟩ ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ ∎ - Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra D) → Product C (Elgot-Algebra.A EA) (Elgot-Algebra.A EB) → Product Elgot-Algebras EA EB - Product-Elgot-Algebras EA EB p = record - { A×B = A×B-Helper {EA} {EB} p + Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra D) → Product Elgot-Algebras EA EB + Product-Elgot-Algebras EA EB = record + { A×B = A×B-Helper {EA} {EB} ; π₁ = record { h = π₁ ; preserves = λ {X} {f} → project₁ } ; π₂ = record { h = π₂ ; preserves = λ {X} {f} → project₂ } ; ⟨_,_⟩ = λ {E} f g → let @@ -223,7 +222,7 @@ module _ (D : DistributiveCategory o ℓ e) where open Elgot-Algebra-Morphism g renaming (h to g′; preserves to preservesᵍ) open Elgot-Algebra E renaming (_# to _#ᵉ) in record { h = ⟨ f′ , g′ ⟩ ; preserves = λ {X} {h} → begin - ⟨ f′ , g′ ⟩ ∘ (h #ᵉ) ≈⟨ ∘-distribʳ-⟨⟩ ⟩ + ⟨ f′ , g′ ⟩ ∘ (h #ᵉ) ≈⟨ ⟨⟩∘ ⟩ ⟨ f′ ∘ (h #ᵉ) , g′ ∘ (h #ᵉ) ⟩ ≈⟨ ⟨⟩-cong₂ preservesᶠ preservesᵍ ⟩ ⟨ ((f′ +₁ idC) ∘ h) #ᵃ , ((g′ +₁ idC) ∘ h) #ᵇ ⟩ ≈⟨ sym (⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₁ identity²))) (#ᵇ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₂ identity²)))) ⟩ ⟨ ((π₁ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵃ , ((π₂ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵇ ⟩ ≈⟨ sym (⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ +₁∘+₁)) (#ᵇ-resp-≈ (∘-resp-≈ˡ +₁∘+₁))) ⟩ @@ -236,32 +235,32 @@ module _ (D : DistributiveCategory o ℓ e) where where open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈) open Elgot-Algebra EB using () renaming (A to B; _# to _#ᵇ; #-Fixpoint to #ᵇ-Fixpoint; #-Uniformity to #ᵇ-Uniformity; #-Folding to #ᵇ-Folding; #-resp-≈ to #ᵇ-resp-≈) - open Elgot-Algebra (A×B-Helper {EA} {EB} p) using () renaming (_# to _#ᵖ) - open Product C p + open Elgot-Algebra (A×B-Helper {EA} {EB}) using () renaming (_# to _#ᵖ) open HomReasoning open Equiv -- if the carrier is cartesian, so is the category of algebras - Cartesian-Elgot-Algebras : Cartesian C → Cartesian Elgot-Algebras - Cartesian-Elgot-Algebras CaC = record { + Cartesian-Elgot-Algebras : Cartesian Elgot-Algebras + Cartesian-Elgot-Algebras = record { terminal = Terminal-Elgot-Algebras terminal; - products = record { product = λ {EA EB} → Product-Elgot-Algebras EA EB product } + products = record { product = λ {EA EB} → Product-Elgot-Algebras EA EB } } where - open Cartesian CaC using (terminal; products) - open BinaryProducts products using (product) open Equiv -- if the carriers of the algebra form a exponential, so do the algebras - B^A-Helper : ∀ {EA EB : Elgot-Algebra D} → Exponential C (Elgot-Algebra.A EA) (Elgot-Algebra.A EB) → Elgot-Algebra D - B^A-Helper {EA} {EB} e = record - { A = B^A - ; _# = λ {X} f → λg {! !} {! !} - ; #-Fixpoint = {! !} + B^A-Helper : ∀ {EA : Elgot-Algebra D} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra D + B^A-Helper {EA} {X} exp = record + { A = A^X + ; _# = λ {Z} f → λg product (((((eval +₁ idC) ∘ (Categories.Object.Product.repack C product product' +₁ idC)) ∘ dstl) ∘ (f ⁂ idC)) #ᵃ) + ; #-Fixpoint = λ {X} {f} → {! !} ; #-Uniformity = {! !} ; #-Folding = {! !} ; #-resp-≈ = {! !} } where - open Exponential e \ No newline at end of file + open Exponential exp renaming (B^A to A^X; product to product') + open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈) + dstr = λ {X Y Z} → _≅_.to (distributeˡ {X} {Y} {Z}) + dstl = λ {X Y Z} → _≅_.to (distributeʳ {X} {Y} {Z}) \ No newline at end of file diff --git a/Extensive/Bundle.agda b/Extensive/Bundle.agda new file mode 100644 index 0000000..e6ec336 --- /dev/null +++ b/Extensive/Bundle.agda @@ -0,0 +1,31 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category +open import Categories.Category.Cartesian +open import Categories.Category.BinaryProducts +open import Categories.Category.Cocartesian +open import Distributive.Core +open import Extensive.Core +import Categories.Morphism as M + +module Extensive.Bundle where + +open import Level + +record ExtensiveCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where + field + U : Category o ℓ e + extensive : Extensive U + + open Category U public + open Extensive extensive public + +record ExtensiveDistributiveCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where + field + U : Category o ℓ e + cartesian : Cartesian U + extensive : Extensive U + + open Category U public + open Extensive extensive public + open Distributive (Extensive⇒Distributive cartesian extensive) public diff --git a/Extensive/Core.agda b/Extensive/Core.agda new file mode 100644 index 0000000..df0d83e --- /dev/null +++ b/Extensive/Core.agda @@ -0,0 +1,99 @@ +{-# OPTIONS --without-K --safe #-} + +module Extensive.Core where + +-- https://ncatlab.org/nlab/show/extensive+category + +open import Level + +open import Categories.Category.Core +open import Distributive.Core +open import Categories.Diagram.Pullback +open import Categories.Category.Cocartesian +open import Categories.Category.Cartesian +open import Categories.Category.BinaryProducts +open import Categories.Object.Coproduct +open import Categories.Morphism +open import Function using (_$_) +open import Coproduct + + +private + variable + o ℓ e : Level + +record Extensive (𝒞 : Category o ℓ e) : Set (suc (o ⊔ ℓ ⊔ e)) where + open Category 𝒞 + open Pullback + + field + cocartesian : Cocartesian 𝒞 + + module CC = Cocartesian cocartesian + open CC using (_+_; i₁; i₂; ¡) + + field + -- top-row is coproduct ⇒ pullback + cp⇒pullback₁ : {A B C D : Obj} (cp : Coproduct 𝒞 A B) (p₂ : A ⇒ C) (f : Coproduct.A+B cp ⇒ C + D) → IsPullback 𝒞 (Coproduct.i₁ cp) p₂ f i₁ + cp⇒pullback₂ : {A B C D : Obj} (cp : Coproduct 𝒞 A B) (p₂ : B ⇒ D) (f : Coproduct.A+B cp ⇒ C + D) → IsPullback 𝒞 (Coproduct.i₂ cp) p₂ f i₂ + + -- pullbacks ⇒ top-row is coproduct + pullbacks⇒cp : {A B C : Obj} {f : A ⇒ B + C} (P₁ : Pullback 𝒞 f i₁) (P₂ : Pullback 𝒞 f i₂) → IsCoproduct 𝒞 (Pullback.p₁ P₁) (Pullback.p₁ P₂) + +Extensive⇒Distributive : ∀ {𝒞 : Category o ℓ e} → (cartesian : Cartesian 𝒞) → (E : Extensive 𝒞) → Distributive 𝒞 cartesian (Extensive.cocartesian E) +Extensive⇒Distributive {𝒞 = 𝒞} cartesian E = record + { distributeˡ = λ {A} {B} {C} → ≅-sym 𝒞 $ iso {A} {B} {C} + } + where + open Category 𝒞 + open Extensive E + open Cocartesian cocartesian + open Cartesian cartesian + open BinaryProducts products + open HomReasoning + open Equiv + open ≅ using () renaming (sym to ≅-sym) + pb₁ : ∀ {A B C} → Pullback 𝒞 (π₂ {A = A} {B = B + C}) i₁ + pb₁ {A} {B} {C} = record { P = A × B ; p₁ = id ⁂ i₁ ; p₂ = π₂ ; isPullback = record + { commute = π₂∘⁂ + ; universal = λ {X} {h₁} {h₂} H → ⟨ π₁ ∘ h₁ , h₂ ⟩ + ; unique = λ {X} {h₁} {h₂} {i} {eq} H1 H2 → sym (unique (sym $ + begin + π₁ ∘ h₁ ≈⟨ ∘-resp-≈ʳ (sym H1) ⟩ + (π₁ ∘ (id ⁂ i₁) ∘ i) ≈⟨ sym-assoc ⟩ + ((π₁ ∘ (id ⁂ i₁)) ∘ i) ≈⟨ ∘-resp-≈ˡ π₁∘⁂ ⟩ + ((id ∘ π₁) ∘ i) ≈⟨ ∘-resp-≈ˡ identityˡ ⟩ + π₁ ∘ i ∎) H2) + ; p₁∘universal≈h₁ = λ {X} {h₁} {h₂} {eq} → + begin + (id ⁂ i₁) ∘ ⟨ π₁ ∘ h₁ , h₂ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩ + ⟨ id ∘ π₁ ∘ h₁ , i₁ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congʳ identityˡ ⟩ + ⟨ π₁ ∘ h₁ , i₁ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congˡ (sym eq) ⟩ + ⟨ π₁ ∘ h₁ , π₂ ∘ h₁ ⟩ ≈⟨ g-η ⟩ + h₁ ∎ + ; p₂∘universal≈h₂ = λ {X} {h₁} {h₂} {eq} → project₂ + } } + pb₂ : ∀ {A B C} → Pullback 𝒞 (π₂ {A = A} {B = B + C}) i₂ + pb₂ {A} {B} {C} = record { P = A × C ; p₁ = id ⁂ i₂ ; p₂ = π₂ ; isPullback = record + { commute = π₂∘⁂ + ; universal = λ {X} {h₁} {h₂} H → ⟨ π₁ ∘ h₁ , h₂ ⟩ + ; unique = λ {X} {h₁} {h₂} {i} {eq} H1 H2 → sym (unique (sym $ + begin + π₁ ∘ h₁ ≈⟨ ∘-resp-≈ʳ (sym H1) ⟩ + (π₁ ∘ (id ⁂ i₂) ∘ i) ≈⟨ sym-assoc ⟩ + ((π₁ ∘ (id ⁂ i₂)) ∘ i) ≈⟨ ∘-resp-≈ˡ π₁∘⁂ ⟩ + ((id ∘ π₁) ∘ i) ≈⟨ ∘-resp-≈ˡ identityˡ ⟩ + π₁ ∘ i ∎) H2) + ; p₁∘universal≈h₁ = λ {X} {h₁} {h₂} {eq} → + begin + (id ⁂ i₂) ∘ ⟨ π₁ ∘ h₁ , h₂ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩ + ⟨ id ∘ π₁ ∘ h₁ , i₂ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congʳ identityˡ ⟩ + ⟨ π₁ ∘ h₁ , i₂ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congˡ (sym eq) ⟩ + ⟨ π₁ ∘ h₁ , π₂ ∘ h₁ ⟩ ≈⟨ g-η ⟩ + h₁ ∎ + ; p₂∘universal≈h₂ = λ {X} {h₁} {h₂} {eq} → project₂ + } } + cp₁ : ∀ {A B C : Obj} → IsCoproduct 𝒞 {A+B = A × (B + C)} (id ⁂ i₁) (id ⁂ i₂) + cp₁ {A} {B} {C} = pullbacks⇒cp pb₁ pb₂ + cp₂ = λ {A B C : Obj} → coproduct {A × B} {A × C} + iso = λ {A B C : Obj} → Coproduct.up-to-iso 𝒞 (IsCoproduct⇒Coproduct 𝒞 (cp₁ {A} {B} {C})) cp₂ \ No newline at end of file diff --git a/bsc.agda-lib b/bsc.agda-lib index 3f08382..a84bec8 100644 --- a/bsc.agda-lib +++ b/bsc.agda-lib @@ -1,3 +1,3 @@ name: bsc include: . -depend: standard-library, agda-categories \ No newline at end of file +depend: standard-library agda-categories \ No newline at end of file