Finished extend congruence proof

src/FinalCoalgebras.lagda.md

@@ -0,0 +1,41 @@
+```agda
+open import Level
+open import Categories.Category
+open import Categories.Functor
+import Categories.Morphism as M
+import Categories.Morphism.Reasoning as MR
+
+module FinalCoalgebras {o ℓ e} {C : Category o ℓ e} (F : Endofunctor C) where
+open Category C renaming (id to idC)
+open import Categories.Object.Terminal
+open import Categories.Functor.Coalgebra
+open import Categories.Category.Construction.F-Coalgebras
+open Functor F
+open MR C
+open HomReasoning
+open Equiv
+
+lemma : ∀ {X} → {f g : X ⇒ F₀ X} → f ≈ g → (terminal : Terminal (F-Coalgebras F)) → F-Coalgebra-Morphism.f (Terminal.! terminal {A = (to-Coalgebra f)}) ≈ F-Coalgebra-Morphism.f (Terminal.! terminal {A = (to-Coalgebra g)})
+lemma {X} {f} {g} eq terminal = begin 
+  F-Coalgebra-Morphism.f (Terminal.! terminal) ≈⟨ Terminal.!-unique terminal (record 
+    { f = F-Coalgebra-Morphism.f (Terminal.! terminal {A = (to-Coalgebra g)}) ∘ F-Coalgebra-Morphism.f from 
+    ; commutes = begin 
+      F-Coalgebra.α (Terminal.⊤ terminal) ∘ F-Coalgebra-Morphism.f (IsTerminal.! (Terminal.⊤-is-terminal terminal)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ○ F-Coalgebra-Morphism.commutes (Terminal.! terminal) ⟩ 
+      F₁ (F-Coalgebra-Morphism.f (Terminal.! terminal)) ∘ g ≈⟨ refl⟩∘⟨ ⟺ eq ⟩
+      F₁ (F-Coalgebra-Morphism.f (Terminal.! terminal)) ∘ f ≈˘⟨ F-resp-≈ identityʳ ⟩∘⟨refl ⟩
+      F₁ (F-Coalgebra-Morphism.f (Terminal.! terminal) ∘ idC) ∘ f ∎ 
+    }) ⟩ 
+  F-Coalgebra-Morphism.f (Terminal.! terminal) ∘ idC ≈⟨ identityʳ ⟩
+  F-Coalgebra-Morphism.f (Terminal.! terminal) ∎
+  where
+    eq' : M._≅_ (F-Coalgebras F) (to-Coalgebra f) (to-Coalgebra g)
+    eq' = record 
+      { from = record { f = idC ; commutes = id-comm ○ ⟺ identity ⟩∘⟨ ⟺ eq } 
+      ; to = record { f = idC ; commutes = id-comm ○ ⟺ identity ⟩∘⟨ eq } 
+      ; iso = record 
+        { isoˡ = identity² 
+        ; isoʳ = identity² 
+        } 
+      }
+    open M._≅_ eq'
+```

src/Monad/Instance/Delay.lagda.md

@@ -20,6 +20,7 @@ open import Categories.Functor.Algebra
 open import Categories.Monad.Construction.Kleisli
 open import Categories.Category.Construction.F-Coalgebras
 open import Categories.NaturalTransformation
