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

Add search-algebras, start work on elgot-algebra properties

Browse source
This commit is contained in:
Leon Vatthauer 2023-09-12 18:21:26 +02:00
parent 481e1011e5
commit 7f3351dd6c
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
5 changed files with 174 additions and 89 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/Algebra/Elgot/Properties.lagda.md Normal file
View file

@ -0,0 +1,41 @@
<!--
```agda
open import Level
open import Category.Instance.AmbientCategory
open import Categories.Functor
open import Categories.Monad.Relative renaming (Monad to RMonad)
```
-->
## Summary
Some properties of elgot-algebras, namely:
- Every elgot-algebra `(A, α : D₀ A ⇒ A)` satisfies `α (extend ι) ≈ α (D₁ π₁)` **[Lemma 32]**
```agda
module Algebra.Elgot.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Monad.Instance.Delay ambient using (DelayM)
open import Algebra.ElgotAlgebra ambient
open Equiv
open HomReasoning
module _ {D : DelayM} (algebra : Guarded-Elgot-Algebra (DelayM.functor D)) where
open DelayM D
open Functor functor renaming (F₁ to D₁)
open RMonad kleisli
open Guarded-Elgot-Algebra algebra
commutes : α ∘ extend ι ≈ α ∘ (D₁ π₁)
commutes = {! !}
where
α∘ι : α ∘ ι ≈ π₁
α∘ι = sym (begin
π₁ ≈⟨ unique {f = idC} {g = idC} (sym project₁) (sym project₁) ⟩
universal idC idC ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
universal {! !} {! !} ≈˘⟨ unique {! !} {! !} ⟩
α ∘ ι ∎)
```

17
src/Algebra/ElgotAlgebra.lagda.md
View file

@ -24,8 +24,7 @@ module Algebra.ElgotAlgebra {o ℓ e} (ambient : Ambient o ℓ e) where
### *Definition 7* Guarded Elgot Algebras ### *Definition 7* Guarded Elgot Algebras
```agda ```agda
module _ {F : Endofunctor C} (FA : F-Algebra F) where record Guarded-Elgot-Algebra-on {F : Endofunctor C} (FA : F-Algebra F) : 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
@ -45,6 +44,11 @@ module Algebra.ElgotAlgebra {o ℓ e} (ambient : Ambient o ℓ e) where
→ f ≈ g → f ≈ g
→ (f #) ≈ (g #) → (f #) ≈ (g #)
record Guarded-Elgot-Algebra (F : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
field
algebra : F-Algebra F
guarded-elgot-algebra-on : Guarded-Elgot-Algebra-on algebra
open Guarded-Elgot-Algebra-on guarded-elgot-algebra-on public
``` ```
### *Proposition 10* Unguarded Elgot Algebras ### *Proposition 10* Unguarded Elgot Algebras
@ -136,21 +140,24 @@ Here we give a different Characterization and show that it is equal.
where open Functor (idF {C = C}) where open Functor (idF {C = C})
-- constructing an Id-Guarded Elgot-Algebra from an unguarded one -- constructing an Id-Guarded Elgot-Algebra from an unguarded one
Unguarded→Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra (Id-Algebra (Elgot-Algebra.A EA)) Unguarded→Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra idF
Unguarded→Id-Guarded ea = record Unguarded→Id-Guarded ea = record
{ algebra = Id-Algebra A
; guarded-elgot-algebra-on = record
{ _# = _# { _# = _#
; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (sym (∘-resp-≈ˡ ([]-congˡ identityˡ))) ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (sym (∘-resp-≈ˡ ([]-congˡ identityˡ)))
; #-Uniformity = #-Uniformity ; #-Uniformity = #-Uniformity
; #-Compositionality = #-Compositionality ; #-Compositionality = #-Compositionality
; #-resp-≈ = #-resp-≈ ; #-resp-≈ = #-resp-≈
} }
}
where where
open Elgot-Algebra ea open Elgot-Algebra ea
open HomReasoning open HomReasoning
open Equiv open Equiv
-- constructing an unguarded Elgot-Algebra from an Id-Guarded one -- constructing an unguarded Elgot-Algebra from an Id-Guarded one
Id-Guarded→Unguarded : ∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra Id-Guarded→Unguarded : ∀ {A} → Guarded-Elgot-Algebra-on (Id-Algebra A) → Elgot-Algebra
Id-Guarded→Unguarded gea = record Id-Guarded→Unguarded gea = record
{ A = A { A = A
; algebra = record ; algebra = record
@ -166,7 +173,7 @@ Here we give a different Characterization and show that it is equal.
} }
} }
where where
open Guarded-Elgot-Algebra gea open Guarded-Elgot-Algebra-on gea
open HomReasoning open HomReasoning
open Equiv open Equiv
left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}

