⚡️ Finished many helper lemmas and a small proof

src/Monad/Instance/Delay.lagda.md

@@ -71,6 +71,9 @@ We then use Lambek's Lemma to gain an isomorphism `D X ≅ X + D X`, whose inver
 
       unitlaw : out ∘ now ≈ i₁
       unitlaw = cancelˡ (_≅_.isoʳ out-≅)
+
+      laterlaw : out ∘ later ≈ i₂
+      laterlaw = cancelˡ (_≅_.isoʳ out-≅)
 ```
 
 Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the final coalgebras to get a *coiteration operator* `coit`:

src/Monad/Instance/Delay/Quotienting.lagda.md

@@ -57,7 +57,7 @@ We will now show that the following conditions are equivalent:
     open DelayM D renaming (functor to D-Functor; monad to D-Monad; kleisli to D-Kleisli)
 
     open Functor D-Functor using () renaming (F₁ to D₁; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈; identity to D-identity)
-    open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
+    open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ; identityˡ to k-identityˡ)
     open Monad D-Monad using () renaming (assoc to M-assoc; identityʳ to M-identityʳ)
     open HomReasoning
     open M C
@@ -75,28 +75,67 @@ We will now show that the following conditions are equivalent:
       ρ-epi : ∀ {X} → Epi (ρ {X})
       ρ-epi {X} = Coequalizer⇒Epi (coeqs X)
 
-      -- TODO this belongs in different module
-      ▷extend : ∀ {X} {Y} (f : X ⇒ D₀ Y) → ▷ ∘ extend f ≈ extend f ∘ ▷
-      ▷extend {X} {Y} f = {!   !}
-        where
-          helper₁ : [ f , extend (▷ ∘ f) ] ∘ out ≈ extend f
-          helper₁ = {!   !}
+      -- TODO this belongs in a different module
+      module _ {X Y} (f : X ⇒ D₀ Y) where
+        private
+            helper : out ∘ [ f , extend (▷ ∘ f) ] ∘ out ≈ [ out ∘ f , i₂ ∘ [ f , extend (▷ ∘ f) ] ∘ out ] ∘ out
+            helper = pullˡ ∘[] ○ (([]-cong₂ refl (extendlaw (▷ ∘ f) ○ ((([]-cong₂ (pullˡ laterlaw) refl) ⟩∘⟨refl) ○ sym (pullˡ ∘[])))) ⟩∘⟨refl)
+            helper₁ : [ f , extend (▷ ∘ f) ] ∘ out ≈ extend f
+            helper₁ = sym (extend'-unique f ([ f , extend (▷ ∘ f) ] ∘ out) helper)
+
+        ▷∘extendˡ : ▷ ∘ extend f ≈ extend (▷ ∘ f)
+        ▷∘extendˡ = sym (begin 
+          extend (▷ ∘ f) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
+          (out⁻¹ ∘ out) ∘ extend (▷ ∘ f) ≈⟨ pullʳ (extendlaw (▷ ∘ f)) ⟩
+          out⁻¹ ∘ [ out ∘ ▷ ∘ f , i₂ ∘ extend (▷ ∘ f) ] ∘ out ≈⟨ (refl⟩∘⟨ (([]-cong₂ (pullˡ laterlaw) refl) ○ (sym ∘[])) ⟩∘⟨refl) ⟩
+          out⁻¹ ∘ (i₂ ∘ [ f , extend (▷ ∘ f) ]) ∘ out ≈⟨ (refl⟩∘⟨ (pullʳ helper₁)) ⟩
+          out⁻¹ ∘ i₂ ∘ extend f ≈⟨ sym-assoc ⟩
+          ▷ ∘ extend f ∎)
+
+        ▷∘extend-comm : ▷ ∘ extend f ≈ extend f ∘ ▷
+        ▷∘extend-comm = sym (begin 
+          extend f ∘ ▷ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
+          (out⁻¹ ∘ out) ∘ extend f ∘ ▷ ≈⟨ pullʳ (pullˡ (extendlaw f)) ⟩ 
+          out⁻¹ ∘ ([ out ∘ f , i₂ ∘ extend f ] ∘ out) ∘ ▷ ≈⟨ (refl⟩∘⟨ pullʳ laterlaw) ⟩ 
+          out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ i₂ ≈⟨ (refl⟩∘⟨ inject₂) ○ sym-assoc ⟩ 
+          ▷ ∘ extend f ∎)
+
+        ▷∘extendʳ : extend f ∘ ▷ ≈ extend (▷ ∘ f)
+        ▷∘extendʳ = (sym ▷∘extend-comm) ○ ▷∘extendˡ
+
+
 
-      -- TODO maybe needs that ρ is natural in X
       ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X}
-      ρ▷ {X} = begin 
-        ρ ∘ ▷ ≈⟨ coeq-universal {eq = eq'} ⟩ 
-        coequalize eq' ∘ ρ ≈⟨ ({!   !} ⟩∘⟨refl) ⟩ 
-        coequalize equality ∘ ρ ≈⟨ elimˡ (sym id-coequalize) ⟩ 
-        ρ ∎
+      ρ▷ {X} = sym (begin 
+        ρ ≈⟨ introʳ intro-helper ⟩ 
+        ρ ∘ D₁ π₁ ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullˡ (sym equality) ⟩ 
+        (ρ ∘ extend ι) ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (sym k-assoc) ⟩ 
+        ρ ∘ extend (extend ι ∘ now ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩) ≈⟨ (refl⟩∘⟨ extend-≈ (pullˡ k-identityʳ)) ⟩ 
+        ρ ∘ extend (ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩) ≈⟨ (refl⟩∘⟨ extend-≈ helper) ⟩ 
+        ρ ∘ extend (▷ ∘ now) ≈⟨ (refl⟩∘⟨ sym (▷∘extendʳ now)) ⟩ 
+        ρ ∘ extend now ∘ ▷ ≈⟨ elim-center k-identityˡ ⟩ 
+        ρ ∘ ▷ ∎)
         where
-          open Coequalizer (coeqs X) using (equality; coequalize; id-coequalize) renaming (universal to coeq-universal; unique to coeq-unique; unique′ to coeq-unique′)
-          eq' = begin 
-            (ρ ∘ ▷) ∘ extend ι ≈⟨ pullʳ (▷extend ι) ⟩ 
-            ρ ∘ extend ι ∘ ▷ ≈⟨ pullˡ equality ⟩
-            (ρ ∘ D₁ π₁) ∘ ▷ ≈⟨ assoc ⟩
-            ρ ∘ D₁ π₁ ∘ ▷ ≈⟨ sym (pullʳ (▷extend (now ∘ π₁))) ⟩
-            (ρ ∘ ▷) ∘ D₁ π₁ ∎
+          open Coequalizer (coeqs X) using (equality; coequalize; id-coequalize; coequalize-resp-≈) renaming (universal to coeq-universal; unique to coeq-unique; unique′ to coeq-unique′)
+          intro-helper : D₁ π₁ ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ idC
+          intro-helper = sym D-homomorphism ○ D-resp-≈ project₁ ○ D-identity
+          helper : ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ ▷ ∘ now
+          helper = begin 
+            ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
+            (out⁻¹ ∘ out) ∘ ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (pullˡ (coalg-commutes ((Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})))) ⟩
+            out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl)) ⟩
+            out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (idC ⁂ s) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₂ ⟩∘⟨refl) ⟩
+            out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (_≅_.to nno-iso ∘ i₂) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (cancelˡ (_≅_.isoʳ nno-iso))))) ⟩
+            out⁻¹ ∘ (idC +₁ ι) ∘ i₂ ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ pullˡ +₁∘i₂) ⟩
+            out⁻¹ ∘ (i₂ ∘ ι) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₁) ⟩
+            out⁻¹ ∘ (i₂ ∘ ι) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ intro-center (_≅_.isoˡ out-≅) ⟩∘⟨refl) ⟩
+            out⁻¹ ∘ (i₂ ∘ (out⁻¹ ∘ out) ∘ ι) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ pullʳ (coalg-commutes ((Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})))) ⟩∘⟨refl) ⟩
+            out⁻¹ ∘ (i₂ ∘ out⁻¹ ∘ (idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (pullʳ (cancelʳ (_≅_.isoʳ nno-iso)))))) ⟩
+            out⁻¹ ∘ i₂ ∘ (out⁻¹ ∘ (idC +₁ ι)) ∘ i₁ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pullʳ +₁∘i₁) ⟩
+            out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ∘ idC ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ) ⟩
+            out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ≈⟨ ((refl⟩∘⟨ sym-assoc) ○ assoc²'') ⟩
+            ▷ ∘ now ∎
+-- ⁂ ○
 
       Ď-Functor : Endofunctor C
       Ď-Functor = record
@@ -178,10 +217,11 @@ We will now show that the following conditions are equivalent:
               ρ ≈⟨ sym identityˡ ⟩
               idC ∘ ρ ∎) 
             ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ ▷) α' (begin 
-              (α' ∘ ▷) ∘ D₁ ρ ≈⟨ {!   !} ⟩ 
-              {!   !} ≈⟨ {!   !} ⟩
-              {!   !} ≈⟨ {!   !} ⟩
-              {!   !} ≈⟨ {!   !} ⟩
+              (α' ∘ ▷) ∘ D₁ ρ ≈⟨ pullʳ (▷∘extend-comm (now ∘ ρ)) ⟩ 
+              α' ∘ D₁ ρ ∘ ▷ ≈⟨ pullˡ (sym D-universal) ⟩
+              (ρ ∘ μ.η X) ∘ ▷ ≈⟨ pullʳ (sym (▷∘extend-comm idC)) ⟩
+              ρ ∘ ▷ ∘ extend idC ≈⟨ pullˡ ρ▷ ⟩
+              ρ ∘ extend idC ≈⟨ D-universal ⟩
               α' ∘ D₁ ρ ∎) 
             }
             where