+open import FinalCoalgebras
 import Categories.Morphism as M
 import Categories.Morphism.Reasoning as MR
 ```
@@ -92,7 +93,6 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
 
         coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f
         coit-commutes f = F-Coalgebra-Morphism.commutes (! {A = record { A = Y ; α = f }})
-
     monad : Monad C
     monad = Kleisli⇒Monad C (record
       { F₀ = D₀ 
@@ -119,31 +119,14 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
         (idC +₁ extend (now X)) ∘ out X                                                                                    ∎ })
       ; assoc = {!   !}
       ; sym-assoc = {!   !}
-      ; extend-≈ = λ {X} {Y} {f} {g} eq → {!   !}
+      ; extend-≈ = λ {X} {Y} {f} {g} eq → begin 
-      
+          F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (Terminal.!-unique (algebras Y) (record { f = (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g }) ∘ idC) ; commutes = begin 
-        -- begin 
+            F-Coalgebra.α (Terminal.⊤ (algebras Y)) ∘ F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ 
-        --   extend f ≈⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend f ; commutes = F-Coalgebra-Morphism.commutes {!   !} })) ⟩ 
+            F-Coalgebra.α (Terminal.⊤ (algebras Y)) ∘ F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ≈⟨ F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y)) ⟩ 
-        --   F-Coalgebra-Morphism.f ((Terminal.! (algebras Y) {A = alg' {X} {Y}})) ≈˘⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend g ; commutes = {!   !} })) ⟩
+            Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y))) ∘ F-Coalgebra.α (alg g) ≈˘⟨ (Functor.F-resp-≈ (delayF Y) identityʳ) ⟩∘⟨ (αf≈αg eq) ⟩ 
-        --   extend g ∎
+            Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ∘ idC) ∘ F-Coalgebra.α (alg f) ∎ })) ⟩∘⟨refl ⟩ 
-      
+          (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩
-        -- let 
+          extend g ∎
-        --   h : F-Coalgebra-Morphism (alg f) (alg g)
-        --   h = record { f = idC ; commutes = begin 
-        --     F-Coalgebra.α (alg g) ∘ idC ≈⟨ id-comm ⟩ 
-        --     idC ∘ F-Coalgebra.α (alg g) ≈⟨ refl⟩∘⟨ []-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (sym eq))) refl) ⟩∘⟨refl) refl ⟩ 
-        --     idC ∘ F-Coalgebra.α (alg f) ≈˘⟨ ([]-cong₂ identityʳ identityʳ ○ +-η) ⟩∘⟨refl ⟩
-        --     (idC +₁ idC) ∘ F-Coalgebra.α (alg f) ∎ }
-        --   x : F-Coalgebra-Morphism (alg f) (Terminal.⊤ (algebras Y))
-        --   x = (F-Coalgebras (delayF Y)) [ Terminal.! (algebras Y) ∘ h ]
-        -- in Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = {!   !} } ⟩∘⟨refl
-        
-        -- extend f ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩ 
-        -- out⁻¹ Y ∘ out Y ∘ extend f ≈⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg f})) ⟩
-        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ ((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y) {A = alg f}} {g = Terminal.! (algebras Y) {A = alg f}}) ⟩∘⟨ ([]-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ eq)) refl) ⟩∘⟨refl) refl)) ⟩∘⟨refl) ⟩
-        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ (((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = record { f = F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ; commutes = {!   !} }})) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
-        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈˘⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg g})) ⟩
-        -- out⁻¹ Y ∘ out Y ∘ extend g ≈˘⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩
-        -- extend g ∎
       })
       where
         alg' : ∀ {X Y} → F-Coalgebra (delayF Y)
@@ -169,6 +152,25 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
             [ [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₂ ] ∘ (out Y ∘ f) 
             , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₁ ] ∘ out X                                         ≈⟨ ([]-cong₂ (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) assoc) ⟩∘⟨refl ⟩
             [ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎ 
+        αf≈αg : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → F-Coalgebra.α (alg f) ≈ F-Coalgebra.α (alg g)
+        αf≈αg {X} {Y} {f} {g} eq = []-cong₂ ([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ eq) refl ⟩∘⟨refl) refl
+        alg-f≈alg-g : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → M._≅_ (F-Coalgebras (delayF Y)) (alg f) (alg g)
+        alg-f≈alg-g {X} {Y} {f} {g} eq = record 
+          { from = record { f = idC ; commutes = begin 
+            F-Coalgebra.α (alg g) ∘ idC ≈⟨ identityʳ ⟩ 
+            F-Coalgebra.α (alg g) ≈⟨ ⟺ (αf≈αg eq) ⟩ 
+            F-Coalgebra.α (alg f) ≈˘⟨ elimˡ (Functor.identity (delayF Y)) ⟩ 
+            Functor.F₁ (delayF Y) idC ∘ F-Coalgebra.α (alg f) ∎ } 
+          ; to = record { f = idC ; commutes = begin 
+            F-Coalgebra.α (alg f) ∘ idC ≈⟨ identityʳ ⟩ 
+            F-Coalgebra.α (alg f) ≈⟨ αf≈αg eq ⟩ 
+            F-Coalgebra.α (alg g) ≈˘⟨ elimˡ (Functor.identity (delayF Y)) ⟩ 
+            Functor.F₁ (delayF Y) idC ∘ F-Coalgebra.α (alg g) ∎ } 
+          ; iso = record 
+            { isoˡ = identity² 
+            ; isoʳ = identity² 
+            } 
+          }
 ```
 
 ### Old definitions: