leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Big refactor, tidying up some proofs, compiling sadly is still slow

Browse source
This commit is contained in:
Leon 2023-08-08 13:13:27 +02:00
parent 597b03af8a
commit 609f75781e
Failed to generate hash of commit
2 changed files with 76 additions and 118 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
ElgotAlgebra.agda
View file

@ -73,10 +73,10 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
#-Compositionality : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} #-Compositionality : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
→ (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ → (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂
#-Compositionality {X} {Y} {f} {h} = begin #-Compositionality {X} {Y} {f} {h} = begin
(((f #) +₁ idC) ∘ h)# ≈⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ h} (((f #) +₁ idC) ∘ h)# ≈⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ h}
{g = (f #) +₁ h} {g = (f #) +₁ h}
{h = h} {h = h}
(trans (pullˡ +₁∘+₁) (+₁-cong₂ identityˡ identityʳ ⟩∘⟨refl))⟩ (trans (pullˡ +₁∘+₁) (+₁-cong₂ identityˡ identityʳ ⟩∘⟨refl))⟩
((f # +₁ h)# ∘ h) ≈˘⟨ inject₂ ⟩ ((f # +₁ h)# ∘ h) ≈˘⟨ inject₂ ⟩
(([ idC ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂)) ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ (([ idC ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂)) ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
(([ idC , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂) ≈˘⟨ #-Fixpoint {f = (f # +₁ h) } ⟩∘⟨refl ⟩ (([ idC , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂) ≈˘⟨ #-Fixpoint {f = (f # +₁ h) } ⟩∘⟨refl ⟩

182
ElgotAlgebras.agda
View file

@ -1,24 +1,18 @@
open import Level renaming (suc to ℓ-suc) open import Level
open import Function using (_$_) renaming (id to idf; _∘_ to _∘ᶠ_)
open import Data.Product using (_,_) renaming (_×_ to _∧_)
open import Categories.Category.Cocartesian open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category.Cocartesian.Bundle open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.Cartesian open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Functor renaming (id to idF) open import Categories.Functor using (Functor) renaming (id to idF)
open import Categories.Functor.Algebra open import Categories.Object.Terminal using (Terminal)
open import Categories.Object.Terminal open import Categories.Object.Product using (Product)
open import Categories.Object.Product open import Categories.Object.Coproduct using (Coproduct)
open import Categories.Object.Exponential open import Categories.Object.Exponential using (Exponential)
open import Categories.Object.Coproduct
open import Categories.Category.BinaryProducts
open import Categories.Category open import Categories.Category
open import ElgotAlgebra open import ElgotAlgebra using (Elgot-Algebra)
open import Distributive.Bundle open import Extensive.Bundle using (ExtensiveDistributiveCategory)
open import Distributive.Core import Categories.Morphism as M
open import Extensive.Bundle import Categories.Morphism.Reasoning as MR
open import Extensive.Core
open import Categories.Morphism
module ElgotAlgebras where module ElgotAlgebras where
@ -31,6 +25,10 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
open Cocartesian cocartesian open Cocartesian cocartesian
open Cartesian cartesian open Cartesian cartesian
open BinaryProducts products open BinaryProducts products
open M C
open MR C
open HomReasoning
open Equiv
--* --*
-- let's define the category of elgot-algebras -- let's define the category of elgot-algebras
@ -53,15 +51,9 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
; _≈_ = λ f g → Elgot-Algebra-Morphism.h f ≈ Elgot-Algebra-Morphism.h g ; _≈_ = λ f g → Elgot-Algebra-Morphism.h f ≈ Elgot-Algebra-Morphism.h g
; id = λ {EB} → let open Elgot-Algebra EB in ; id = λ {EB} → let open Elgot-Algebra EB in
record { h = idC; preserves = λ {X : Obj} {f : X ⇒ A + X} → begin record { h = idC; preserves = λ {X : Obj} {f : X ⇒ A + X} → begin
idC ∘ f # ≈⟨ identityˡ ⟩ idC ∘ f # ≈⟨ identityˡ ⟩
(f #) ≈⟨ sym $ #-resp-≈ identityˡ ⟩ f # ≈⟨ #-resp-≈ (introˡ (coproduct.unique id-comm-sym id-comm-sym)) ⟩
((idC ∘ f) #) ≈⟨ sym (#-resp-≈ (∘-resp-≈ˡ +-η)) ⟩ ((idC +₁ idC) ∘ f) # ∎ }
(([ 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) # ∎ }
; _∘_ = λ {EA} {EB} {EC} f g → let ; _∘_ = λ {EA} {EB} {EC} f g → let
open Elgot-Algebra-Morphism f renaming (h to hᶠ; preserves to preservesᶠ) open Elgot-Algebra-Morphism f renaming (h to hᶠ; preserves to preservesᶠ)
open Elgot-Algebra-Morphism g 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 EB using () renaming (_# to _#ᵇ; A to B)
open Elgot-Algebra EC using () renaming (_# to _#ᶜ; A to C; #-resp-≈ to #ᶜ-resp-≈) 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 in record { h = hᶠ ∘ hᵍ; preserves = λ {X} {f : X ⇒ A + X} → begin
(hᶠ ∘ hᵍ) ∘ (f #ᵃ) ≈⟨ assoc ⟩ (hᶠ ∘ hᵍ) ∘ (f #ᵃ) ≈⟨ pullʳ preservesᵍ ⟩
(hᶠ ∘ hᵍ ∘ (f #ᵃ)) ≈⟨ ∘-resp-≈ʳ preservesᵍ ⟩
(hᶠ ∘ (((hᵍ +₁ idC) ∘ f) #ᵇ)) ≈⟨ preservesᶠ ⟩ (hᶠ ∘ (((hᵍ +₁ idC) ∘ f) #ᵇ)) ≈⟨ preservesᶠ ⟩
(((hᶠ +₁ idC) ∘ (hᵍ +₁ idC) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ sym-assoc ⟩ (((hᶠ +₁ idC) ∘ (hᵍ +₁ idC) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (pullˡ (trans +₁∘+₁ (+₁-cong₂ refl (identity²)))) ⟩
((((hᶠ +₁ idC) ∘ (hᵍ +₁ idC)) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (∘-resp-≈ˡ +₁∘+₁) ⟩
((((hᶠ ∘ hᵍ) +₁ (idC ∘ idC)) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ refl (identity²))) ⟩
((hᶠ ∘ hᵍ +₁ idC) ∘ f) #ᶜ ∎ } ((hᶠ ∘ hᵍ +₁ idC) ∘ f) #ᶜ ∎ }
; identityˡ = identityˡ ; identityˡ = identityˡ
; identityʳ = identityʳ ; identityʳ = identityʳ
@ -88,10 +77,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
} }
; ∘-resp-≈ = ∘-resp-≈ ; ∘-resp-≈ = ∘-resp-≈
} }
where where open Elgot-Algebra-Morphism
open Elgot-Algebra-Morphism
open HomReasoning
open Equiv
--* --*
-- products and exponentials of elgot-algebras -- products and exponentials of elgot-algebras
@ -115,7 +101,6 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
} }
where where
open Terminal T open Terminal T
open Equiv
-- if the carriers of the algebra form a product, so do the algebras -- if the carriers of the algebra form a product, so do the algebras
A×B-Helper : ∀ {EA EB : Elgot-Algebra D} → Elgot-Algebra D 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)#ᵇ ⟩ ; _# = λ {X : Obj} (h : X ⇒ A×B + X) → ⟨ ((π₁ +₁ idC) ∘ h)#ᵃ , ((π₂ +₁ idC) ∘ h)#ᵇ ⟩
; #-Fixpoint = λ {X} {f} → begin ; #-Fixpoint = λ {X} {f} → begin
⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩ ⟨ ((π₁ +₁ 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₂ (pullˡ []∘+₁) (pullˡ []∘+₁) ⟩
⟨ ([ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ (π₁ +₁ idC)) ∘ f , ([ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ (π₂ +₁ idC)) ∘ f ⟩ ≈⟨ ⟨⟩-cong₂ (∘-resp-≈ˡ []∘+₁) (∘-resp-≈ˡ []∘+₁) ⟩ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩ ≈˘⟨ ⟨⟩∘ ⟩
⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩ ≈⟨ sym ⟨⟩∘ ⟩ (⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f) ≈⟨ ∘-resp-≈ˡ (unique′
(⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f) ≈⟨ ∘-resp-≈ˡ (unique′ (begin (begin
π₁ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₁ ⟩ π₁ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₁ ⟩
[ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ≈⟨ []-cong₂ identityˡ identityʳ ⟩ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₁)) ⟩
[ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ] ≈⟨ sym ([]-cong₂ identityʳ project₁) ⟩ [ π₁ ∘ idC , π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈˘⟨ ∘[] ⟩
[ π₁ ∘ idC , π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈⟨ sym ∘[] ⟩ π₁ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∎)
π₁ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∎) (begin (begin
π₂ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₂ ⟩ π₂ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₂ ⟩
[ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ≈⟨ []-cong₂ identityˡ identityʳ ⟩ [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₂)) ⟩
[ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ] ≈⟨ sym ([]-cong₂ identityʳ project₂) ⟩ [ π₂ ∘ idC , π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈˘⟨ ∘[] ⟩
[ π₂ ∘ idC , π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈⟨ sym ∘[] ⟩ π₂ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∎)
π₂ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∎)
)⟩ )⟩
([ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∘ f) ∎ ([ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∘ f) ∎
; #-Uniformity = λ {X Y f g h} uni → unique′ (begin ; #-Uniformity = λ {X Y f g h} uni → unique′
π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩ (begin
(((π₁ +₁ idC) ∘ f)#ᵃ) ≈⟨ #ᵃ-Uniformity (begin π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩
(idC +₁ h) ∘ (π₁ +₁ idC) ∘ f ≈⟨ sym-assoc ⟩ (((π₁ +₁ idC) ∘ f)#ᵃ) ≈⟨ #ᵃ-Uniformity
((idC +₁ h) ∘ (π₁ +₁ idC)) ∘ f ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ (begin
(idC ∘ π₁ +₁ h ∘ idC) ∘ f ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ -- TODO factor these out or adjust +₁ swap... maybe call it +₁-id-comm
((π₁ +₁ h) ∘ f) ≈⟨ sym (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) ⟩ (idC +₁ h) ∘ (π₁ +₁ idC) ∘ f ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm)) ⟩
(((π₁ ∘ idC +₁ idC ∘ h)) ∘ f) ≈⟨ sym (∘-resp-≈ˡ +₁∘+₁) ⟩ (π₁ ∘ idC +₁ idC ∘ h) ∘ f ≈˘⟨ pullˡ +₁∘+₁ ⟩
((π₁ +₁ idC) ∘ (idC +₁ h)) ∘ f ≈⟨ assoc ⟩ (π₁ +₁ idC) ∘ (idC +₁ h) ∘ f ≈⟨ pushʳ uni ⟩
(π₁ +₁ idC) ∘ ((idC +₁ h) ∘ f) ≈⟨ ∘-resp-≈ʳ uni ⟩ ((π₁ +₁ idC) ∘ g) ∘ h ∎)⟩
(π₁ +₁ idC) ∘ g ∘ h ≈⟨ sym-assoc ⟩ (((π₁ +₁ idC) ∘ g)#ᵃ ∘ h) ≈˘⟨ pullˡ project₁ ⟩
((π₁ +₁ idC) ∘ g) ∘ h ∎ π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎)
)⟩ (begin
(((π₁ +₁ idC) ∘ g)#ᵃ ∘ h) ≈⟨ sym (∘-resp-≈ˡ project₁) ⟩ π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩
((π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩) ∘ h) ≈⟨ assoc ⟩ ((π₂ +₁ idC) ∘ f)#ᵇ ≈⟨ #ᵇ-Uniformity
π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎ (begin
) (begin (idC +₁ h) ∘ (π₂ +₁ idC) ∘ f ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))⟩
π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩ ((π₂ ∘ idC +₁ idC ∘ h) ∘ f) ≈˘⟨ pullˡ +₁∘+₁ ⟩
((π₂ +₁ idC) ∘ f)#ᵇ ≈⟨ #ᵇ-Uniformity (begin (π₂ +₁ idC) ∘ ((idC +₁ h)) ∘ f ≈⟨ pushʳ uni ⟩
(idC +₁ h) ∘ (π₂ +₁ idC) ∘ f ≈⟨ sym-assoc ⟩ ((π₂ +₁ idC) ∘ g) ∘ h ∎)⟩
(((idC +₁ h) ∘ (π₂ +₁ idC)) ∘ f) ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ ((π₂ +₁ idC) ∘ g)#ᵇ ∘ h ≈˘⟨ pullˡ project₂ ⟩
((idC ∘ π₂ +₁ h ∘ idC) ∘ f) ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎)
((π₂ +₁ 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 ∎
)
; #-Folding = λ {X} {Y} {f} {h} → ⟨⟩-cong₂ (foldingˡ {X} {Y}) (foldingʳ {X} {Y}) ; #-Folding = λ {X} {Y} {f} {h} → ⟨⟩-cong₂ (foldingˡ {X} {Y}) (foldingʳ {X} {Y})
; #-resp-≈ = λ fg → ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ʳ fg)) (#ᵇ-resp-≈ (∘-resp-≈ʳ fg)) ; #-resp-≈ = λ fg → ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ʳ fg)) (#ᵇ-resp-≈ (∘-resp-≈ʳ fg))
} }
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 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 EB using () renaming (A to B; _# to _#ᵇ; #-Fixpoint to #ᵇ-Fixpoint; #-Uniformity to #ᵇ-Uniformity; #-Folding to #ᵇ-Folding; #-resp-≈ to #ᵇ-resp-≈)
open HomReasoning +₁-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 ]
open Equiv +₁-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} → (((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ) ≈ ((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ
foldingˡ {X} {Y} {f} {h} = begin foldingˡ {X} {Y} {f} {h} = begin
((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ ≈⟨ #ᵃ-resp-≈ +₁∘+₁ ⟩ ((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ ≈⟨ #ᵃ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₁ identityˡ)) ⟩
((π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵃ) ≈⟨ #ᵃ-resp-≈ (+₁-cong₂ project₁ identityˡ) ⟩
((((π₁ +₁ idC) ∘ f)#ᵃ +₁ h)#ᵃ) ≈⟨ #ᵃ-Folding ⟩ ((((π₁ +₁ idC) ∘ f)#ᵃ +₁ h)#ᵃ) ≈⟨ #ᵃ-Folding ⟩
([ (idC +₁ i₁) ∘ ((π₁ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-congʳ sym-assoc) ⟩ ([ (idC +₁ i₁) ∘ ((π₁ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ (+₁-id-swap π₁)⟩
([ ((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) ∘ [ (idC +₁ i₁) ∘ f , 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} → ((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈ ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ
foldingʳ {X} {Y} {f} {h} = begin foldingʳ {X} {Y} {f} {h} = begin
((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈⟨ #ᵇ-resp-≈ +₁∘+₁ ⟩ ((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈⟨ #ᵇ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₂ identityˡ)) ⟩
((π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵇ) ≈⟨ #ᵇ-resp-≈ (+₁-cong₂ project₂ identityˡ) ⟩
((((π₂ +₁ idC) ∘ f)#ᵇ +₁ h)#ᵇ) ≈⟨ #ᵇ-Folding ⟩ ((((π₂ +₁ idC) ∘ f)#ᵇ +₁ h)#ᵇ) ≈⟨ #ᵇ-Folding ⟩
[ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ ≈⟨ #ᵇ-resp-≈ ([]-congʳ sym-assoc) ⟩ [ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ ≈⟨ #ᵇ-resp-≈ (+₁-id-swap π₂) ⟩
([ ((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) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ ∎ ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ ∎
Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra D) → Product Elgot-Algebras EA EB Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra D) → Product Elgot-Algebras EA EB
@ -220,9 +183,8 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
begin begin
⟨ f′ , g′ ⟩ ∘ (h #ᵉ) ≈⟨ ⟨⟩∘ ⟩ ⟨ f′ , g′ ⟩ ∘ (h #ᵉ) ≈⟨ ⟨⟩∘ ⟩
⟨ f′ ∘ (h #ᵉ) , g′ ∘ (h #ᵉ) ⟩ ≈⟨ ⟨⟩-cong₂ preservesᶠ preservesᵍ ⟩ ⟨ 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′ +₁ 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) #ᵇ ⟩ ≈⟨ sym (⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ +₁∘+₁)) (#ᵇ-resp-≈ (∘-resp-≈ˡ +₁∘+₁))) ⟩ ⟨ ((π₁ ∘ ⟨ 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) #ᵇ ⟩ ≈⟨ (⟨⟩-cong₂ (#ᵃ-resp-≈ assoc) (#ᵇ-resp-≈ assoc)) ⟩
⟨ ((π₁ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵃ , ((π₂ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵇ ⟩ ∎ } ⟨ ((π₁ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵃ , ((π₂ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵇ ⟩ ∎ }
; project₁ = project₁ ; project₁ = project₁
; 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 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 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 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 -- 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 { terminal = Terminal-Elgot-Algebras terminal
; products = record { product = λ {EA EB} → Product-Elgot-Algebras EA EB } ; 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 -- 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 B^A-Helper : ∀ {EA : Elgot-Algebra D} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra D