diff --git a/src/Algebra/Elgot/Properties.lagda.md b/src/Algebra/Elgot/Properties.lagda.md new file mode 100644 index 0000000..85979f8 --- /dev/null +++ b/src/Algebra/Elgot/Properties.lagda.md @@ -0,0 +1,41 @@ + + +## 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 {! !} {! !} ⟩ + α ∘ ι ∎) + + +``` \ No newline at end of file diff --git a/src/Algebra/ElgotAlgebra.lagda.md b/src/Algebra/ElgotAlgebra.lagda.md index d9234ea..4ec60bc 100644 --- a/src/Algebra/ElgotAlgebra.lagda.md +++ b/src/Algebra/ElgotAlgebra.lagda.md @@ -24,27 +24,31 @@ module Algebra.ElgotAlgebra {o ℓ e} (ambient : Ambient o ℓ e) where ### *Definition 7* Guarded Elgot Algebras ```agda - module _ {F : Endofunctor C} (FA : F-Algebra F) where - record Guarded-Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where - open Functor F public - open F-Algebra FA public - -- iteration operator - field - _# : ∀ {X} → (X ⇒ A + F₀ X) → (X ⇒ A) + record Guarded-Elgot-Algebra-on {F : Endofunctor C} (FA : F-Algebra F) : Set (o ⊔ ℓ ⊔ e) where + open Functor F public + open F-Algebra FA public + -- iteration operator + field + _# : ∀ {X} → (X ⇒ A + F₀ X) → (X ⇒ A) - -- _# properties - field - #-Fixpoint : ∀ {X} {f : X ⇒ A + F₀ X } - → f # ≈ [ idC , α ∘ F₁ (f #) ] ∘ f - #-Uniformity : ∀ {X Y} {f : X ⇒ A + F₀ X} {g : Y ⇒ A + F₀ Y} {h : X ⇒ Y} - → (idC +₁ F₁ h) ∘ f ≈ g ∘ h - → f # ≈ g # ∘ h - #-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₂ - #-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X} - → f ≈ g - → (f #) ≈ (g #) + -- _# properties + field + #-Fixpoint : ∀ {X} {f : X ⇒ A + F₀ X } + → f # ≈ [ idC , α ∘ F₁ (f #) ] ∘ f + #-Uniformity : ∀ {X Y} {f : X ⇒ A + F₀ X} {g : Y ⇒ A + F₀ Y} {h : X ⇒ Y} + → (idC +₁ F₁ h) ∘ f ≈ g ∘ h + → f # ≈ g # ∘ h + #-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₂ + #-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X} + → 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 @@ -136,13 +140,16 @@ Here we give a different Characterization and show that it is equal. where open Functor (idF {C = C}) -- 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 - { _# = _# - ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (sym (∘-resp-≈ˡ ([]-congˡ identityˡ))) - ; #-Uniformity = #-Uniformity - ; #-Compositionality = #-Compositionality - ; #-resp-≈ = #-resp-≈ + { algebra = Id-Algebra A + ; guarded-elgot-algebra-on = record + { _# = _# + ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (sym (∘-resp-≈ˡ ([]-congˡ identityˡ))) + ; #-Uniformity = #-Uniformity + ; #-Compositionality = #-Compositionality + ; #-resp-≈ = #-resp-≈ + } } where open Elgot-Algebra ea @@ -150,7 +157,7 @@ Here we give a different Characterization and show that it is equal. open Equiv -- 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 { A = A ; algebra = record @@ -166,7 +173,7 @@ Here we give a different Characterization and show that it is equal. } } where - open Guarded-Elgot-Algebra gea + open Guarded-Elgot-Algebra-on gea open HomReasoning open Equiv left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} diff --git a/src/Algebra/Search.lagda.md b/src/Algebra/Search.lagda.md new file mode 100644 index 0000000..93135e9 --- /dev/null +++ b/src/Algebra/Search.lagda.md @@ -0,0 +1,29 @@ + +## 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₂ : α ∘ ▷ ≈ α +``` \ No newline at end of file diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index c1e0b46..c022274 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/src/Monad/Instance/Delay.lagda.md @@ -55,11 +55,9 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X + ```agda - module _ (X : Obj) where + module _ {X : Obj} where open Terminal (coalgebras X) using (⊤; !; !-unique) - open F-Coalgebra ⊤ renaming (A to DX) - - D₀ = DX + open F-Coalgebra ⊤ using () renaming (A to DX) public out-≅ : DX ≅ X + DX 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 = out⁻¹ ∘ i₂ + -- convenient notation + ▷ = later + unitlaw : out ∘ now ≈ i₁ 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`: @@ -100,6 +102,12 @@ TODO add diagram ι : X × N ⇒ DX ι = 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)`. @@ -112,7 +120,7 @@ TODO kleisli : KleisliTriple C kleisli = record { F₀ = D₀ - ; unit = λ {X} → now X + ; unit = now ; extend = extend ; identityʳ = identityʳ' ; identityˡ = identityˡ' @@ -124,7 +132,7 @@ TODO open Terminal module _ {X Y : Obj} (f : X ⇒ D₀ Y) where 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 = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y} @@ -132,39 +140,39 @@ TODO !∘i₂ : u (! (coalgebras Y) {A = alg}) ∘ i₂ ≈ idC !∘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 - 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)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] - ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ - [ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) - , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ + ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩ + [ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) + , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩ [ [ (idC +₁ (u (! (coalgebras Y)))) ∘ i₁ - , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) - , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ + , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f) + , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl ⟩ - [ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f) - , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ + [ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out ∘ f) + , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂ (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) 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 (coalgebras Y) (record { f = [ g , idC ] ; commutes = begin - out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩ - [ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩ - [ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂ + out ∘ [ g , idC ] ≈⟨ ∘[] ⟩ + [ out ∘ g , out ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩ + [ [ out ∘ f , i₂ ∘ g ] ∘ out , out ] ≈˘⟨ []-cong₂ (([]-cong₂ (([]-cong₂ refl identityʳ) ⟩∘⟨refl ○ (elimˡ +-η)) refl) ⟩∘⟨refl) refl ⟩ - [ [ [ i₁ , i₂ ∘ idC ] ∘ (out Y ∘ f) - , i₂ ∘ g ] ∘ out X - , out Y ] ≈˘⟨ []-cong₂ + [ [ [ i₁ , i₂ ∘ idC ] ∘ (out ∘ f) + , i₂ ∘ g ] ∘ out + , out ] ≈˘⟨ []-cong₂ (([]-cong₂ (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl) refl) @@ -172,9 +180,9 @@ TODO refl ⟩ [ [ [ i₁ ∘ idC - , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out Y ∘ f) - , i₂ ∘ g ] ∘ out X - , out Y ] ≈˘⟨ []-cong₂ + , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out ∘ f) + , i₂ ∘ g ] ∘ out + , out ] ≈˘⟨ []-cong₂ (([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) (pullʳ inject₁)) @@ -182,16 +190,16 @@ TODO (elimˡ (Functor.identity (Y +-))) ⟩ [ [ [ (idC +₁ [ g , idC ]) ∘ i₁ - , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) - , (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out X - , (idC +₁ idC) ∘ out Y ] ≈˘⟨ []-cong₂ + , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f) + , (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out + , (idC +₁ idC) ∘ out ] ≈˘⟨ []-cong₂ (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl) ((+₁-cong₂ identity² inject₂) ⟩∘⟨refl) ⟩ - [ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) - , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out X - , (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out Y ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩ - [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X - , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out Y ] ≈˘⟨ ∘[] ⟩ + [ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) + , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out + , (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩ + [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out + , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out ] ≈˘⟨ ∘[] ⟩ (idC +₁ [ g , idC ]) ∘ α alg ∎ })) ⟩∘⟨refl ⟩ [ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩ g ∎ @@ -218,38 +226,38 @@ TODO } 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 - extend f ∘ now X ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩∘⟨refl ⟩ - (out⁻¹ Y ∘ out Y ∘ extend f) ∘ now X ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩ - (out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ out X) ∘ now X ≈⟨ pullʳ (pullʳ (unitlaw X)) ⟩ - out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ - out⁻¹ Y ∘ out Y ∘ f ≈⟨ cancelˡ (_≅_.isoˡ (out-≅ Y)) ⟩ + extend f ∘ now ≈⟨ insertˡ (_≅_.isoˡ out-≅) ⟩∘⟨refl ⟩ + (out⁻¹ ∘ out ∘ extend f) ∘ now ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩ + (out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitlaw) ⟩ + out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ + out⁻¹ ∘ out ∘ f ≈⟨ cancelˡ (_≅_.isoˡ out-≅) ⟩ f ∎ - identityˡ' : ∀ {X} → extend (now X) ≈ idC - identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend (now X) ; commutes = begin - out X ∘ extend (now X) ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg (now X)}))) ⟩ - ((idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ - (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) - ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out X ∘ (now X)) , i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw X) ○ inject₁) refl ⟩∘⟨refl ⟩ - (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ - [ (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₁ - , (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ []-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₂ ∘ (extend (now X)) ] ∘ out X ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ - ([ i₁ , i₂ ] ∘ (idC +₁ extend (now X))) ∘ out X ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩ - (idC +₁ extend (now X)) ∘ out X ∎ }) + identityˡ' : ∀ {X} → extend now ≈ idC + identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend now ; commutes = begin + out ∘ extend now ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg now}))) ⟩ + ((idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ α (alg now)) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ + (idC +₁ (u (! (coalgebras X) {A = alg now}))) + ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩ + (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩ + [ (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ + , (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₂ ∘ i₁ ] ∘ out ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩ + [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ ] ∘ out ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩ + [ i₁ ∘ idC , i₂ ∘ (extend now) ] ∘ out ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ + ([ i₁ , i₂ ] ∘ (idC +₁ extend now)) ∘ out ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩ + (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 - out Z ∘ extend h ∘ extend g ≈⟨ pullˡ (extendlaw h) ⟩ - ([ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y) ∘ extend g ≈⟨ pullʳ (extendlaw g) ⟩ - [ out Z ∘ h , i₂ ∘ extend h ] ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈⟨ pullˡ ∘[] ⟩ - [ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g - , [ out Z ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out X ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩ - [ (out Z ∘ extend h) ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out X ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩ - [ out Z ∘ extend h ∘ g , i₂ ∘ extend h ∘ extend g ] ∘ out X ∎) + out ∘ extend h ∘ extend g ≈⟨ pullˡ (extendlaw h) ⟩ + ([ out ∘ h , i₂ ∘ extend h ] ∘ out) ∘ extend g ≈⟨ pullʳ (extendlaw g) ⟩ + [ out ∘ h , i₂ ∘ extend h ] ∘ [ out ∘ g , i₂ ∘ extend g ] ∘ out ≈⟨ pullˡ ∘[] ⟩ + [ [ out ∘ h , i₂ ∘ extend h ] ∘ out ∘ g + , [ out ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩ + [ (out ∘ extend h) ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩ + [ 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} eq = begin diff --git a/src/Monad/Instance/Delay/Quotienting.lagda.md b/src/Monad/Instance/Delay/Quotienting.lagda.md index 3705684..5c21293 100644 --- a/src/Monad/Instance/Delay/Quotienting.lagda.md +++ b/src/Monad/Instance/Delay/Quotienting.lagda.md @@ -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 RMonad kleisli - module _ {X : Obj} (coeq : Coequalizer (extend (ι X)) (D₁ π₁)) where + module _ {X : Obj} (coeq : Coequalizer (extend (ι {X})) (D₁ π₁)) where -- TODO ``` \ No newline at end of file