From 609f75781ef5cdd25aa63839774ab062acecc8fa Mon Sep 17 00:00:00 2001 From: Leon Date: Tue, 8 Aug 2023 13:13:27 +0200 Subject: [PATCH] Big refactor, tidying up some proofs, compiling sadly is still slow --- ElgotAlgebra.agda | 10 +-- ElgotAlgebras.agda | 184 +++++++++++++++++---------------------------- 2 files changed, 76 insertions(+), 118 deletions(-) diff --git a/ElgotAlgebra.agda b/ElgotAlgebra.agda index 2b6d42e..25f115d 100644 --- a/ElgotAlgebra.agda +++ b/ElgotAlgebra.agda @@ -73,10 +73,10 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where #-Compositionality : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} → (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ #-Compositionality {X} {Y} {f} {h} = begin - (((f #) +₁ idC) ∘ h)# ≈⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ h} - {g = (f #) +₁ h} - {h = h} - (trans (pullˡ +₁∘+₁) (+₁-cong₂ identityˡ identityʳ ⟩∘⟨refl))⟩ + (((f #) +₁ idC) ∘ h)# ≈⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ h} + {g = (f #) +₁ h} + {h = h} + (trans (pullˡ +₁∘+₁) (+₁-cong₂ identityˡ identityʳ ⟩∘⟨refl))⟩ ((f # +₁ h)# ∘ h) ≈˘⟨ inject₂ ⟩ (([ idC ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂)) ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ (([ idC , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂) ≈˘⟨ #-Fixpoint {f = (f # +₁ h) } ⟩∘⟨refl ⟩ @@ -89,7 +89,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ] ∘ i₂) ≈˘⟨ pushˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = [ i₁ , h ]} - (begin + (begin (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ refl⟩∘⟨ ∘[] ⟩ (idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ diff --git a/ElgotAlgebras.agda b/ElgotAlgebras.agda index 2470731..2e3cec4 100644 --- a/ElgotAlgebras.agda +++ b/ElgotAlgebras.agda @@ -1,24 +1,18 @@ -open import Level renaming (suc to ℓ-suc) -open import Function using (_$_) renaming (id to idf; _∘_ to _∘ᶠ_) -open import Data.Product using (_,_) renaming (_×_ to _∧_) +open import Level -open import Categories.Category.Cocartesian -open import Categories.Category.Cocartesian.Bundle -open import Categories.Category.Cartesian -open import Categories.Functor renaming (id to idF) -open import Categories.Functor.Algebra -open import Categories.Object.Terminal -open import Categories.Object.Product -open import Categories.Object.Exponential -open import Categories.Object.Coproduct -open import Categories.Category.BinaryProducts +open import Categories.Category.Cocartesian using (Cocartesian) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.BinaryProducts using (BinaryProducts) +open import Categories.Functor using (Functor) renaming (id to idF) +open import Categories.Object.Terminal using (Terminal) +open import Categories.Object.Product using (Product) +open import Categories.Object.Coproduct using (Coproduct) +open import Categories.Object.Exponential using (Exponential) 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 +open import ElgotAlgebra using (Elgot-Algebra) +open import Extensive.Bundle using (ExtensiveDistributiveCategory) +import Categories.Morphism as M +import Categories.Morphism.Reasoning as MR module ElgotAlgebras where @@ -31,6 +25,10 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where open Cocartesian cocartesian open Cartesian cartesian open BinaryProducts products + open M C + open MR C + open HomReasoning + open Equiv --* -- let's define the category of elgot-algebras @@ -52,16 +50,10 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where ; _⇒_ = Elgot-Algebra-Morphism ; _≈_ = λ f g → Elgot-Algebra-Morphism.h f ≈ Elgot-Algebra-Morphism.h g ; id = λ {EB} → let open Elgot-Algebra EB in - record { h = idC; preserves = λ {X : Obj} {f : X ⇒ A + X} → begin - idC ∘ f # ≈⟨ identityˡ ⟩ - (f #) ≈⟨ sym $ #-resp-≈ identityˡ ⟩ - ((idC ∘ f) #) ≈⟨ sym (#-resp-≈ (∘-resp-≈ˡ +-η)) ⟩ - (([ i₁ , i₂ ] ∘ f)#) ≈⟨ sym $ #-resp-≈ (∘-resp-≈ˡ ([]-cong₂ identityʳ identityʳ)) ⟩ - (([ i₁ ∘ idC , i₂ ∘ idC ] ∘ f)#) ≈⟨ sym $ #-resp-≈ (∘-resp-≈ˡ []∘+₁) ⟩ - ((([ i₁ , i₂ ] ∘ (idC +₁ idC)) ∘ f)#) ≈⟨ #-resp-≈ assoc ⟩ - (([ i₁ , i₂ ] ∘ (idC +₁ idC) ∘ f)#) ≈⟨ #-resp-≈ (∘-resp-≈ˡ +-η) ⟩ - ((idC ∘ (idC +₁ idC) ∘ f)#) ≈⟨ #-resp-≈ identityˡ ⟩ - ((idC +₁ idC) ∘ f) # ∎ } + record { h = idC; preserves = λ {X : Obj} {f : X ⇒ A + X} → begin + idC ∘ f # ≈⟨ identityˡ ⟩ + f # ≈⟨ #-resp-≈ (introˡ (coproduct.unique id-comm-sym id-comm-sym)) ⟩ + ((idC +₁ idC) ∘ f) # ∎ } ; _∘_ = λ {EA} {EB} {EC} f g → let open Elgot-Algebra-Morphism f renaming (h to hᶠ; preserves to preservesᶠ) open Elgot-Algebra-Morphism g renaming (h to hᵍ; preserves to preservesᵍ) @@ -69,12 +61,9 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where open Elgot-Algebra EB using () renaming (_# to _#ᵇ; A to B) open Elgot-Algebra EC using () renaming (_# to _#ᶜ; A to C; #-resp-≈ to #ᶜ-resp-≈) in record { h = hᶠ ∘ hᵍ; preserves = λ {X} {f : X ⇒ A + X} → begin - (hᶠ ∘ hᵍ) ∘ (f #ᵃ) ≈⟨ assoc ⟩ - (hᶠ ∘ hᵍ ∘ (f #ᵃ)) ≈⟨ ∘-resp-≈ʳ preservesᵍ ⟩ + (hᶠ ∘ hᵍ) ∘ (f #ᵃ) ≈⟨ pullʳ preservesᵍ ⟩ (hᶠ ∘ (((hᵍ +₁ idC) ∘ f) #ᵇ)) ≈⟨ preservesᶠ ⟩ - (((hᶠ +₁ idC) ∘ (hᵍ +₁ idC) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ sym-assoc ⟩ - ((((hᶠ +₁ idC) ∘ (hᵍ +₁ idC)) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (∘-resp-≈ˡ +₁∘+₁) ⟩ - ((((hᶠ ∘ hᵍ) +₁ (idC ∘ idC)) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ refl (identity²))) ⟩ + (((hᶠ +₁ idC) ∘ (hᵍ +₁ idC) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (pullˡ (trans +₁∘+₁ (+₁-cong₂ refl (identity²)))) ⟩ ((hᶠ ∘ hᵍ +₁ idC) ∘ f) #ᶜ ∎ } ; identityˡ = identityˡ ; identityʳ = identityʳ @@ -88,10 +77,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where } ; ∘-resp-≈ = ∘-resp-≈ } - where - open Elgot-Algebra-Morphism - open HomReasoning - open Equiv + where open Elgot-Algebra-Morphism --* -- products and exponentials of elgot-algebras @@ -115,7 +101,6 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where } where open Terminal T - open Equiv -- if the carriers of the algebra form a product, so do the algebras A×B-Helper : ∀ {EA EB : Elgot-Algebra D} → Elgot-Algebra D @@ -124,88 +109,66 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where ; _# = λ {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 ⟨⟩∘ ⟩ - (⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f) ≈⟨ ∘-resp-≈ˡ (unique′ (begin - π₁ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₁ ⟩ - [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ≈⟨ []-cong₂ identityˡ identityʳ ⟩ - [ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ] ≈⟨ sym ([]-cong₂ identityʳ project₁) ⟩ - [ π₁ ∘ idC , π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈⟨ sym ∘[] ⟩ - π₁ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∎) (begin - π₂ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₂ ⟩ - [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ≈⟨ []-cong₂ identityˡ identityʳ ⟩ - [ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ] ≈⟨ sym ([]-cong₂ identityʳ project₂) ⟩ - [ π₂ ∘ idC , π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈⟨ sym ∘[] ⟩ - π₂ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∎) + ⟨ [ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ ((π₁ +₁ idC) ∘ f) , [ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ ((π₂ +₁ idC) ∘ f) ⟩ ≈⟨ ⟨⟩-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁) ⟩ + ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩ ≈˘⟨ ⟨⟩∘ ⟩ + (⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f) ≈⟨ ∘-resp-≈ˡ (unique′ + (begin + π₁ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₁ ⟩ + [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₁)) ⟩ + [ π₁ ∘ idC , π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈˘⟨ ∘[] ⟩ + π₁ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∎) + (begin + π₂ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₂ ⟩ + [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₂)) ⟩ + [ π₂ ∘ idC , π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈˘⟨ ∘[] ⟩ + π₂ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∎) )⟩ ([ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∘ f) ∎ - ; #-Uniformity = λ {X Y f g h} uni → unique′ (begin - π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩ - (((π₁ +₁ idC) ∘ f)#ᵃ) ≈⟨ #ᵃ-Uniformity (begin - (idC +₁ h) ∘ (π₁ +₁ idC) ∘ f ≈⟨ sym-assoc ⟩ - ((idC +₁ h) ∘ (π₁ +₁ idC)) ∘ f ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ - (idC ∘ π₁ +₁ h ∘ idC) ∘ f ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ - ((π₁ +₁ h) ∘ f) ≈⟨ sym (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) ⟩ - (((π₁ ∘ idC +₁ idC ∘ h)) ∘ f) ≈⟨ sym (∘-resp-≈ˡ +₁∘+₁) ⟩ - ((π₁ +₁ idC) ∘ (idC +₁ h)) ∘ f ≈⟨ assoc ⟩ - (π₁ +₁ idC) ∘ ((idC +₁ h) ∘ f) ≈⟨ ∘-resp-≈ʳ uni ⟩ - (π₁ +₁ idC) ∘ g ∘ h ≈⟨ sym-assoc ⟩ - ((π₁ +₁ idC) ∘ g) ∘ h ∎ - )⟩ - (((π₁ +₁ idC) ∘ g)#ᵃ ∘ h) ≈⟨ sym (∘-resp-≈ˡ project₁) ⟩ - ((π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩) ∘ h) ≈⟨ assoc ⟩ - π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎ - ) (begin - π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩ - ((π₂ +₁ idC) ∘ f)#ᵇ ≈⟨ #ᵇ-Uniformity (begin - (idC +₁ h) ∘ (π₂ +₁ idC) ∘ f ≈⟨ sym-assoc ⟩ - (((idC +₁ h) ∘ (π₂ +₁ idC)) ∘ f) ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ - ((idC ∘ π₂ +₁ h ∘ idC) ∘ f) ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ - ((π₂ +₁ h) ∘ f) ≈⟨ sym (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) ⟩ - ((((π₂ ∘ idC +₁ idC ∘ h)) ∘ f)) ≈⟨ sym (∘-resp-≈ˡ +₁∘+₁) ⟩ - ((π₂ +₁ idC) ∘ ((idC +₁ h))) ∘ f ≈⟨ assoc ⟩ - (π₂ +₁ idC) ∘ ((idC +₁ h)) ∘ f ≈⟨ ∘-resp-≈ʳ uni ⟩ - (π₂ +₁ idC) ∘ g ∘ h ≈⟨ sym-assoc ⟩ - ((π₂ +₁ idC) ∘ g) ∘ h ∎ - )⟩ - ((π₂ +₁ idC) ∘ g)#ᵇ ∘ h ≈⟨ sym (∘-resp-≈ˡ project₂) ⟩ - ((π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩) ∘ h) ≈⟨ assoc ⟩ - π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎ - ) + ; #-Uniformity = λ {X Y f g h} uni → unique′ + (begin + π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩ + (((π₁ +₁ idC) ∘ f)#ᵃ) ≈⟨ #ᵃ-Uniformity + (begin + -- TODO factor these out or adjust +₁ swap... maybe call it +₁-id-comm + (idC +₁ h) ∘ (π₁ +₁ idC) ∘ f ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm)) ⟩ + (π₁ ∘ idC +₁ idC ∘ h) ∘ f ≈˘⟨ pullˡ +₁∘+₁ ⟩ + (π₁ +₁ idC) ∘ (idC +₁ h) ∘ f ≈⟨ pushʳ uni ⟩ + ((π₁ +₁ idC) ∘ g) ∘ h ∎)⟩ + (((π₁ +₁ idC) ∘ g)#ᵃ ∘ h) ≈˘⟨ pullˡ project₁ ⟩ + π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎) + (begin + π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩ + ((π₂ +₁ idC) ∘ f)#ᵇ ≈⟨ #ᵇ-Uniformity + (begin + (idC +₁ h) ∘ (π₂ +₁ idC) ∘ f ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))⟩ + ((π₂ ∘ idC +₁ idC ∘ h) ∘ f) ≈˘⟨ pullˡ +₁∘+₁ ⟩ + (π₂ +₁ idC) ∘ ((idC +₁ h)) ∘ f ≈⟨ pushʳ uni ⟩ + ((π₂ +₁ idC) ∘ g) ∘ h ∎)⟩ + ((π₂ +₁ idC) ∘ g)#ᵇ ∘ h ≈˘⟨ pullˡ project₂ ⟩ + π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎) ; #-Folding = λ {X} {Y} {f} {h} → ⟨⟩-cong₂ (foldingˡ {X} {Y}) (foldingʳ {X} {Y}) ; #-resp-≈ = λ fg → ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ʳ fg)) (#ᵇ-resp-≈ (∘-resp-≈ʳ fg)) } 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 HomReasoning - open Equiv + +₁-id-swap : ∀ {X Y C} {f : X ⇒ (A × B) + X} {h : Y ⇒ X + Y} (π : A × B ⇒ C) → [ (idC +₁ i₁) ∘ ((π +₁ idC) ∘ f) , i₂ ∘ h ] ≈ (π +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] + +₁-id-swap {X} {Y} {C} {f} {h} π = begin ([ (idC +₁ i₁) ∘ ((π +₁ idC) ∘ f) , i₂ ∘ h ] ) ≈⟨ ([]-congʳ sym-assoc) ⟩ + ([ ((idC +₁ i₁) ∘ (π +₁ idC)) ∘ f , i₂ ∘ h ] ) ≈⟨ []-cong₂ (∘-resp-≈ˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))) (∘-resp-≈ˡ (sym identityʳ)) ⟩ + (([ (π ∘ idC +₁ idC ∘ i₁) ∘ f , (i₂ ∘ idC) ∘ h ])) ≈˘⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂) ⟩ + (([ (π +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π +₁ idC) ∘ i₂ ∘ h ])) ≈˘⟨ ∘[] ⟩ + ((π +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∎ foldingˡ : ∀ {X} {Y} {f} {h} → (((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ) ≈ ((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ foldingˡ {X} {Y} {f} {h} = begin - ((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ ≈⟨ #ᵃ-resp-≈ +₁∘+₁ ⟩ - ((π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵃ) ≈⟨ #ᵃ-resp-≈ (+₁-cong₂ project₁ identityˡ) ⟩ + ((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ ≈⟨ #ᵃ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₁ identityˡ)) ⟩ ((((π₁ +₁ idC) ∘ f)#ᵃ +₁ h)#ᵃ) ≈⟨ #ᵃ-Folding ⟩ - ([ (idC +₁ i₁) ∘ ((π₁ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-congʳ sym-assoc) ⟩ - ([ ((idC +₁ i₁) ∘ (π₁ +₁ idC)) ∘ f , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-congʳ (∘-resp-≈ˡ +₁∘+₁)) ⟩ - ([ ((idC ∘ π₁ +₁ i₁ ∘ idC)) ∘ f , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-congʳ (∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ))) ⟩ - ([ ((π₁ +₁ i₁)) ∘ f , i₂ ∘ h ] #ᵃ) ≈⟨ sym (#ᵃ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) (∘-resp-≈ˡ identityʳ))) ⟩ - (([ (π₁ ∘ idC +₁ idC ∘ i₁) ∘ f , (i₂ ∘ idC) ∘ h ])#ᵃ) ≈⟨ sym (#ᵃ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ +₁∘i₂))) ⟩ - (([ ((π₁ +₁ idC) ∘ (idC +₁ i₁)) ∘ f , ((π₁ +₁ idC) ∘ i₂) ∘ h ])#ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-cong₂ assoc assoc) ⟩ - (([ (π₁ +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π₁ +₁ idC) ∘ i₂ ∘ h ])#ᵃ) ≈⟨ sym (#ᵃ-resp-≈ ∘[]) ⟩ + ([ (idC +₁ i₁) ∘ ((π₁ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ (+₁-id-swap π₁)⟩ ((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ ∎ foldingʳ : ∀ {X} {Y} {f} {h} → ((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈ ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ foldingʳ {X} {Y} {f} {h} = begin - ((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈⟨ #ᵇ-resp-≈ +₁∘+₁ ⟩ - ((π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵇ) ≈⟨ #ᵇ-resp-≈ (+₁-cong₂ project₂ identityˡ) ⟩ + ((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈⟨ #ᵇ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₂ identityˡ)) ⟩ ((((π₂ +₁ idC) ∘ f)#ᵇ +₁ h)#ᵇ) ≈⟨ #ᵇ-Folding ⟩ - [ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ ≈⟨ #ᵇ-resp-≈ ([]-congʳ sym-assoc) ⟩ - ([ ((idC +₁ i₁) ∘ (π₂ +₁ idC)) ∘ f , i₂ ∘ h ] #ᵇ) ≈⟨ #ᵇ-resp-≈ ([]-congʳ (∘-resp-≈ˡ +₁∘+₁)) ⟩ - ([ ((idC ∘ π₂ +₁ i₁ ∘ idC)) ∘ f , i₂ ∘ h ] #ᵇ) ≈⟨ #ᵇ-resp-≈ ([]-congʳ (∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ))) ⟩ - ([ ((π₂ +₁ i₁)) ∘ f , i₂ ∘ h ] #ᵇ) ≈⟨ sym (#ᵇ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) (∘-resp-≈ˡ identityʳ))) ⟩ - (([ (π₂ ∘ idC +₁ idC ∘ i₁) ∘ f , (i₂ ∘ idC) ∘ h ])#ᵇ) ≈⟨ sym (#ᵇ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ +₁∘i₂))) ⟩ - (([ ((π₂ +₁ idC) ∘ (idC +₁ i₁)) ∘ f , ((π₂ +₁ idC) ∘ i₂) ∘ h ])#ᵇ) ≈⟨ #ᵇ-resp-≈ ([]-cong₂ assoc assoc) ⟩ - (([ (π₂ +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π₂ +₁ idC) ∘ i₂ ∘ h ])#ᵇ) ≈⟨ sym (#ᵇ-resp-≈ ∘[]) ⟩ + [ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ ≈⟨ #ᵇ-resp-≈ (+₁-id-swap π₂) ⟩ ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ ∎ Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra D) → Product Elgot-Algebras EA EB @@ -220,9 +183,8 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where begin ⟨ 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-≈ˡ +₁∘+₁))) ⟩ - ⟨ (((π₁ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC)) ∘ h) #ᵃ , (((π₂ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC)) ∘ h) #ᵇ ⟩ ≈⟨ (⟨⟩-cong₂ (#ᵃ-resp-≈ assoc) (#ᵇ-resp-≈ assoc)) ⟩ + ⟨ ((f′ +₁ idC) ∘ h) #ᵃ , ((g′ +₁ idC) ∘ h) #ᵇ ⟩ ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₁ identity²))) (#ᵇ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₂ identity²))) ⟩ + ⟨ ((π₁ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵃ , ((π₂ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵇ ⟩ ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (pullˡ +₁∘+₁)) (#ᵇ-resp-≈ (pullˡ +₁∘+₁)) ⟩ ⟨ ((π₁ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵃ , ((π₂ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵇ ⟩ ∎ } ; project₁ = project₁ ; project₂ = project₂ @@ -232,8 +194,6 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) 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}) using () renaming (_# to _#ᵖ) - open HomReasoning - open Equiv -- if the carrier is cartesian, so is the category of algebras @@ -242,8 +202,6 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where { terminal = Terminal-Elgot-Algebras terminal ; products = record { product = λ {EA EB} → Product-Elgot-Algebras EA EB } } - where - open Equiv -- if the carriers of the algebra form a exponential, so do the algebras B^A-Helper : ∀ {EA : Elgot-Algebra D} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra D