Finish delayMonad proofs without musical notation

agda/src/Monad/Instance/K/Instance/D.lagda.md

@@ -8,7 +8,10 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_)
 open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
-
+open import Function using (id)
+open import Categories.Monad
+open import Categories.Category.Instance.Setoids
+open import Categories.NaturalTransformation hiding (id)
 
 module Monad.Instance.K.Instance.D {c ℓ} where
 
@@ -107,7 +110,7 @@ module Bisimilarity (A : Setoid c (c ⊔ ℓ)) where
   force∼ (∼′-trans x∼y y∼z) = ∼-trans (force∼ x∼y) (force∼ y∼z)
 
   data _↓_ : Delay ∣ A ∣ → ∣ A ∣ → Set (c ⊔ ℓ) where
-    now↓   : ∀ {x y} → [ A ][ x ≡ y ] → now x ↓ y
+    now↓   : ∀ {x y} (x≡y : [ A ][ x ≡ y ]) → now x ↓ y
     later↓ : ∀ {x y} (x↓y : (force x) ↓ y) → later x ↓ y
 
   unique↓ : ∀ {a : Delay ∣ A ∣ } {x y : ∣ A ∣} → a ↓ x → a ↓ y → [ A ][ x ≡ y ]
@@ -210,9 +213,6 @@ module DelayMonad where
   now-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → [ A ][ x ≡ y ] → [ A ][ now x ≈ now y ]
   now-cong {A} {x} {y} x≡y = ↓≈ x≡y (now↓ (≡-refl A)) (now↓ (≡-refl A))
 
-  η : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ Delayₛ A
-  η A = record { _⟨$⟩_ = now ; cong = now-cong }
-
   now-inj : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ 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))
 
@@ -220,12 +220,133 @@ module DelayMonad where
   _≋_ : ∀ {c' ℓ'} {A B : Setoid c' ℓ'} → A ⟶ B → A ⟶ B → Set (c' ⊔ ℓ')
   _≋_ {c'} {ℓ'} {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
 
-  -- later-eq : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay′ ∣ A ∣} {y : Delay ∣ A ∣} → [ A ][ later x ≈ y ] → [ A ][ force x ≈ y ] 
+  later-self : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay′ ∣ A ∣} → [ A ][ force x ≈ later x ]
+  later-self {A} {x} with force x in eqx
+  ...                | now y = ↓≈ (≡-refl A) (now↓ (≡-refl A)) (later↓ helper)
+    where
+      helper : [ A ][ force x ↓ y ]
+      helper rewrite eqx = now↓ (≡-refl A)
+  ...                | later y = later≈ helper
+    where
+      helper : [ A ][ force y ≈′ force x ]
+      force≈ (helper) rewrite eqx = later-self {x = y}
+
+  later-eq : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay′ ∣ A ∣} {y : Delay ∣ A ∣} → [ A ][ later x ≈ y ] → [ A ][ force x ≈ y ] 
   -- later-eq′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay′ ∣ A ∣} {y : Delay ∣ A ∣} → [ A ][ later x ≈′ y ] → [ A ][ force x ≈′ y ] 
   -- force≈ (later-eq′ {A} {x} {y} x≈y) = later-eq (force≈ x≈y)
