⚡️ Proof that quotiented D is a functor

src/Algebra/Search.lagda.md

@@ -21,9 +21,17 @@ module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where
   module _ (D : DelayM) where
     open DelayM D
 
-    record IsSearchAlgebra (algebra : F-Algebra functor) : Set e where
+    record Search-Algebra-on (A : Obj) : Set (ℓ ⊔ e) where
-      open F-Algebra algebra using (A; α)
+      field
+        α : F-Algebra-on functor A
+
       field
         identity₁ : α ∘ now ≈ idC
         identity₂ : α ∘ ▷ ≈ α 
+
+    record Search-Algebra : Set (o ⊔ ℓ ⊔ e) where
+      field
+        A : Obj
+        search-algebra-on : Search-Algebra-on A
+      open Search-Algebra-on search-algebra-on public
 ```

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

@@ -5,8 +5,13 @@ open import Level
 
 open import Categories.Functor
 open import Category.Instance.AmbientCategory using (Ambient)
+open import Categories.Monad
 open import Categories.Monad.Construction.Kleisli
 open import Categories.Monad.Relative renaming (Monad to RMonad)
+open import Data.Product using (_,_; Σ; Σ-syntax)
+open import Categories.Functor.Algebra
+open import Categories.Functor.Coalgebra
+open import Categories.Object.Terminal
 ```
 -->
 
@@ -15,6 +20,8 @@ module Monad.Instance.Delay.Quotienting {o ℓ e} (ambient : Ambient o ℓ e) wh
   open Ambient ambient
   open import Categories.Diagram.Coequalizer C 
   open import Monad.Instance.Delay ambient
+  open import Algebra.Search ambient
+  open F-Coalgebra-Morphism using () renaming (f to u; commutes to coalg-commutes)
 ```
 
 
@@ -34,7 +41,7 @@ Existence of the coequalizer doesn't suffice, we will need some conditions havin
 
 ```agda
   preserves : ∀ {X Y} {f g : X ⇒ Y} → Endofunctor C → Coequalizer f g → Set (o ⊔ ℓ ⊔ e)
-  preserves {X} {Y} {f} {g} F coeq = Coequalizer (Functor.₁ F f) (Functor.₁ F g)
+  preserves {X} {Y} {f} {g} F coeq = IsCoequalizer (Functor.₁ F f) (Functor.₁ F g) (Functor.₁ F (Coequalizer.arr coeq))
 ```
 
 We will now show that the following conditions are equivalent:
@@ -46,28 +53,132 @@ We will now show that the following conditions are equivalent:
 
 ```agda
   module _ (D : DelayM) where
-    open DelayM D renaming (functor to D-Fun; monad to D-Monad; kleisli to D-Kleisli)
+    open DelayM D renaming (functor to D-Functor; monad to D-Monad; kleisli to D-Kleisli)
 
