From bb49f238145f24006cd1ed67ad5da759ee4238d4 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Sun, 4 Feb 2024 17:55:22 +0100
Subject: [PATCH] Finish proof that quotient of D is freealgebra

---
 agda/src/Monad/Instance/Setoids/K.lagda.md | 40 ++++++++++++++++++----
 1 file changed, 34 insertions(+), 6 deletions(-)

diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md
index ed03469..6da595f 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -350,7 +350,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
           ... | inj₁ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
           ... | inj₂ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
 
-  <<_>> = Elgot-Algebra-Morphism.h
+  open Elgot-Algebra-Morphism using (preserves) renaming (h to <<_>>)
 
   freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
   freeAlgebra A = record 
@@ -358,13 +358,41 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
     ; η = ηₛ A
     ; _* = delay-lift 
     ; *-lift = λ {B} f {x} → Elgot-Algebra.#-Fixpoint B
-    ; *-uniq = λ {B} f g eq {x} → *-uniq' {B} f g eq {x}
+    ; *-uniq = λ {B} f g eq {x} → *-uniq' {B} f g (delay-lift f) eq (#-Fixpoint B) {x}
     }
     where
-      *-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g : Elgot-Algebra-Morphism (delay-algebras A) B) (eq : (<< g >> ∘ (ηₛ A)) ≋ f) {x : Delay ∣ A ∣} → [_][_≡_] (⟦ B ⟧) ((<< g >>) ⟨$⟩ x) ((<< delay-lift {A} {B} f >>) ⟨$⟩ x)
-      *-uniq' {B} f g eq {now x} = ≡-trans ⟦ B ⟧ (eq {x}) (≡-sym ⟦ B ⟧ (#-Fixpoint B))
-      *-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {!   !} (≡-sym ⟦ B ⟧ (#-Fixpoint B)) 
-      -- *-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {! *-uniq' {B} f g eq {force x}  !} (≡-sym ⟦ B ⟧ (#-Fixpoint B)) 
+      *-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g h : Elgot-Algebra-Morphism (delay-algebras A) B) 
+        → (<< g >> ∘ (ηₛ A)) ≋ f
+        → (<< h >> ∘ (ηₛ A)) ≋ f
+        → << g >> ≋ << h >>
+      *-uniq' {B} f g h eqᵍ eqʰ {x} = ≡-trans ⟦ B ⟧ (cong << g >> iter-id) 
+                                     (≡-trans ⟦ B ⟧ (preserves g {Delayₛ∼ A} {[ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now} {x = x}) 
+                                     (≡-trans ⟦ B ⟧ (#-resp-≈ B (λ {x} → helper-eq' {x}) {x}) 
+                                     (≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ (preserves h {Delayₛ∼ A} {[ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now} {x = x})) 
+                                                    (≡-sym ⟦ B ⟧ (cong << h >> iter-id)))))
+        where
+        open Elgot-Algebra B using (_#)
+        quot-morph : ∀ {A : Setoid ℓ ℓ} → Delayₛ∼ A ⟶ Delayₛ A
+        quot-morph {A} = record { to = λ x → x ; cong = λ eq → ∼⇒≈ eq }
+
+        helper-now₁ : (Delay ∣ A ∣) → (Delay ∣ A ∣ ⊎ (Delay ∣ A ∣))
+        helper-now₁ (now x) = inj₁ (now x)
+        helper-now₁ (later x) = inj₂ (force x)
+        helper-now : Delayₛ∼ A ⟶ ((Delayₛ∼ A) ⊎ₛ (Delayₛ∼ A))
+        helper-now = record { to = helper-now₁ ; cong = λ { (now∼ eq)   → inj₁ (now∼ eq) 
+                                                          ; (later∼ eq) → inj₂ (force∼ eq) } }
+
+        helper-eq' : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ ([ inj₁ₛ ∘ << g >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x 
+                                                   ≡ ([ inj₁ₛ ∘ << h >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
+        helper-eq' {now x} = inj₁ (≡-trans ⟦ B ⟧ eqᵍ (≡-sym ⟦ B ⟧ eqʰ))
+        helper-eq' {later x} = inj₂ (∼-refl A)
+
+        iter-id :  ∀ {x} → [ A ][ x ≈  iterₛ ([ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
+        iter-id′ : ∀ {x} → [ A ][ x ≈′ iterₛ ([ inj₁ₛ ∘ quot-morph , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
+        force≈ (iter-id′ {x}) = iter-id {x}
+        iter-id {now x} = ≈-refl A
+        iter-id {later x} = later≈ (iter-id′ {force x})
+
 
   delayK : MonadK
   delayK = record { freealgebras = freeAlgebra ; stable = {!   !} }