29
src/Algebra/Search.lagda.md Normal file
View file

@ -0,0 +1,29 @@
<!--
```agda
open import Level
open import Category.Instance.AmbientCategory using (Ambient)
open import Categories.Functor.Algebra
```
-->
## Summary
A *D-Algebra* `(A, α : D₀ A ⇒ A)` is called a *search-algebra* if it satiesfies
- α now ≈ id
- α ▷ ≈ α
## Code
```agda
module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Monad.Instance.Delay ambient using (DelayM)
module _ (D : DelayM) where
open DelayM D
record IsSearchAlgebra (algebra : F-Algebra functor) : Set e where
open F-Algebra algebra using (A; α)
field
identity₁ : α ∘ now ≈ idC
identity₂ : α ∘ ▷ ≈ α
```

130
src/Monad/Instance/Delay.lagda.md
View file

@ -55,11 +55,9 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X +
```agda ```agda
module _ (X : Obj) where module _ {X : Obj} where
open Terminal (coalgebras X) using (⊤; !; !-unique) open Terminal (coalgebras X) using (⊤; !; !-unique)
open F-Coalgebra ⊤ renaming (A to DX) open F-Coalgebra ⊤ using () renaming (A to DX) public
D₀ = DX
out-≅ : DX ≅ X + DX out-≅ : DX ≅ X + DX
out-≅ = colambek {F = X +- } (coalgebras X) out-≅ = colambek {F = X +- } (coalgebras X)
@ -73,8 +71,12 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X +
later : DX ⇒ DX later : DX ⇒ DX
later = out⁻¹ ∘ i₂ later = out⁻¹ ∘ i₂
-- convenient notation
▷ = later
unitlaw : out ∘ now ≈ i₁ unitlaw : out ∘ now ≈ i₁
unitlaw = cancelˡ (_≅_.isoʳ out-≅) unitlaw = cancelˡ (_≅_.isoʳ out-≅)
``` ```
Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use our terminal coalgebras to get a *coiteration operator* `coit`: Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use our terminal coalgebras to get a *coiteration operator* `coit`:
@ -100,6 +102,12 @@ TODO add diagram
ι : X × N ⇒ DX ι : X × N ⇒ DX
ι = u (! {A = record { A = X × N ; α = _≅_.from iso }}) ι = u (! {A = record { A = X × N ; α = _≅_.from iso }})
```
Make `DX` conveniently accessible
```agda
D₀ : Obj → Obj
D₀ X = DX {X}
``` ```
With these definitions at hand, we can now indeed construct a monad (in extension form) as the triple `(F₀, unit, extend)`. With these definitions at hand, we can now indeed construct a monad (in extension form) as the triple `(F₀, unit, extend)`.
@ -112,7 +120,7 @@ TODO
kleisli : KleisliTriple C kleisli : KleisliTriple C
kleisli = record kleisli = record
{ F₀ = D₀ { F₀ = D₀
; unit = λ {X} → now X ; unit = now
; extend = extend ; extend = extend
; identityʳ = identityʳ' ; identityʳ = identityʳ'
; identityˡ = identityˡ' ; identityˡ = identityˡ'
@ -124,7 +132,7 @@ TODO
open Terminal open Terminal
module _ {X Y : Obj} (f : X ⇒ D₀ Y) where module _ {X Y : Obj} (f : X ⇒ D₀ Y) where
alg : F-Coalgebra (Y +-) alg : F-Coalgebra (Y +-)
alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] } alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out , (idC +₁ i₂) ∘ out ] }
extend : D₀ X ⇒ D₀ Y extend : D₀ X ⇒ D₀ Y
extend = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} extend = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y}
@ -132,39 +140,39 @@ TODO
!∘i₂ : u (! (coalgebras Y) {A = alg}) ∘ i₂ ≈ idC !∘i₂ : u (! (coalgebras Y) {A = alg}) ∘ i₂ ≈ idC
!∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (Y +-) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] ) !∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (Y +-) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] )
extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X extendlaw : out ∘ extend ≈ [ out ∘ f , i₂ ∘ extend ] ∘ out
extendlaw = begin extendlaw = begin
out Y ∘ extend ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩ out ∘ extend ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩
((idC +₁ (u (! (coalgebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ ((idC +₁ (u (! (coalgebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
(idC +₁ (u (! (coalgebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] (idC +₁ (u (! (coalgebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ]
∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
[ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) [ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f)
, (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
[ [ (idC +₁ (u (! (coalgebras Y)))) ∘ i₁ [ [ (idC +₁ (u (! (coalgebras Y)))) ∘ i₁
, (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f)
, (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂
(([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl)
refl) ⟩∘⟨refl ⟩ refl) ⟩∘⟨refl ⟩
[ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f) [ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out ∘ f)
, (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂
(elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η))
assoc) ⟩∘⟨refl ⟩ assoc) ⟩∘⟨refl ⟩
[ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎ [ out ∘ f , i₂ ∘ extend ] ∘ out ∎
extend-unique : (g : D₀ X ⇒ D₀ Y) → (out Y ∘ g ≈ [ out Y ∘ f , i₂ ∘ g ] ∘ out X) → extend ≈ g extend-unique : (g : D₀ X ⇒ D₀ Y) → (out ∘ g ≈ [ out ∘ f , i₂ ∘ g ] ∘ out) → extend ≈ g
extend-unique g g-commutes = begin extend-unique g g-commutes = begin
extend ≈⟨ (!-unique (coalgebras Y) (record { f = [ g , idC ] ; commutes = begin extend ≈⟨ (!-unique (coalgebras Y) (record { f = [ g , idC ] ; commutes = begin
out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩ out ∘ [ g , idC ] ≈⟨ ∘[] ⟩
[ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩ [ out ∘ g , out ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩
[ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ [ [ out ∘ f , i₂ ∘ g ] ∘ out , out ] ≈˘⟨ []-cong₂
(([]-cong₂ (([]-cong₂
(([]-cong₂ refl identityʳ) ⟩∘⟨refl ○ (elimˡ +-η)) (([]-cong₂ refl identityʳ) ⟩∘⟨refl ○ (elimˡ +-η))
refl) refl)
⟩∘⟨refl) ⟩∘⟨refl)
refl ⟩ refl ⟩
[ [ [ i₁ , i₂ ∘ idC ] ∘ (out Y ∘ f) [ [ [ i₁ , i₂ ∘ idC ] ∘ (out ∘ f)
, i₂ ∘ g ] ∘ out X , i₂ ∘ g ] ∘ out
, out Y ] ≈˘⟨ []-cong₂ , out ] ≈˘⟨ []-cong₂
(([]-cong₂ (([]-cong₂
(([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl) (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl)
refl) refl)
@ -172,9 +180,9 @@ TODO
refl refl
⟩ ⟩
[ [ [ i₁ ∘ idC [ [ [ i₁ ∘ idC
, (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out Y ∘ f) , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out ∘ f)
, i₂ ∘ g ] ∘ out X , i₂ ∘ g ] ∘ out
, out Y ] ≈˘⟨ []-cong₂ , out ] ≈˘⟨ []-cong₂
(([]-cong₂ (([]-cong₂
(([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl)
(pullʳ inject₁)) (pullʳ inject₁))
@ -182,16 +190,16 @@ TODO
(elimˡ (Functor.identity (Y +-))) (elimˡ (Functor.identity (Y +-)))
⟩ ⟩
[ [ [ (idC +₁ [ g , idC ]) ∘ i₁ [ [ [ (idC +₁ [ g , idC ]) ∘ i₁
, (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f)
, (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out X , (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out
, (idC +₁ idC) ∘ out Y ] ≈˘⟨ []-cong₂ , (idC +₁ idC) ∘ out ] ≈˘⟨ []-cong₂
(([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl) (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl)
((+₁-cong₂ identity² inject₂) ⟩∘⟨refl) ⟩ ((+₁-cong₂ identity² inject₂) ⟩∘⟨refl) ⟩
[ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) [ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f)
, (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out X , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out
, (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out Y ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩ , (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩
[ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out
, (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out Y ] ≈˘⟨ ∘[] ⟩ , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out ] ≈˘⟨ ∘[] ⟩
(idC +₁ [ g , idC ]) ∘ α alg ∎ })) ⟩∘⟨refl ⟩ (idC +₁ [ g , idC ]) ∘ α alg ∎ })) ⟩∘⟨refl ⟩
[ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩ [ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩
g ∎ g ∎
@ -218,38 +226,38 @@ TODO
} }
where open Functor (Y +-) using (identity) where open Functor (Y +-) using (identity)
identityʳ' : ∀ {X} {Y} {f} → extend f ∘ now X ≈ f identityʳ' : ∀ {X Y : Obj} {f : X ⇒ D₀ Y} → extend f ∘ now {X} ≈ f
identityʳ' {X} {Y} {f} = begin identityʳ' {X} {Y} {f} = begin
extend f ∘ now X ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩∘⟨refl ⟩ extend f ∘ now ≈⟨ insertˡ (_≅_.isoˡ out-≅) ⟩∘⟨refl ⟩
(out⁻¹ Y ∘ out Y ∘ extend f) ∘ now X ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩ (out⁻¹ ∘ out ∘ extend f) ∘ now ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩
(out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ out X) ∘ now X ≈⟨ pullʳ (pullʳ (unitlaw X)) ⟩ (out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitlaw) ⟩
out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩
out⁻¹ Y ∘ out Y ∘ f ≈⟨ cancelˡ (_≅_.isoˡ (out-≅ Y)) ⟩ out⁻¹ ∘ out ∘ f ≈⟨ cancelˡ (_≅_.isoˡ out-≅) ⟩
f ∎ f ∎
identityˡ' : ∀ {X} → extend (now X) ≈ idC identityˡ' : ∀ {X} → extend now ≈ idC
identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend (now X) ; commutes = begin identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend now ; commutes = begin
out X ∘ extend (now X) ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg (now X)}))) ⟩ out ∘ extend now ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg now}))) ⟩
((idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ ((idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ α (alg now)) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
(idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) (idC +₁ (u (! (coalgebras X) {A = alg now})))
∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out X ∘ (now X)) , i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw X) ○ inject₁) refl ⟩∘⟨refl ⟩ ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩
(idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
[ (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₁ [ (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₁
, (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩ , (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₂ ∘ i₁ ] ∘ out ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩
[ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ ] ∘ out ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩
[ i₁ ∘ idC , i₂ ∘ (extend (now X)) ] ∘ out X ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ [ i₁ ∘ idC , i₂ ∘ (extend now) ] ∘ out ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
([ i₁ , i₂ ] ∘ (idC +₁ extend (now X))) ∘ out X ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩ ([ i₁ , i₂ ] ∘ (idC +₁ extend now)) ∘ out ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
(idC +₁ extend (now X)) ∘ out X ∎ }) (idC +₁ extend now) ∘ out ∎ })
assoc' : ∀ {X} {Y} {Z} {g} {h} → extend (extend h ∘ g) ≈ extend h ∘ extend g assoc' : ∀ {X Y Z : Obj} {g : X ⇒ D₀ Y} {h : Y ⇒ D₀ Z} → extend (extend h ∘ g) ≈ extend h ∘ extend g
assoc' {X} {Y} {Z} {g} {h} = extend-unique (extend h ∘ g) (extend h ∘ extend g) (begin assoc' {X} {Y} {Z} {g} {h} = extend-unique (extend h ∘ g) (extend h ∘ extend g) (begin
out Z ∘ extend h ∘ extend g ≈⟨ pullˡ (extendlaw h) ⟩ out ∘ extend h ∘ extend g ≈⟨ pullˡ (extendlaw h) ⟩
([ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y) ∘ extend g ≈⟨ pullʳ (extendlaw g) ⟩ ([ out ∘ h , i₂ ∘ extend h ] ∘ out) ∘ extend g ≈⟨ pullʳ (extendlaw g) ⟩
[ out Z ∘ h , i₂ ∘ extend h ] ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ [ out ∘ h , i₂ ∘ extend h ] ∘ [ out ∘ g , i₂ ∘ extend g ] ∘ out ≈⟨ pullˡ ∘[] ⟩
[ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g [ [ out ∘ h , i₂ ∘ extend h ] ∘ out ∘ g
, [ out Z ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out X ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩ , [ out ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩
[ (out Z ∘ extend h) ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out X ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩ [ (out ∘ extend h) ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩
[ out Z ∘ extend h ∘ g , i₂ ∘ extend h ∘ extend g ] ∘ out X ∎) [ out ∘ extend h ∘ g , i₂ ∘ extend h ∘ extend g ] ∘ out ∎)
extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g
extend-≈' {X} {Y} {f} {g} eq = begin extend-≈' {X} {Y} {f} {g} eq = begin

2
src/Monad/Instance/Delay/Quotienting.lagda.md
View file

@ -22,6 +22,6 @@ module Monad.Instance.Delay.Quotienting {o ℓ e} (ambient : Ambient o ℓ e) wh
open Functor functor using () renaming (F₁ to D₁) open Functor functor using () renaming (F₁ to D₁)
open RMonad kleisli open RMonad kleisli
module _ {X : Obj} (coeq : Coequalizer (extend (ι X)) (D₁ π₁)) where module _ {X : Obj} (coeq : Coequalizer (extend (ι {X})) (D₁ π₁)) where
-- TODO -- TODO
``` ```