-    open Functor D-Fun using () renaming (F₁ to D₁)
+    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
+    open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
-
+    open Monad D-Monad using () renaming (assoc to M-assoc; identityʳ to M-identityʳ)
-
+    open HomReasoning
-    
+    open M C
+    open MR C
+    open Equiv
 
     module _ (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where
 
       Ď₀ : Obj → Obj
       Ď₀ X = Coequalizer.obj (coeqs X)
 
+      ρ : ∀ {X} → D₀ X ⇒ Ď₀ X
+      ρ {X} = Coequalizer.arr (coeqs X)
+
+      ρ-epi : ∀ {X} → Epi (ρ {X})
+      ρ-epi {X} = Coequalizer⇒Epi (coeqs X)
+
+      -- TODO maybe needs that ρ is natural in X
+      ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X}
+      ρ▷ {X} = sym {! coeq-universal  !}
+        where
+          open Coequalizer (coeqs X) using () renaming (universal to coeq-universal)
+
+      Ď-Functor : Endofunctor C
+      Ď-Functor = record
+        { F₀ = Ď₀
+        ; F₁ = F₁'
+        ; identity = λ {X} → Coequalizer.coequalize-resp-≈ (coeqs X) (elimʳ D-identity) ○ sym (Coequalizer.id-coequalize (coeqs X))
+        ; homomorphism = λ {X} {Y} {Z} {f} {g} → sym (Coequalizer.unique (coeqs X) (sym (begin 
+          (F₁' g ∘ F₁' f) ∘ ρ ≈⟨ pullʳ (sym (Coequalizer.universal (coeqs X))) ⟩ 
+          F₁' g ∘ ρ ∘ D₁ f ≈⟨ pullˡ (sym (Coequalizer.universal (coeqs Y))) ⟩
+          (ρ ∘ D₁ g) ∘ D₁ f ≈⟨ pullʳ (sym D-homomorphism) ⟩
+          ρ ∘ D₁ (g ∘ f) ∎)))
+        ; F-resp-≈ = λ {X} {Y} {f} {g} eq → Coequalizer.coequalize-resp-≈ (coeqs X) (refl⟩∘⟨ (D-resp-≈ eq))
+        }
+        where
+          F₁' : ∀ {X} {Y} (f : X ⇒ Y) → Ď₀ X ⇒ Ď₀ Y
+          F₁' {X} {Y} f = coequalize {h = ρ ∘ D₁ f} (begin 
+            (ρ ∘ D₁ f) ∘ extend ι ≈⟨ pullʳ (sym k-assoc) ⟩ 
+            ρ ∘ extend (extend (now ∘ f) ∘ ι) ≈⟨ refl⟩∘⟨ (extend-≈ (sym (Terminal.!-unique (coalgebras Y) (record { f = extend (now ∘ f) ∘ ι ; commutes = begin 
+              out ∘ extend (now ∘ f) ∘ ι ≈⟨ pullˡ (extendlaw (now ∘ f)) ⟩ 
+              ([ out ∘ now ∘ f , i₂ ∘ D₁ f ] ∘ out) ∘ ι ≈⟨ pullʳ (coalg-commutes (Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})) ⟩ 
+              [ out ∘ now ∘ f , i₂ ∘ D₁ f ] ∘ (idC +₁ ι) ∘  _≅_.from nno-iso ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩ 
+              (f +₁ D₁ f) ∘ (idC +₁ ι) ∘ _≅_.from nno-iso ≈⟨ pullˡ +₁∘+₁ ⟩ 
+              (f ∘ idC +₁ D₁ f ∘ ι) ∘ _≅_.from nno-iso ≈⟨ ((+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl) ⟩ 
+              (idC ∘ f +₁ (D₁ f ∘ ι) ∘ idC) ∘ _≅_.from nno-iso ≈⟨ sym (pullˡ +₁∘+₁) ⟩ 
+              (idC +₁ extend (now ∘ f) ∘ ι) ∘ (f +₁ idC) ∘ _≅_.from nno-iso ∎ })))) ⟩
+            ρ ∘ extend (u (Terminal.! (coalgebras Y) {A = record { A = X × N ; α = (f +₁ idC) ∘ _≅_.from nno-iso }})) ≈⟨ (refl⟩∘⟨ (extend-≈ (Terminal.!-unique (coalgebras Y) (record { f = ι ∘ (f ⁂ idC) ; commutes = begin 
+              out ∘ ι ∘ (f ⁂ idC) ≈⟨ pullˡ (coalg-commutes (Terminal.! (coalgebras Y) {A = record { A = Y × N ; α = _≅_.from nno-iso }})) ⟩ 
+              ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (f ⁂ idC) ≈⟨ assoc ⟩ 
+              (idC +₁ ι) ∘ _≅_.from nno-iso ∘ (f ⁂ idC) ≈⟨ (refl⟩∘⟨ (introʳ (_≅_.isoˡ nno-iso))) ⟩ 
+              (idC +₁ ι) ∘ (_≅_.from nno-iso ∘ (f ⁂ idC)) ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ , idC ⁂ s ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ pullʳ (pullˡ ∘[])) ⟩ 
+              (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ (f ⁂ idC) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ , (f ⁂ idC) ∘ (idC ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ (([]-cong₂ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) (⁂∘⁂ ○ ⁂-cong₂ identityʳ identityˡ)) ⟩∘⟨refl))) ⟩ 
+              (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ f , z ∘ Terminal.! terminal ⟩ , (f ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ refl (refl⟩∘⟨ Terminal.!-unique terminal (Terminal.! terminal ∘ f))) refl ⟩∘⟨refl) ⟩ 
+              (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ f , z ∘ Terminal.! terminal ∘ f ⟩ , (f ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ assoc) (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩ 
+              (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ ∘ f , (idC ⁂ s) ∘ (f ⁂ idC) ] ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ (pullʳ (pullˡ []∘+₁))) ⟩ 
+              (idC +₁ ι) ∘ (_≅_.from nno-iso ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ , idC ⁂ s ]) ∘ (f +₁ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ introˡ (_≅_.isoʳ nno-iso)) ⟩ 
+              (idC +₁ ι) ∘ (f +₁ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) ⟩ 
+              (f +₁ ι ∘ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ sym (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) ⟩
+              (idC +₁ ι ∘ (f ⁂ idC)) ∘ (f +₁ idC) ∘ _≅_.from nno-iso ∎ })))) ⟩
+            ρ ∘ extend (ι ∘ (f ⁂ idC)) ≈⟨ (refl⟩∘⟨ extend-≈ (pushˡ (sym k-identityʳ))) ⟩
+            ρ ∘ extend (extend ι ∘ now ∘ (f ⁂ idC)) ≈⟨ pushʳ k-assoc ⟩
+            (ρ ∘ extend ι) ∘ D₁ (f ⁂ idC) ≈⟨ pushˡ (Coequalizer.equality (coeqs Y)) ⟩
+            ρ ∘ D₁ π₁ ∘ D₁ (f ⁂ idC) ≈⟨ refl⟩∘⟨ sym D-homomorphism ⟩
+            ρ ∘ D₁ (π₁ ∘ (f ⁂ idC)) ≈⟨ (refl⟩∘⟨ (D-resp-≈ project₁)) ⟩
+            ρ ∘ D₁ (f ∘ π₁) ≈⟨ pushʳ D-homomorphism ⟩
+            (ρ ∘ D₁ f) ∘ D₁ π₁ ∎)
+            where 
+              open Coequalizer (coeqs X) using (coequalize; equality) renaming (universal to coeq-universal)
+
       cond-1 : Set (o ⊔ ℓ ⊔ e)
