⚡️ Proof that rho is natural in X

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

@@ -12,6 +12,7 @@ open import Data.Product using (_,_; Σ; Σ-syntax)
 open import Categories.Functor.Algebra
 open import Categories.Functor.Coalgebra
 open import Categories.Object.Terminal
+open import Categories.NaturalTransformation.Core
 ```
 -->
 
@@ -74,11 +75,28 @@ 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 maybe needs that ρ is natural in X
       ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X}
-      ρ▷ {X} = sym {! coeq-universal  !}
+      ρ▷ {X} = begin 
+        ρ ∘ ▷ ≈⟨ coeq-universal {eq = eq'} ⟩ 
+        coequalize eq' ∘ ρ ≈⟨ ({!   !} ⟩∘⟨refl) ⟩ 
+        coequalize equality ∘ ρ ≈⟨ elimˡ (sym id-coequalize) ⟩ 
+        ρ ∎
         where
-          open Coequalizer (coeqs X) using () renaming (universal to coeq-universal)
+          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₁ π₁ ∎
 
       Ď-Functor : Endofunctor C
       Ď-Functor = record
@@ -127,6 +145,12 @@ We will now show that the following conditions are equivalent:
             where 
               open Coequalizer (coeqs X) using (coequalize; equality) renaming (universal to coeq-universal)
 
+      ρ-natural : NaturalTransformation D-Functor Ď-Functor
+      ρ-natural = ntHelper (record 
+        { η = λ X → ρ {X} 
+        ; commute = λ {X} {Y} f → Coequalizer.universal (coeqs X)
+        })
+
       cond-1 : Set (o ⊔ ℓ ⊔ e)
       cond-1 = ∀ X → preserves D-Functor (coeqs X)
 
@@ -176,9 +200,4 @@ We will now show that the following conditions are equivalent:
                 ρ ∘ extend ι ∘ μ.η (X × N) ≈⟨ pullˡ equality ⟩
                 (ρ ∘ D₁ π₁) ∘ μ.η (X × N) ≈⟨ (pullʳ (sym (μ.commute π₁)) ○ sym-assoc) ⟩
                 (ρ ∘ μ.η X) ∘ D₁ (D₁ π₁) ∎)
-              ▷extend : ∀ {X} {Y} (f : X ⇒ D₀ Y) → ▷ ∘ extend f ≈ extend f ∘ ▷
-              ▷extend {X} {Y} f = {!   !}
-                where
-                  helper₁ : [ f , extend (▷ ∘ f) ] ∘ out ≈ extend f
-                  helper₁ = {!   !}
 ```