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

Major refactor and improvement of proofs

Browse source
This commit is contained in:
Leon Vatthauer 2023-08-07 19:58:08 +02:00
parent ae16aea8b4
commit f7dfe31f3d
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 202 additions and 205 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

405
ElgotAlgebra.agda
View file

@ -1,228 +1,225 @@
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.Bundle using (CocartesianCategory)
open import Categories.Functor renaming (id to idF) open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Algebra open import Categories.Functor.Algebra
open import Categories.Object.Product
open import Categories.Object.Coproduct
open import Categories.Category open import Categories.Category
open import Distributive.Core
open import Categories.Category.Cartesian open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts open import Categories.Category.BinaryProducts
open import Categories.Category.Cocartesian open import Categories.Category.Cocartesian
open import Extensive.Bundle open import Extensive.Bundle
open import Extensive.Core import Categories.Morphism.Reasoning as MR
private private
variable variable
o ℓ e : Level o ℓ e : Level
module _ (D : ExtensiveDistributiveCategory o ℓ e) where module _ (D : ExtensiveDistributiveCategory o ℓ e) where
open ExtensiveDistributiveCategory D renaming (U to C; id to idC) open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
open Cocartesian cocartesian open Cocartesian cocartesian
open Cartesian cartesian open Cartesian cartesian
open MR C
--* --*
-- F-guarded Elgot Algebra -- F-guarded Elgot Algebra
--* --*
module _ {F : Endofunctor C} (FA : F-Algebra F) where module _ {F : Endofunctor C} (FA : F-Algebra F) where
record Guarded-Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where record Guarded-Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where
open Functor F public open Functor F public
open F-Algebra FA public open F-Algebra FA public
-- iteration operator -- iteration operator
field field
_# : ∀ {X} → (X ⇒ A + F₀ X) → (X ⇒ A) _# : ∀ {X} → (X ⇒ A + F₀ X) → (X ⇒ A)
-- _# properties -- _# properties
field field
#-Fixpoint : ∀ {X} {f : X ⇒ A + F₀ X } #-Fixpoint : ∀ {X} {f : X ⇒ A + F₀ X }
→ f # ≈ [ idC , α ∘ F₁ (f #) ] ∘ f → f # ≈ [ idC , α ∘ F₁ (f #) ] ∘ f
#-Uniformity : ∀ {X Y} {f : X ⇒ A + F₀ X} {g : Y ⇒ A + F₀ Y} {h : X ⇒ Y} #-Uniformity : ∀ {X Y} {f : X ⇒ A + F₀ X} {g : Y ⇒ A + F₀ Y} {h : X ⇒ Y}
→ (idC +₁ F₁ h) ∘ f ≈ g ∘ h → (idC +₁ F₁ h) ∘ f ≈ g ∘ h
→ f # ≈ g # ∘ h → f # ≈ g # ∘ h
#-Compositionality : ∀ {X Y} {f : X ⇒ A + F₀ X} {h : Y ⇒ X + F₀ Y} #-Compositionality : ∀ {X Y} {f : X ⇒ A + F₀ X} {h : Y ⇒ X + F₀ Y}
→ (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ (F₁ i₁)) ∘ f , i₂ ∘ (F₁ i₂) ] ∘ [ i₁ , h ])# ∘ i₂ → (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ (F₁ i₁)) ∘ f , i₂ ∘ (F₁ i₂) ] ∘ [ i₁ , h ])# ∘ i₂
#-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X} #-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X}
→ f ≈ g → f ≈ g
→ (f #) ≈ (g #) → (f #) ≈ (g #)
--* --*
-- (unguarded) Elgot-Algebra -- (unguarded) Elgot-Algebra
--* --*
module _ where record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where
record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where -- Object
-- Object field
field A : Obj
A : Obj
-- iteration operator -- iteration operator
field field
_# : ∀ {X} → (X ⇒ A + X) → (X ⇒ A) _# : ∀ {X} → (X ⇒ A + X) → (X ⇒ A)
-- _# properties -- _# properties
field field
#-Fixpoint : ∀ {X} {f : X ⇒ A + X } #-Fixpoint : ∀ {X} {f : X ⇒ A + X }
→ f # ≈ [ idC , f # ] ∘ f → f # ≈ [ idC , f # ] ∘ f
#-Uniformity : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ A + Y} {h : X ⇒ Y} #-Uniformity : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ A + Y} {h : X ⇒ Y}
→ (idC +₁ h) ∘ f ≈ g ∘ h → (idC +₁ h) ∘ f ≈ g ∘ h
→ f # ≈ g # ∘ h → f # ≈ g # ∘ h
#-Folding : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} #-Folding : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
→ ((f #) +₁ h)# ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # → ((f #) +₁ h)# ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #
#-resp-≈ : ∀ {X} {f g : X ⇒ A + X} → f ≈ g → (f #) ≈ (g #) #-resp-≈ : ∀ {X} {f g : X ⇒ A + X} → f ≈ g → (f #) ≈ (g #)
open HomReasoning open HomReasoning
open Equiv open Equiv
-- Compositionality is derivable -- Compositionality is derivable
#-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} {g = (f #) +₁ h} {h = h} ( (((f #) +₁ idC) ∘ h)# ≈⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ h}
begin {g = (f #) +₁ h}
((idC +₁ h) ∘ ((f #) +₁ idC) ∘ h) ≈⟨ sym-assoc ⟩ {h = h}
(((idC +₁ h) ∘ ((f #) +₁ idC)) ∘ h) ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ (trans (pullˡ +₁∘+₁) (+₁-cong₂ identityˡ identityʳ ⟩∘⟨refl))⟩
((((idC ∘ (f #)) +₁ (h ∘ idC))) ∘ h) ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ ((f # +₁ h)# ∘ h) ≈˘⟨ inject₂ ⟩
((((f #) +₁ h)) ∘ h) ∎) (([ idC ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂)) ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
⟩ (([ idC , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂) ≈˘⟨ #-Fixpoint {f = (f # +₁ h) } ⟩∘⟨refl ⟩
((f # +₁ h)# ∘ h) ≈⟨ sym inject₂ ⟩ (f # +₁ h)# ∘ i₂ ≈⟨ #-Folding ⟩∘⟨refl ⟩
(([ idC ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂)) ≈⟨ ∘-resp-≈ˡ (sym $ []∘+₁) ⟩ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂) ≈⟨ #-Fixpoint ⟩∘⟨refl ⟩
(([ idC , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂) ≈⟨ (sym $ ∘-resp-≈ˡ (#-Fixpoint {f = (f # +₁ h) })) ⟩ ([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ]
(f # +₁ h)# ∘ i₂ ≈⟨ ∘-resp-≈ˡ #-Folding ⟩ ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂ ≈⟨ pullʳ inject₂ ⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂) ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ [ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ (i₂ ∘ h) ≈⟨ pullˡ inject₂ ⟩
([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂ ≈⟨ assoc ⟩ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h) ≈˘⟨ refl⟩∘⟨ inject₂ {f = i₁} {g = h} ⟩
[ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂) ≈⟨ ∘-resp-≈ʳ inject₂ ⟩ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ] ∘ i₂) ≈˘⟨ pushˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]}
[ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ (i₂ ∘ h) ≈⟨ sym-assoc ⟩ {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]}
(([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h) ≈⟨ ∘-resp-≈ˡ inject₂ ⟩ {h = [ i₁ , h ]}
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h) ≈⟨ ∘-resp-≈ʳ $ sym (inject₂ {f = i₁} {g = h}) ⟩ (begin
[ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ ([ i₁ , h ] ∘ i₂) ≈⟨ sym-assoc ⟩ (idC +₁ [ i₁ , h ])
(([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂) ≈⟨ sym (∘-resp-≈ˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = [ i₁ , h ]} ( ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ refl⟩∘⟨ ∘[] ⟩
begin (idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁
(idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ ∘-resp-≈ʳ ∘[] ⟩ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ refl⟩∘⟨ []-congʳ inject₁ ⟩
(idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘-resp-≈ʳ ([]-congʳ inject₁) ⟩ (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f
((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]) ≈⟨ ∘[] ⟩ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘[] ⟩
[ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) , (idC +₁ [ i₁ , h ]) ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ sym-assoc sym-assoc ⟩ [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f)
[ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ ∘[]) ⟩ , (idC +₁ [ i₁ , h ]) ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ ∘[]) ⟩
[ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f , ([ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) , (idC +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁))) (∘-resp-≈ˡ ([]-cong₂ sym-assoc sym-assoc)) ⟩ [ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
[ (idC +₁ i₁) ∘ f , ([ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ i₂) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ inject₂))) ⟩ , [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f)
[ (idC +₁ i₁) ∘ f , ([ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩ , (idC +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ] ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁)))
[ (idC +₁ i₁) ∘ f , ([ (idC +₁ i₁) ∘ f , i₂ ∘ ([ i₁ , h ] ∘ i₂) ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩ (∘-resp-≈ˡ ([]-cong₂ (pullˡ +₁∘+₁) (pullˡ inject₂))) ⟩
[ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ []-congʳ (sym (inject₁)) ⟩ [ (idC +₁ i₁) ∘ f , ([ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
[ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ sym ∘[] ⟩ , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁))
[ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎)) (pullʳ inject₂))) ⟩
)⟩ [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ []-congʳ inject₁ ⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ ∎ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁
, [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ ∘[] ⟩
[ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎))
⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ ∎
-- every elgot-algebra comes with a divergence constant -- every elgot-algebra comes with a divergence constant
!ₑ : ⊥ ⇒ A !ₑ : ⊥ ⇒ A
!ₑ = i₂ # !ₑ = i₂ #
--* --*
-- Here follows the proof of equivalence for unguarded and Id-guarded Elgot-Algebras -- Here follows the proof of equivalence for unguarded and Id-guarded Elgot-Algebras
--* --*
private private
-- identity functor on 𝒞 -- identity algebra
Id : Functor C C Id-Algebra : Obj → F-Algebra (idF {C = C})
Id = idF {C = C} Id-Algebra A = record
{ A = A
; α = idC
}
where open Functor (idF {C = C})
-- identity algebra -- constructing an Id-Guarded Elgot-Algebra from an unguarded one
Id-Algebra : Obj → F-Algebra Id Unguarded→Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra (Id-Algebra (Elgot-Algebra.A EA))
Id-Algebra A = record Unguarded→Id-Guarded ea = record
{ A = A { _# = _#
; α = idC ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (sym (∘-resp-≈ˡ ([]-congˡ identityˡ)))
} ; #-Uniformity = #-Uniformity
where open Functor Id ; #-Compositionality = #-Compositionality
; #-resp-≈ = #-resp-≈
}
where
open Elgot-Algebra ea
open HomReasoning
open Equiv
-- constructing an Id-Guarded Elgot-Algebra from an unguarded one -- constructing an unguarded Elgot-Algebra from an Id-Guarded one
Unguarded→Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra (Id-Algebra (Elgot-Algebra.A EA)) Id-Guarded→Unguarded : ∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra
Unguarded→Id-Guarded ea = record Id-Guarded→Unguarded gea = record
{ _# = _# { _# = _#
; #-Fixpoint = λ {X} {f} → begin ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (∘-resp-≈ˡ ([]-congˡ identityˡ))
f # ≈⟨ #-Fixpoint ⟩ ; #-Uniformity = #-Uniformity
[ idC , f # ] ∘ f ≈⟨ sym $ ∘-resp-≈ˡ ([]-congˡ identityˡ) ⟩ ; #-Folding = λ {X} {Y} {f} {h} → begin
[ idC , idC ∘ f # ] ∘ f ∎ ((f #) +₁ h) # ≈˘⟨ +-g-η ⟩
; #-Uniformity = #-Uniformity [ (f # +₁ h)# ∘ i₁ , (f # +₁ h)# ∘ i₂ ] ≈⟨ []-cong₂ left right ⟩
; #-Compositionality = #-Compositionality [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ] ≈⟨ +-g-η ⟩
; #-resp-≈ = #-resp-≈ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #) ∎
} ; #-resp-≈ = #-resp-≈
where }
open Elgot-Algebra ea where
open HomReasoning open Guarded-Elgot-Algebra gea
open Equiv open HomReasoning
open Equiv
-- constructing an unguarded Elgot-Algebra from an Id-Guarded one left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
Id-Guarded→Unguarded : ∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra → (f # +₁ h)# ∘ i₁ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁
Id-Guarded→Unguarded gea = record left {X} {Y} {f} {h} = begin
{ _# = _# (f # +₁ h)# ∘ i₁ ≈⟨ #-Fixpoint ⟩∘⟨refl ⟩
; #-Fixpoint = λ {X} {f} → begin ([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₁ ≈⟨ pullʳ +₁∘i₁ ⟩
f # ≈⟨ #-Fixpoint ⟩ [ idC , idC ∘ (((f #) +₁ h) #) ] ∘ (i₁ ∘ f #) ≈⟨ cancelˡ inject₁ ⟩
[ idC , idC ∘ f # ] ∘ f ≈⟨ ∘-resp-≈ˡ ([]-congˡ identityˡ) ⟩ (f #) ≈⟨ #-Uniformity {f = f}
[ idC , f # ] ∘ f ∎ {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]}
; #-Uniformity = #-Uniformity {h = i₁}
; #-Folding = λ {X} {Y} {f} {h} → begin (sym inject₁)⟩
((f #) +₁ h) # ≈⟨ sym +-g-η ⟩ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁) ∎
[ (f # +₁ h)# ∘ i₁ , (f # +₁ h)# ∘ i₂ ] ≈⟨ []-cong₂ left right ⟩ byUni : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
[ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ] ≈⟨ +-g-η ⟩ → (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ]
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #) ∎ byUni {X} {Y} {f} {h} = begin
; #-resp-≈ = #-resp-≈ (idC +₁ [ i₁ , h ])
} ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ ∘-resp-≈ʳ (trans ∘[] ([]-congʳ inject₁)) ⟩
where (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f
open Guarded-Elgot-Algebra gea , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘[] ⟩
open HomReasoning [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f)
open Equiv , (idC +₁ [ i₁ , h ]) ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ sym-assoc sym-assoc ⟩
left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} [ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f
→ (f # +₁ h)# ∘ i₁ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ ∘[]) ⟩
left {X} {Y} {f} {h} = begin [ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
(f # +₁ h)# ∘ i₁ ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ , [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f)
(([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₁) ≈⟨ assoc ⟩ , (idC +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ] ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁)))
([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ (((f #) +₁ h) ∘ i₁)) ≈⟨ ∘-resp-≈ ([]-congˡ identityˡ) +₁∘i₁ ⟩ (∘-resp-≈ˡ ([]-cong₂ sym-assoc sym-assoc)) ⟩
([ idC , ((f #) +₁ h) # ] ∘ (i₁ ∘ (f #))) ≈⟨ sym-assoc ⟩ [ (idC +₁ i₁) ∘ f
(([ idC , ((f #) +₁ h) # ] ∘ i₁) ∘ (f #)) ≈⟨ ∘-resp-≈ˡ inject₁ ⟩ , [ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f
idC ∘ (f #) ≈⟨ identityˡ ⟩ , ((idC +₁ [ i₁ , h ]) ∘ i₂) ∘ i₂ ] ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ inject₂))) ⟩
(f #) ≈⟨ #-Uniformity {f = f} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = i₁} (sym inject₁) ⟩ [ (idC +₁ i₁) ∘ f
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁) ∎ , [ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
right : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ] ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩
→ (f # +₁ h)# ∘ i₂ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ [ (idC +₁ i₁) ∘ f
right {X} {Y} {f} {h} = begin , [ (idC +₁ i₁) ∘ f
(f # +₁ h)# ∘ i₂ ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ , i₂ ∘ ([ i₁ , h ] ∘ i₂) ] ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩
(([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₂) ≈⟨ assoc ⟩ [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ []-congʳ inject₁ ⟩
([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h) ∘ i₂) ≈⟨ ∘-resp-≈ ([]-congˡ identityˡ) +₁∘i₂ ⟩ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁
([ idC , ((f #) +₁ h) # ] ∘ (i₂ ∘ h)) ≈⟨ sym-assoc ⟩ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ ∘[] ⟩
([ idC , ((f #) +₁ h) # ] ∘ i₂) ∘ h ≈⟨ ∘-resp-≈ˡ inject₂ ⟩ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎
((f #) +₁ h) # ∘ h ≈⟨ sym (#-Uniformity {f = ((f #) +₁ idC) ∘ h} {g = (f #) +₁ h} {h = h} ( right : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
begin → (f # +₁ h)# ∘ i₂ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂
(idC +₁ h) ∘ ((f #) +₁ idC) ∘ h ≈⟨ sym-assoc ⟩ right {X} {Y} {f} {h} = begin
(((idC +₁ h) ∘ ((f #) +₁ idC)) ∘ h) ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ (f # +₁ h)# ∘ i₂ ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩
(((idC ∘ (f #)) +₁ (h ∘ idC)) ∘ h) ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ ([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₂ ≈⟨ pullʳ +₁∘i₂ ⟩
(f # +₁ h) ∘ h ∎) [ idC , idC ∘ (((f #) +₁ h) #) ] ∘ i₂ ∘ h ≈⟨ pullˡ inject₂ ⟩
)⟩ (idC ∘ (((f #) +₁ h) #)) ∘ h ≈⟨ (identityˡ ⟩∘⟨refl) ⟩
((((f #) +₁ idC) ∘ h) #) ≈⟨ #-Compositionality ⟩ ((f #) +₁ h) # ∘ h ≈˘⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ h}
(([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂) ≈⟨ ∘-resp-≈ˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = [ i₁ , h ]} ( {g = (f #) +₁ h}
begin {h = h}
(idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ ∘-resp-≈ʳ ∘[] ⟩ (pullˡ (trans (+₁∘+₁) (+₁-cong₂ identityˡ identityʳ)))⟩
(idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘-resp-≈ʳ ([]-congʳ inject₁) ⟩ (((f #) +₁ idC) ∘ h) # ≈⟨ #-Compositionality ⟩
((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]) ≈⟨ ∘[] ⟩ (([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂) ≈⟨ ∘-resp-≈ˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]}
[ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) , (idC +₁ [ i₁ , h ]) ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ sym-assoc sym-assoc ⟩ {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]}
[ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ ∘[]) ⟩ {h = [ i₁ , h ]}
[ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f , ([ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) , (idC +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁))) (∘-resp-≈ˡ ([]-cong₂ sym-assoc sym-assoc)) ⟩ byUni)⟩
[ (idC +₁ i₁) ∘ f , ([ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ i₂) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ inject₂))) ⟩ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂ ≈⟨ pullʳ inject₂ ⟩
[ (idC +₁ i₁) ∘ f , ([ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h ≈˘⟨ inject₂ ⟩∘⟨refl ⟩
[ (idC +₁ i₁) ∘ f , ([ (idC +₁ i₁) ∘ f , i₂ ∘ ([ i₁ , h ] ∘ i₂) ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩ ([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h ≈˘⟨ pushʳ inject₂ ⟩
[ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ []-congʳ (sym (inject₁)) ⟩ [ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ]
[ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ sym ∘[] ⟩ ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂) ≈˘⟨ []-congˡ identityˡ ⟩∘⟨refl ⟩
[ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎) [ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ]
)⟩ ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂) ≈˘⟨ pushˡ #-Fixpoint ⟩
(([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂) ≈⟨ assoc ⟩ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ∎
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ ([ i₁ , h ] ∘ i₂)) ≈⟨ (∘-resp-≈ʳ $ inject₂) ⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h) ≈⟨ sym $ ∘-resp-≈ˡ inject₂ ⟩
(([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h) ≈⟨ assoc ⟩
([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂ ∘ h) ≈⟨ sym (∘-resp-≈ ([]-congˡ identityˡ) inject₂) ⟩
([ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂)) ≈⟨ sym-assoc ⟩
(([ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂) ≈⟨ ∘-resp-≈ˡ (sym #-Fixpoint) ⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂) ∎
-- unguarded elgot-algebras are just Id-guarded Elgot-Algebras
Unguarded↔Id-Guarded : ((ea : Elgot-Algebra) → Guarded-Elgot-Algebra (Id-Algebra (Elgot-Algebra.A ea))) ∧ (∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra)
Unguarded↔Id-Guarded = Unguarded→Id-Guarded , Id-Guarded→Unguarded