-      cond-1 = ∀ {X} → preserves D-Fun (coeqs X)
+      cond-1 = ∀ X → preserves D-Functor (coeqs X)
 
       cond-2 : Set (o ⊔ ℓ ⊔ e)
-      cond-2 = {!   !}
+      cond-2 = ∀ X → Σ[ s-alg-on ∈ Search-Algebra-on D (Ď₀ X) ] is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = Search-Algebra-on.α s-alg-on }) (ρ {X})
 
       cond-3 : Set (o ⊔ ℓ ⊔ e)
       cond-3 = {!   !}
 
       cond-4 : Set (o ⊔ ℓ ⊔ e)
       cond-4 = {!   !}
+
+      1⇒2 : cond-1 → cond-2
+      1⇒2 c-1 X = s-alg-on , {!   !}
+        where
+          open Coequalizer (coeqs X) renaming (universal to coeq-universal)
+          open IsCoequalizer (c-1 X) using () renaming (equality to D-equality; coequalize to D-coequalize; universal to D-universal; unique to D-unique)
+          s-alg-on : Search-Algebra-on D (Ď₀ X)
+          s-alg-on = record 
+            { α = α'
+            ; identity₁ = ρ-epi (α' ∘ now) idC (begin 
+              (α' ∘ now) ∘ ρ ≈⟨ pullʳ (η.commute ρ) ⟩ 
+              α' ∘ D₁ ρ ∘ now ≈⟨ pullˡ (sym D-universal) ⟩
+              (ρ ∘ μ.η X) ∘ now ≈⟨ cancelʳ M-identityʳ ⟩
+              ρ ≈⟨ sym identityˡ ⟩
+              idC ∘ ρ ∎) 
+            ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ ▷) α' (begin 
+              (α' ∘ ▷) ∘ D₁ ρ ≈⟨ {!   !} ⟩ 
+              {!   !} ≈⟨ {!   !} ⟩
+              {!   !} ≈⟨ {!   !} ⟩
+              {!   !} ≈⟨ {!   !} ⟩
+              α' ∘ D₁ ρ ∎) 
+            }
+            where
+              μ∘Dι : μ.η X ∘ D₁ ι ≈ extend ι
+              μ∘Dι = sym k-assoc ○ extend-≈ (cancelˡ k-identityʳ)
+              eq₁ : D₁ (extend ι) ≈ D₁ (μ.η X) ∘ D₁ (D₁ ι)
+              eq₁ = sym (begin 
+                D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ sym D-homomorphism ⟩ 
+                D₁ (μ.η X ∘ D₁ ι) ≈⟨ D-resp-≈ μ∘Dι ⟩
+                D₁ (extend ι) ∎)
+              α' = D-coequalize {h = ρ {X} ∘ μ.η X} (begin 
+                (ρ ∘ μ.η X) ∘ D₁ (extend ι) ≈⟨ (refl⟩∘⟨ eq₁) ⟩ 
+                (ρ ∘ μ.η X) ∘ D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ pullʳ (pullˡ M-assoc) ⟩
+                ρ ∘ (μ.η X ∘ μ.η (D₀ X)) ∘ D₁ (D₁ ι) ≈⟨ (refl⟩∘⟨ pullʳ (μ.commute ι)) ⟩
+                ρ ∘ μ.η X ∘ (D₁ ι) ∘ μ.η (X × N) ≈⟨ (refl⟩∘⟨ pullˡ μ∘Dι) ⟩
+                ρ ∘ 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₁ = {!   !}
 ```