-  -- later-eq {A} {x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ a≡b x↓a (now↓ y≡b)
-  -- later-eq {A} {x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = ↓≈ a≡b x↓a (later↓ y↓b)
-  -- later-eq {A} {x} {later y} (later≈ x≈y) with force x
-  -- ...                                     | now a = {!   !}
-  -- ...                                     | later a = later≈ (later-eq′ x≈y)
+  later-eq {A} {x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ a≡b x↓a (now↓ y≡b)
+  later-eq {A} {x} {later y} x≈ly = ≈-trans A later-self x≈ly
+
+  lift-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (liftFₛ idₛ) ≋ (idₛ {A = Delayₛ A})
+  lift-id′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay ∣ A ∣} → [ A ][ x ≈′ y ] → [ A ][ (liftF id) x ≈′ id y ]
+  lift-id {A} {now x} {y} x≈y = x≈y
+  lift-id {A} {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ x≡b)) = ↓≈ a≡b (lift↓ idₛ (later↓ x↓a)) (now↓ x≡b)
+  lift-id {A} {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (lift-id′ (≈→≈′ A (↓≈ a≡b x↓a y↓b)))
+  lift-id {A} {later x} {.(later _)} (later≈ x≈y) = later≈ (lift-id′ x≈y)
+  force≈ (lift-id′ {A} {x} {y} x≈y) = lift-id (force≈ x≈y)
+
+  lift-comp : ∀ {A B C : Setoid c (c ⊔ ℓ)} {f : A ⟶ B} {g : B ⟶ C} → liftFₛ (g ∘ f) ≋ (liftFₛ g ∘ liftFₛ f)
+  lift-comp′ : ∀ {A B C : Setoid c (c ⊔ ℓ)} {f : A ⟶ B} {g : B ⟶ C} {x y : Delay ∣ A ∣} → [ A ][ x ≈′ y ] → [ C ][ liftFₛ (g ∘ f) ⟨$⟩ x ≈′ (liftFₛ g ∘ liftFₛ f) ⟨$⟩ y ]
+  force≈ (lift-comp′ {A} {B} {C} {f} {g} {x} {y} x≈y) = lift-comp {A} {B} {C} {f} {g} (force≈ x≈y)
+  lift-comp {A} {B} {C} {f} {g} {now x} {now y} (↓≈ a≡b (now↓ x≡a) (now↓ y≡b)) = now-cong (cong g (cong f (≡-trans A x≡a (≡-trans A a≡b (≡-sym A y≡b)))))
+  lift-comp {A} {B} {C} {f} {g} {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ↓≈ (cong g (cong f a≡b)) (now↓ (cong g (cong f (x≡a)))) (later↓ (lift↓ g (lift↓ f y↓b)))
+  lift-comp {A} {B} {C} {f} {g} {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ (cong g (cong f a≡b)) (later↓ (lift↓ (g ∘ f) x↓a)) (now↓ (cong g (cong f y≡b)))
+  lift-comp {A} {B} {C} {f} {g} {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (lift-comp′ {A} {B} {C} {f} {g} (≈→≈′ A (↓≈ a≡b x↓a y↓b)))
+  lift-comp {A} {B} {C} {f} {g} {later x} {later y} (later≈ x≈y) = later≈ (lift-comp′ {A} {B} {C} {f} {g} x≈y)
+
+  lift-resp-≈ : ∀ {A B : Setoid c (c ⊔ ℓ)} {f g : A ⟶ B} → f ≋ g → liftFₛ f ≋ liftFₛ g
+  lift-resp-≈′ : ∀ {A B : Setoid c (c ⊔ ℓ)} {f g : A ⟶ B} → f ≋ g → ∀ {x y : Delay ∣ A ∣} → [ A ][ x ≈′ y ] → [ B ][ liftFₛ f ⟨$⟩ x ≈′ liftFₛ g ⟨$⟩ y ]
+  lift-resp-≈ {A} {B} {f} {g} f≋g {now x} {now y} x≈y = now-cong (f≋g (now-inj x≈y))
+  lift-resp-≈ {A} {B} {f} {g} f≋g {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ↓≈ (f≋g a≡b) (now↓ (cong f x≡a)) (later↓ (lift↓ g y↓b))
+  lift-resp-≈ {A} {B} {f} {g} f≋g {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ (f≋g a≡b) (later↓ (lift↓ f x↓a)) (now↓ (cong g y≡b))
+  lift-resp-≈ {A} {B} {f} {g} f≋g {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (lift-resp-≈′ {A} {B} {f} {g} f≋g (≈→≈′ A (↓≈ a≡b x↓a y↓b)))
+  lift-resp-≈ {A} {B} {f} {g} f≋g {later x} {later y} (later≈ x≈y) = later≈ (lift-resp-≈′ {A} {B} {f} {g} f≋g x≈y)
+  force≈ (lift-resp-≈′ {A} {B} {f} {g} f≋g {x} {y} x≈y) = lift-resp-≈ {A} {B} {f} {g} f≋g (force≈ x≈y)
+
+  ηₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ Delayₛ A
+  ηₛ A = record { _⟨$⟩_ = now ; cong = now-cong }
+
+  η-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (ηₛ B ∘ f) ≋ (liftFₛ f ∘ ηₛ A)
+  η-natural {A} {B} f {x} {y} x≈y = now-cong (cong f x≈y)
+
+  μ : ∀ {A : Setoid c (c ⊔ ℓ)} → Delay (Delay ∣ A ∣) → Delay ∣ A ∣
+  μ′ : ∀ {A : Setoid c (c ⊔ ℓ)} → Delay′ (Delay ∣ A ∣) → Delay′ ∣ A ∣
+  force (μ′ {A} x) = μ {A} (force x)
+  μ {A} (now x) = x
+  μ {A} (later x) = later (μ′ {A} x)
+
+  μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} {b : ∣ A ∣} → [ Delayₛ A ][ x ↓ y ] → [ A ][ y ↓ b ] → [ A ][ (μ {A} x) ↓ b ]
+  μ↓-trans {A} {now x} {y} {b} (now↓ x≡y) y↓b = ≈↓ A (≈-sym A x≡y) y↓b
+  μ↓-trans {A} {later x} {now y} {b} (later↓ x↓y) (now↓ y≡b) = later↓ (μ↓-trans x↓y (now↓ y≡b))
+  μ↓-trans {A} {later x} {later y} {b} (later↓ x↓y) (later↓ y↓b) = later↓ (μ↓-trans (≡↓ (Delayₛ A) (≈-sym A later-self) x↓y) y↓b)
+
+  μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} → [ Delayₛ A ][ x ↓ y ] → [ A ][ (μ {A} x) ≈ y ]
+  μ↓′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} → [ Delayₛ A ][ x ↓ y ] → [ A ][ (μ {A} x) ≈′ y ]
+  force≈ (μ↓′ {A} {x} {y} x↓y) = μ↓ x↓y
+  μ↓ {A} {now x} {y} (now↓ x≡y) = x≡y
+  μ↓ {A} {later x} {now y} (later↓ x↓y) = ≈-trans A (≈-sym A later-self) (↓≈ (≡-refl A) (μ↓-trans x↓y (now↓ (≡-refl A))) (now↓ (≡-refl A)))
+  μ↓ {A} {later x} {later y} (later↓ x↓y) = later≈ (μ↓′ {A} {force x} {force y} (≡↓ (Delayₛ A) (≈-sym A later-self) x↓y))
+
+  μ-cong : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ A ][ x ≈ y ] → [ A ][ μ {A} x ≈ μ {A} y ]
+  μ-cong′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ A ][ x ≈′ y ] → [ A ][ μ {A} x ≈′ μ {A} y ]
+  μ-cong A {now x} {now y} x≈y = now-inj x≈y
+  μ-cong A {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ≈-trans A (≈-sym A (μ↓ (≡↓ (Delayₛ A) (≈-trans A (≈-sym A a≡b) (≈-sym A x≡a)) y↓b))) later-self
+  μ-cong A {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ≈-trans A (≈-sym A later-self) (μ↓ (≡↓ (Delayₛ A) (≈-trans A a≡b (≈-sym A y≡b)) x↓a))
+  μ-cong A {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (μ-cong′ A (≈→≈′ (Delayₛ A) (↓≈ a≡b x↓a y↓b)))
+  μ-cong A {later x} {later y} (later≈ x≈y) = later≈ (μ-cong′ A x≈y)
+  force≈ (μ-cong′ A {x} {y} x≈y) = μ-cong A (force≈ x≈y)
+
+  μₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delayₛ (Delayₛ A) ⟶ Delayₛ A
+  μₛ A = record { _⟨$⟩_ = μ {A} ; cong = μ-cong A }
+
+  μ-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (μₛ B ∘ liftFₛ (liftFₛ f)) ≋ (liftFₛ f ∘ μₛ A)
+  μ-natural′ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → ∀ {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ A ][ x ≈′ y ] → [ B ][ (μₛ B ∘ liftFₛ (liftFₛ f)) ⟨$⟩ x ≈′ (liftFₛ f ∘ μₛ A) ⟨$⟩ y ]
+  force≈ (μ-natural′ {A} {B} f {x} {y} x≈y) = μ-natural f (force≈ x≈y)
+  μ-natural {A} {B} f {now x} {now y} x≈y = lift-cong f (now-inj x≈y)
+  μ-natural {A} {B} f {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ≈-trans B (lift-cong f (≈-sym A (μ↓ (≡↓ (Delayₛ A) (≈-sym A (≈-trans A x≡a a≡b)) y↓b)))) later-self
+  μ-natural {A} {B} f {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ x≡y)) = ≈-trans B (≈-sym B later-self) (μ↓ (lift↓ (liftFₛ f) (≡↓ (Delayₛ A) (≈-trans A a≡b (≈-sym A x≡y)) x↓a)))
+  μ-natural {A} {B} f {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (μ-natural′ f (≈→≈′ (Delayₛ A) (↓≈ a≡b x↓a y↓b)))
+  μ-natural {A} {B} f {later x} {later y} (later≈ x≈y) = later≈ (μ-natural′ f x≈y)
+
+  μ-assoc' : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼ (μₛ A ∘ μₛ (Delayₛ A)) ⟨$⟩ x ]
+  μ-assoc'′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼′ (μₛ A ∘ μₛ (Delayₛ A)) ⟨$⟩ x ]
+  force∼ (μ-assoc'′ {A} {x}) = μ-assoc' {A} {x}
+  μ-assoc' {A} {now x} = ∼-refl A
+  μ-assoc' {A} {later x} = later∼ (μ-assoc'′ {A} {force x})
+
+  μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ (liftFₛ (μₛ A))) ≋ (μₛ A ∘ μₛ (Delayₛ A))
+  μ-assoc {A} {x} {y} x≈y = ≈-trans A (μ-cong A (lift-cong (μₛ A) x≈y)) (∼⇒≈ (μ-assoc' {A} {y}))
+
+  identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay ∣ A ∣} {y : ∣ A ∣} → [ A ][ x ↓ y ] → [ A ][ ((μₛ A) ⟨$⟩ ((liftFₛ (ηₛ A)) ⟨$⟩ x)) ↓ y ]
+  identityˡ↓ {A} {now x} {y} x↓y = x↓y
+  identityˡ↓ {A} {later x} {y} (later↓ x↓y) = later↓ (identityˡ↓ x↓y)
+
+  identityˡ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ liftFₛ (ηₛ A)) ≋ idₛ
+  identityˡ′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay ∣ A ∣} → [ A ][ x ≈′ y ] → [ A ][ (μₛ A ∘ liftFₛ (ηₛ A)) ⟨$⟩ x ≈′ y ]
+  force≈ (identityˡ′ {A} {x} {y} x≈y) = identityˡ (force≈ x≈y)
+  identityˡ {A} {now x} {y} x≈y = x≈y
+  identityˡ {A} {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ a≡b (later↓ (identityˡ↓ x↓a)) (now↓ y≡b)
+  identityˡ {A} {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (identityˡ′ (≈→≈′ A (↓≈ a≡b x↓a y↓b)))
+  identityˡ {A} {later x} {later y} (later≈ x≈y) = later≈ (identityˡ′ x≈y)
+
+  identityʳ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ ηₛ (Delayₛ A)) ≋ idₛ
+  identityʳ {A} {now x} {y} x≈y = x≈y
+  identityʳ {A} {later x} {y} x≈y = x≈y
+
+  delayMonad : Monad (Setoids c (c ⊔ ℓ))
+  delayMonad = record
+    { F = record
+      { F₀ = Delayₛ
+      ; F₁ = liftFₛ
+      ; identity = lift-id
+      ; homomorphism = λ {X} {Y} {Z} {f} {g} → lift-comp {X} {Y} {Z} {f} {g}
+      ; F-resp-≈ = λ {A} {B} {f} {g} → lift-resp-≈ {A} {B} {f} {g}
+      }
+    ; η = ntHelper (record { η = ηₛ ; commute = η-natural })
+    ; μ = ntHelper (record { η = μₛ ; commute = μ-natural })
+    ; assoc = μ-assoc
+    ; sym-assoc = λ {A} {x} {y} x≈y → ≈-sym A (μ-assoc (≈-sym (Delayₛ (Delayₛ A)) x≈y))
+    ; identityˡ = identityˡ
+    ; identityʳ = identityʳ
+    }
 ```