From 59f60810e78890f1a5c1397f1639e565c41c490b Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Wed, 6 Dec 2023 09:16:10 +0100
Subject: [PATCH] minor

---
 .../Monad/Instance/K/Instance/Delay.lagda.md  | 33 +++++++++++--------
 1 file changed, 20 insertions(+), 13 deletions(-)

diff --git a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md
index ae10bfd..4651843 100644
--- a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md
+++ b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md
@@ -53,7 +53,7 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
 
     data _≈_ : Delay C → Delay C → Set (c ⊔ ℓ) where
       ↓≈ : ∀ {x y a b} (a∼b : a ∼ b) (x↓a : x ↓ a) (y↓b : y ↓ b) → x ≈ y
-      later≈ : ∀ {x y} → (∞ (♭ x ≈ ♭ y)) → later x ≈ later y
+      later≈ : ∀ {x y} (x≈y : ∞ (♭ x ≈ ♭ y)) → later x ≈ later y
 
     ≈-refl : ∀ {x} → x ≈ x
     ≈-refl {now x} = ↓≈ ∼-refl (now↓ ∼-refl) (now↓ ∼-refl)
@@ -85,7 +85,7 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
     where 
       open Setoid A using (Carrier)
       open Equality {A}
-  open Equality using (↓≈; later≈; now↓; later↓; _↓_; ≈↓; ≈-refl; ≈-sym; ≈-trans)
+  open Equality using (↓≈; later≈; now↓; later↓; _↓_; ≈↓; ∼↓; ≈-refl; ≈-sym; ≈-trans)
 
   _[_≈_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : Delay (Setoid.Carrier A)) → Set (c ⊔ ℓ)
   A [ x ≈ y ] = Equality._≈_ {A} x y
@@ -105,6 +105,9 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
   now-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Setoid.Carrier A} → A [ x ∼ y ] → A [ now x ≈ now y ]
   now-cong {A} {x} {y} x∼y = ↓≈ x∼y (now↓ (∼-refl A)) (now↓ (∼-refl A))
 
+  now-inj : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Setoid.Carrier A} → A [ now x ≈ now y ] → A [ x ∼ y ]
+  now-inj {A} {x} {y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = ∼-trans A x∼a (∼-trans A a∼b (∼-sym A y∼b))
+
   delayFun : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → delaySetoid A ⟶ delaySetoid B
   delayFun {A} {B} f = record { _⟨$⟩_ = app ; cong = cong' }
     where
@@ -159,24 +162,28 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
     μ' {A} (now x) = x
     μ' {A} (later x) = later (♯ μ' {A} (♭ x))
 
-    μ↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : Delay (Delay (Setoid.Carrier A))} {y : Delay (Setoid.Carrier A)} → _↓_ {delaySetoid A} x y → A [ (μ' {A} x) ≈ y ]
-    μ↓ {A} {B} f {now x} {y} (now↓ x≈y) = x≈y
-    μ↓ {A} {B} f {later x} {y} (later↓ x↓y) = ≈-trans (later≈ (♯ μ↓ f x↓y)) (≈-sym later-self)
+    μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Setoid.Carrier A))} {y : Delay (Setoid.Carrier A)} → _↓_ {delaySetoid A} x y → A [ (μ' {A} x) ≈ y ]
+    μ↓ {A} {now x} {y} (now↓ x≈y) = x≈y
+    μ↓ {A} {later x} {y} (later↓ x↓y) = ≈-trans (later≈ (♯ μ↓ x↓y)) (≈-sym later-self)
 
     -- TODO μ≈
     -- TODO do delayFun and η in the same style as μ
   
   μ : ∀ (A : Setoid c (c ⊔ ℓ)) → delaySetoid (delaySetoid A) ⟶ delaySetoid A
-  μ A = record { _⟨$⟩_ = μ' {A} ; cong = {!   !} }
+  μ A = record { _⟨$⟩_ = μ' {A} ; cong = cong' }
     where
-      cong' : ∀ {x y : Delay (Delay (Setoid.Carrier A))} → (delaySetoid A) [ x ≈ y ] → A [ μ' x ≈ μ' y ]
-      cong' {now x} {now y} (↓≈ a≈b (now↓ x≈a) (now↓ y≈b)) = ≈-trans x≈a (≈-trans a≈b (≈-sym y≈b))
-      cong' {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = ↓≈ {A} {! a≈b  !} {!   !} (later↓ {!   !})
-      cong' {later x} {now y} (↓≈ a≈b (later↓ x↓a) (now↓ (↓≈ a∼b x↓a₁ y↓b))) = ↓≈ {!   !} (later↓ {!   !}) x↓a₁
-      cong' {later x} {now .(later _)} (↓≈ a≈b (later↓ x↓a) (now↓ (later≈ x₁))) = ↓≈ {!   !} {!   !} {!   !}
-      cong' {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ cong' (↓≈ a∼b x↓a y↓b))
+      cong' : ∀ {x y : Delay (Delay (Setoid.Carrier A))} → (delaySetoid A) [ x ≈ y ] → A [ μ' {A} x ≈ μ' {A} y ]
+      cong' {x} {now y} (↓≈ a≈b x↓a (now↓ y≈b)) = μ↓ (∼↓ (≈-trans a≈b (≈-sym y≈b)) x↓a)
+      cong' {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = ≈-sym (μ↓ (∼↓ (≈-trans (≈-sym a≈b) (≈-sym x≈a)) (later↓ y↓b)))
+      cong' {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ cong' (↓≈ a≈b x↓a y↓b))
       cong' {later x} {later y} (later≈ x≈y) = later≈ (♯ cong' (♭ x≈y))
       
+  μ-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (μ B ∘ delayFun (delayFun f)) ≋ (delayFun f ∘ μ A)
+  μ-natural {A} {B} f {now x} {now y} nx≈ny = cong (delayFun f) (now-inj nx≈ny)
+  μ-natural {A} {B} f {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = later-eq (later≈ (♯ cong (delayFun f) (≈-sym (μ↓ (∼↓ (≈-trans (≈-sym a≈b) (≈-sym x≈a)) y↓b)))))
+  μ-natural {A} {B} f {later x} {now y} (↓≈ a∼b x↓a y↓b) = {!   !}
+  μ-natural {A} {B} f {later x} {later y} (↓≈ a∼b x↓a y↓b) = {!   !}
+  μ-natural {A} {B} f {later x} {later y} (later≈ x≈y) = later≈ (♯ μ-natural f (♭ x≈y))
 
   delayMonad : Monad (Setoids c (c ⊔ ℓ))
   delayMonad = record
@@ -188,7 +195,7 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
       ; F-resp-≈ = {!   !}
       }
     ; η = ntHelper (record { η = η ; commute = η-natural })
-    ; μ = {!   !}
+    ; μ = ntHelper (record { η = μ ; commute = μ-natural })
     ; assoc = {!   !}
     ; sym-assoc = {!   !}
     ; identityˡ = {!   !}