♻ major refactor of example

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

@@ -12,7 +12,7 @@ open import Categories.Category.Cocartesian
 open import Categories.Object.Terminal
 open import Function.Equality as SΠ renaming (id to idₛ)
 import Categories.Morphism.Reasoning as MR
-open import Relation.Binary
+open import Relation.Binary using (Setoid; IsEquivalence)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Sum.Function.Setoid
 open import Data.Sum.Relation.Binary.Pointwise
@@ -24,7 +24,7 @@ import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_)
 open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
 open import Codata.Musical.Notation
-import Category.Monad.Partiality
+-- import Category.Monad.Partiality
 
 open import Category.Ambient.Setoids
 ```
@@ -37,211 +37,212 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
 # Capretta's Delay Monad is an Instance of K in the Category of Setoids
 
 ```agda
-  open Setoid using () renaming (Carrier to ∣_∣)
+  open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_])
+  open module eq (S : Setoid c (c ⊔ ℓ)) = IsEquivalence (Setoid.isEquivalence S) using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
+
+
   data _⊥ (A : Set c) : Set c where
     now : A → A ⊥
     later : ∞ (A ⊥) → A ⊥
 
-  module Equality {A : Setoid c (c ⊔ ℓ)} where
+  module StrongBisimilarity (A : Setoid c (c ⊔ ℓ)) where
-    open Setoid A renaming (Carrier to C; _≈_ to _∼_)
-    open IsEquivalence (Setoid.isEquivalence A) renaming (refl to ∼-refl; sym to ∼-sym; trans to ∼-trans)
 
-    data _↓_ : C ⊥ → C → Set (c ⊔ ℓ) where
+    data _∼_ : ∣ A ∣ ⊥ → ∣ A ∣ ⊥ → Set (c ⊔ ℓ) where
-      now↓ : ∀ {x y} (x∼y : x ∼ y) → now x ↓ y
+      now∼ : ∀ {x y : ∣ A ∣} → [ A ][ x ≡ y ] → now x ∼ now y
+      later∼ : ∀ {x y} → ∞ (♭ x ∼ ♭ y) → later x ∼ later y
+    
+    ∼-refl : ∀ {x} → x ∼ x
+    ∼-refl {now x} = now∼ (≡-refl A)
+    ∼-refl {later x} = later∼ (♯ ∼-refl)
+
+    ∼-sym : ∀ {x y} → x ∼ y → y ∼ x
+    ∼-sym {.(now _)} {.(now _)} (now∼ x≡y) = now∼ (≡-sym A x≡y)
+    ∼-sym {.(later _)} {.(later _)} (later∼ x∼y) = later∼ (♯ ∼-sym (♭ x∼y))
+
+    ∼-trans : ∀ {x y z} → x ∼ y → y ∼ z → x ∼ z
+    ∼-trans {.(now _)} {.(now _)} {.(now _)} (now∼ x≡y) (now∼ y≡z) = now∼ (≡-trans A x≡y y≡z)
+    ∼-trans {.(later _)} {.(later _)} {.(later _)} (later∼ x∼y) (later∼ y∼z) = later∼ (♯ ∼-trans (♭ x∼y) (♭ y∼z))
+
+  open StrongBisimilarity renaming (_∼_ to [_][_∼_])
+
+  module WeakBisimilarity (A : Setoid c (c ⊔ ℓ)) where
+    data _↓_ : ∣ A ∣ ⊥ → ∣ A ∣ → Set (c ⊔ ℓ) where
+      now↓ : ∀ {x y} (x≡y : [ A ][ x ≡ y ]) → now x ↓ y
       later↓ : ∀ {x y} (x↓y : ♭ x ↓ y) → later x ↓ y
 
-    unique↓ : ∀ {c : C ⊥} {x y : C} → c ↓ x → c ↓ y → x ∼ y
+    unique↓ : ∀ {a : ∣ A ∣ ⊥} {x y : ∣ A ∣} → a ↓ x → a ↓ y → [ A ][ x ≡ y ]
-    unique↓ (now↓ eq₁) (now↓ eq₂) = ∼-trans (∼-sym eq₁) eq₂
+    unique↓ (now↓ a≡x) (now↓ a≡y) = ≡-trans A (≡-sym A a≡x) a≡y
-    unique↓ (later↓ p) (later↓ q) = unique↓ p q
+    unique↓ (later↓ a↓x) (later↓ a↓y) = unique↓ a↓x a↓y
 
-    data _≈_ : C ⊥ → C ⊥ → Set (c ⊔ ℓ) where
+    data _≈_ : ∣ A ∣ ⊥ → ∣ A ∣ ⊥ → Set (c ⊔ ℓ) where
-      ↓≈ : ∀ {x y a b} (a∼b : a ∼ b) (x↓a : x ↓ a) (y↓b : y ↓ b) → x ≈ y
+      ↓≈ : ∀ {x y a b} (a≡b : [ A ][ a ≡ b ]) (x↓a : x ↓ a) (y↓b : y ↓ b) → x ≈ y
       later≈ : ∀ {x y} (x≈y : ∞ (♭ x ≈ ♭ y)) → later x ≈ later y
 
     ≈-refl : ∀ {x} → x ≈ x
-    ≈-refl {now x} = ↓≈ ∼-refl (now↓ ∼-refl) (now↓ ∼-refl)
+    ≈-refl {now x} = ↓≈ (≡-refl A) (now↓ (≡-refl A)) (now↓ (≡-refl A))
     ≈-refl {later x} = later≈ (♯ ≈-refl)
 
     ≈-sym : ∀ {x y} → x ≈ y → y ≈ x
-    ≈-sym (↓≈ a∼b x↓a y↓b) = ↓≈ (∼-sym a∼b) y↓b x↓a
+    ≈-sym (↓≈ a≡b x↓a y↓b) = ↓≈ (≡-sym A a≡b) y↓b x↓a
     ≈-sym (later≈ x≈y) = later≈ (♯ ≈-sym (♭ x≈y))
 
-    ∼↓ : ∀ {x y : C} {z : C ⊥} → x ∼ y → z ↓ x → z ↓ y
+    ≡↓ : ∀ {x y : ∣ A ∣} {z : ∣ A ∣ ⊥} → [ A ][ x ≡ y ] → z ↓ x → z ↓ y
-    ∼↓ {x} {y} {.(now _)} x∼y (now↓ a∼x) = now↓ (∼-trans a∼x x∼y)
+    ≡↓ {x} {y} {.(now _)} x≡y (now↓ a≡x) = now↓ (≡-trans A a≡x x≡y)
-    ∼↓ {x} {y} {.(later _)} x∼y (later↓ z↓x) = later↓ (∼↓ x∼y z↓x)
+    ≡↓ {x} {y} {.(later _)} x≡y (later↓ z↓x) = later↓ (≡↓ x≡y z↓x)
 
-    ≈↓ : ∀ {x y : C ⊥} {z : C} → x ≈ y → x ↓ z → y ↓ z
+    ≈↓ : ∀ {x y : ∣ A ∣ ⊥} {z : ∣ A ∣} → x ≈ y → x ↓ z → y ↓ z
-    ≈↓ (↓≈ a∼b (now↓ x∼a) y↓b) (now↓ x∼z) = ∼↓ (∼-trans (∼-sym a∼b) (∼-trans (∼-sym x∼a) x∼z)) y↓b
+    ≈↓ (↓≈ a≡b (now↓ x≡a) y↓b) (now↓ x≡z) = ≡↓ (≡-trans A (≡-sym A a≡b) (≡-trans A (≡-sym A x≡a) x≡z)) y↓b
-    ≈↓ (↓≈ a∼b (later↓ x↓a) y↓b) (later↓ x↓z) with unique↓ x↓a x↓z 
+    ≈↓ (↓≈ a≡b (later↓ x↓a) y↓b) (later↓ x↓z) with unique↓ x↓a x↓z 
-    ...                                         | a∼z = ∼↓ (∼-trans (∼-sym a∼b) a∼z) y↓b
+    ...                                         | a∼z = ≡↓ (≡-trans A (≡-sym A a≡b) a∼z) y↓b
     ≈↓ (later≈ x) (later↓ x↓z) = later↓ (≈↓ (♭ x) x↓z)
 
     ≈-trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
-    ≈-trans (↓≈ a∼b x↓a y↓b) (↓≈ c∼d y↓c z↓d) with unique↓ y↓b y↓c
+    ≈-trans (↓≈ a≡b x↓a y↓b) (↓≈ c≡d y↓c z↓d) with unique↓ y↓b y↓c
-    ...                                 | b∼c = ↓≈ (∼-trans (∼-trans a∼b b∼c) c∼d) x↓a z↓d
+    ...                                       | b≡c = ↓≈ (≡-trans A (≡-trans A a≡b b≡c) c≡d) x↓a z↓d
-    ≈-trans (↓≈ a∼b z↓a (later↓ x↓b)) (later≈ x≈y) = ↓≈ a∼b z↓a (later↓ (≈↓ (♭ x≈y) x↓b))
+    ≈-trans (↓≈ a≡b z↓a (later↓ x↓b)) (later≈ x≈y) = ↓≈ a≡b z↓a (later↓ (≈↓ (♭ x≈y) x↓b))
-    ≈-trans (later≈ x≈y) (↓≈ a∼b (later↓ y↓a) z↓b) = ↓≈ a∼b (later↓ (≈↓ (≈-sym (♭ x≈y)) y↓a)) z↓b
+    ≈-trans (later≈ x≈y) (↓≈ a≡b (later↓ y↓a) z↓b) = ↓≈ a≡b (later↓ (≈↓ (≈-sym (♭ x≈y)) y↓a)) z↓b
     ≈-trans (later≈ x≈y) (later≈ y≈z) = later≈ (♯ ≈-trans (♭ x≈y) (♭ y≈z)) 
     
-  -- _⊥ₛ
+  open WeakBisimilarity renaming (_≈_ to [_][_≈_]; _↓_ to [_][_↓_])
+
+  ∼⇒≈ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣ ⊥} → [ A ][ x ∼ y ] → [ A ][ x ≈ y ]
+  ∼⇒≈ {A} {.(now _)} {.(now _)} (now∼ a≡b) = ↓≈ a≡b (now↓ (≡-refl A)) (now↓ (≡-refl A))
+  ∼⇒≈ {A} {.(later _)} {.(later _)} (later∼ x∼y) = later≈ (♯ ∼⇒≈ (♭ x∼y))
+
+  <_> = Π._⟨$⟩_
+
   _⊥ₛ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
-  _⊥ₛ A = record { Carrier = ∣ A ∣ ⊥ ; _≈_ = _≈_ ; isEquivalence = record { refl = ≈-refl ; sym = ≈-sym ; trans = ≈-trans } }
+  _⊥ₛ A = record { Carrier = ∣ A ∣ ⊥ ; _≈_ = [_][_≈_] A ; isEquivalence = record { refl = ≈-refl A ; sym = ≈-sym A ; trans = ≈-trans A } }
-    where 
-      open Equality {A}
-  open Equality using (↓≈; later≈; now↓; later↓; _↓_; ≈↓; ∼↓; ≈-refl; ≈-sym; ≈-trans)
 
-  _[_≈_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : ∣ A ∣ ⊥) → Set (c ⊔ ℓ)
+  now-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → [ A ][ x ≡ y ] → [ A ][ now x ≈ now y ]
-  A [ x ≈ y ] = Equality._≈_ {A} x y
+  now-cong {A} {x} {y} x∼y = ↓≈ x∼y (now↓ (≡-refl A)) (now↓ (≡-refl A))
 
-  _[_∼_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : ∣ A ∣) → Set (c ⊔ ℓ)
+  now-inj : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → [ A ][ now x ≈ now y ] → [ A ][ x ≡ y ]
-  A [ x ∼ y ] = Setoid._≈_ 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))
 
-  ∼-refl : ∀ (A : Setoid c (c ⊔ ℓ)) {x : ∣ A ∣} → A [ x ∼ x ]
+  liftF : ∀ {A B : Set c} → (A → B) → A ⊥ → B ⊥
-  ∼-refl A = IsEquivalence.refl (Setoid.isEquivalence A) 
+  liftF f (now x) = now (f x)
-
-  ∼-sym : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : ∣ A ∣} → A [ x ∼ y ] → A [ y ∼ x ]
-  ∼-sym A = IsEquivalence.sym (Setoid.isEquivalence A)
-
-  ∼-trans : ∀ (A : Setoid c (c ⊔ ℓ)) {x y z : ∣ A ∣} → A [ x ∼ y ] → A [ y ∼ z ] → A [ x ∼ z ]
-  ∼-trans A = IsEquivalence.trans (Setoid.isEquivalence A)
-
-  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))
-
-  -- slightly different types than later≈
-  -- TODO remove this is useless
-  later-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣ ⊥} → A [ x ≈ y ] → A [ later (♯ x) ≈ later (♯ y) ]
-  later-cong {A} {x} {y} x≈y = later≈ (♯ x≈y)
-
-  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))
-
-  liftF : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → ∣ A ∣ ⊥ → ∣ B ∣ ⊥
-  liftF f (now x) = now (f ⟨$⟩ x)
   liftF f (later x) = later (♯ liftF f (♭ x))
 
-  delayFun : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → A ⊥ₛ ⟶ B ⊥ₛ
+  lift↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : ∣ A ∣ ⊥} {b : ∣ A ∣} → [ A ][ x ↓ b ] → [ B ][ liftF (f ._⟨$⟩_) x ↓ f ⟨$⟩ b ]
-  delayFun {A} {B} f = record { _⟨$⟩_ = liftF f ; cong = cong' }
+  lift↓ {A} {B} f {now x} {b} (now↓ x≡b) = now↓ (cong f x≡b)
-    where
+  lift↓ {A} {B} f {later x} {b} (later↓ x↓b) = later↓ (lift↓ f x↓b)
-      ↓-cong : ∀ {x : ∣ A ∣ ⊥} {b : ∣ A ∣} → _↓_ {A} x b → _↓_ {B} (liftF f x) (f ⟨$⟩ b)
-      ↓-cong {now x} {b} (now↓ x∼y) = now↓ (cong f x∼y) 
-      ↓-cong {later x} {b} (later↓ x↓b) = later↓ (↓-cong x↓b)
-      cong' : ∀ {x y : ∣ A ∣ ⊥} → A [ x ≈ y ] → B [ liftF f x ≈ liftF f y ]
-      cong' {now x} {now y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = now-cong (cong f (∼-trans A x∼a (∼-trans A a∼b (∼-sym A y∼b))))
-      cong' {now x} {later y} (↓≈ a∼b (now↓ x∼a) (later↓ y↓b)) = ↓≈ (cong f (∼-trans A x∼a a∼b)) (now↓ (∼-refl B)) (later↓ (↓-cong y↓b))
-      cong' {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (cong f (∼-trans A a∼b (∼-sym A y∼b))) (later↓ (↓-cong x↓a)) (now↓ (∼-refl 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))
 
-  -- this needs polymorphic universe levels
+  lift-cong : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x y : ∣ A ∣ ⊥} → [ A ][ x ≈ y ] → [ B ][ liftF < f > x ≈ liftF < f > y ]
+  lift-cong {A} {B} f {now x} {now y} (↓≈ a≡b (now↓ x≡a) (now↓ y≡b)) = now-cong (cong f (≡-trans A x≡a (≡-trans A a≡b (≡-sym A y≡b))))
+  lift-cong {A} {B} f {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ↓≈ (cong f (≡-trans A x≡a a≡b)) (now↓ (≡-refl B)) (later↓ (lift↓ f y↓b))
+  lift-cong {A} {B} f {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ (cong f (≡-trans A a≡b (≡-sym A y≡b))) (later↓ (lift↓ f x↓a)) (now↓ (≡-refl B))
+  lift-cong {A} {B} f {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ lift-cong f (↓≈ a≡b x↓a y↓b))
+  lift-cong {A} {B} f {later x} {later y} (later≈ x≈y) = later≈ (♯ lift-cong f (♭ x≈y))
+
+  liftFₛ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → A ⊥ₛ ⟶ B ⊥ₛ
+  liftFₛ {A} {B} f = record { _⟨$⟩_ = liftF < f > ; cong = lift-cong f }
+
+--   -- this needs polymorphic universe levels
   _≋_ : ∀ {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 y : ∣ A ∣ ⊥} → A [ later (♯ x) ≈ y ] → A [ x ≈ y ] 
+  later-eq : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣ ⊥} → [ A ][ later (♯ x) ≈ y ] → [ A ][ x ≈ y ] 
-  later-eq {A} {x} {y} (↓≈ a∼b (later↓ x↓a) y↓b) = ↓≈ a∼b x↓a y↓b
+  later-eq {A} {x} {y} (↓≈ a≡b (later↓ x↓a) y↓b) = ↓≈ a≡b x↓a y↓b
-  later-eq {A} {now x} {later y} (later≈ x≈y) = ↓≈ (∼-refl A) (now↓ (∼-refl A)) (later↓ (≈↓ (♭ x≈y) (now↓ (∼-refl A))))
+  later-eq {A} {now x} {later y} (later≈ x≈y) = ↓≈ (≡-refl A) (now↓ (≡-refl A)) (later↓ (≈↓ A (♭ x≈y) (now↓ (≡-refl A))))
-  later-eq {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ later-eq (≈-trans (later≈ (♯ ≈-refl)) (♭ x≈y)))
+  later-eq {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ later-eq (≈-trans A (later≈ (♯ ≈-refl A)) (♭ x≈y)))
 
-  later-self : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ A ∣ ⊥} → A [ x ≈ later (♯ x) ]
+  later-self : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ A ∣ ⊥} → [ A ][ x ≈ later (♯ x) ]
-  later-self {A} {now x} = ↓≈ (∼-refl A) (now↓ (∼-refl A)) (later↓ (now↓ (∼-refl A)))
+  later-self {A} {now x} = ↓≈ (≡-refl A) (now↓ (≡-refl A)) (later↓ (now↓ (≡-refl A)))
-  later-self {A} {later x} = later-eq (later≈ (♯ ≈-refl))
+  later-self {A} {later x} = later-eq (later≈ (♯ ≈-refl A))
 
-  delayFun↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : ∣ A ∣ ⊥} {y : ∣ A ∣} → _↓_ {A} x y → _↓_ {B} (delayFun f ⟨$⟩ x) (f ⟨$⟩ y)
+  lift-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (liftFₛ idₛ) ≋ (idₛ {A = A ⊥ₛ})
-  delayFun↓ {A} {B} f {now x} {y} (now↓ x∼y) = now↓ (cong f x∼y)
+  lift-id {A} {now x} {now y} (↓≈ a≡b (now↓ x≡a) (now↓ y≡b)) = ↓≈ a≡b (now↓ x≡a) (now↓ y≡b)
-  delayFun↓ {A} {B} f {later x} {y} (later↓ x↓y) = later↓ (delayFun↓ f x↓y)
+  lift-id {A} {now x} {later y} x≈y = x≈y
+  lift-id {A} {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ a≡b (later↓ (lift↓ idₛ x↓a)) (now↓ y≡b)
+  lift-id {A} {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ lift-id (↓≈ a≡b x↓a y↓b))
+  lift-id {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ lift-id (♭ x≈y))
 
-  delayFun-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (delayFun idₛ) ≋ (idₛ {A = A ⊥ₛ})
+  lift-comp : ∀ {A B C : Setoid c (c ⊔ ℓ)} {f : A ⟶ B} {g : B ⟶ C} → liftFₛ (g ∘ f) ≋ (liftFₛ g ∘ liftFₛ f)
-  delayFun-id {A} {now x} {now y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = ↓≈ a∼b (now↓ x∼a) (now↓ y∼b)
+  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)))))
-  delayFun-id {A} {now x} {later y} x≈y = x≈y
+  lift-comp {A} {B} {C} {f} {g} {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ↓≈ (cong g (cong f (≡-trans A x≡a a≡b))) (now↓ (≡-refl C)) (later↓ (lift↓ g (lift↓ f y↓b)))
-  delayFun-id {A} {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ a∼b (later↓ (delayFun↓ idₛ x↓a)) (now↓ 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 (≡-trans A a≡b (≡-sym A y≡b)))) (later↓ (lift↓ (g ∘ f) x↓a)) (now↓ (≡-refl C))
-  delayFun-id {A} {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ delayFun-id (↓≈ a∼b x↓a 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≡b x↓a y↓b))
-  delayFun-id {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ delayFun-id (♭ x≈y))
+  lift-comp {A} {B} {C} {f} {g} {later x} {later y} (later≈ x≈y) = later≈ (♯ lift-comp {A} {B} {C} {f} {g} (♭ x≈y))
 
-  delayFun-comp : ∀ {A B C : Setoid c (c ⊔ ℓ)} {f : A ⟶ B} {g : B ⟶ C} → delayFun (g ∘ f) ≋ (delayFun g ∘ delayFun f)
+  lift-resp-≈ : ∀ {A B : Setoid c (c ⊔ ℓ)} {f g : A ⟶ B} → f ≋ g → liftFₛ f ≋ liftFₛ g
-  delayFun-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-resp-≈ {A} {B} {f} {g} f≋g {now x} {now y} x≈y = now-cong (f≋g (now-inj x≈y))
-  delayFun-comp {A} {B} {C} {f} {g} {now x} {later y} (↓≈ a∼b (now↓ x∼a) (later↓ y↓b)) = ↓≈ (cong g (cong f (∼-trans A x∼a a∼b))) (now↓ (∼-refl C)) (later↓ (delayFun↓ g (delayFun↓ f y↓b)))
+  lift-resp-≈ {A} {B} {f} {g} f≋g {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ↓≈ (f≋g (≡-trans A x≡a a≡b)) (now↓ (≡-refl B)) (later↓ (lift↓ g y↓b))
-  delayFun-comp {A} {B} {C} {f} {g} {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (cong g (cong f (∼-trans A a∼b (∼-sym A y∼b)))) (later↓ (delayFun↓ (g ∘ f) x↓a)) (now↓ (∼-refl C))
+  lift-resp-≈ {A} {B} {f} {g} f≋g {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ (f≋g (≡-trans A a≡b (≡-sym A y≡b))) (later↓ (lift↓ f x↓a)) (now↓ (≡-refl B))
-  delayFun-comp {A} {B} {C} {f} {g} {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ delayFun-comp (↓≈ a∼b x↓a 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≡b x↓a y↓b))
-  delayFun-comp {A} {B} {C} {f} {g} {later x} {later y} (later≈ x≈y) = later≈ (♯ delayFun-comp (♭ x≈y))
+  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))
-
-  delayFun-resp-≈ : ∀ {A B : Setoid c (c ⊔ ℓ)} {f g : A ⟶ B} → f ≋ g → delayFun f ≋ delayFun g
-  delayFun-resp-≈ {A} {B} {f} {g} f≋g {now x} {now y} x≈y = now-cong (f≋g (now-inj x≈y))
-  delayFun-resp-≈ {A} {B} {f} {g} f≋g {now x} {later y} (↓≈ a∼b (now↓ x∼a) (later↓ y↓b)) = ↓≈ (f≋g (∼-trans A x∼a a∼b)) (now↓ (∼-refl B)) (later↓ (delayFun↓ g y↓b))
-  delayFun-resp-≈ {A} {B} {f} {g} f≋g {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (f≋g (∼-trans A a∼b (∼-sym A y∼b))) (later↓ (delayFun↓ f x↓a)) (now↓ (∼-refl B))
-  delayFun-resp-≈ {A} {B} {f} {g} f≋g {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ delayFun-resp-≈ f≋g (↓≈ a∼b x↓a y↓b))
-  delayFun-resp-≈ {A} {B} {f} {g} f≋g {later x} {later y} (later≈ x≈y) = later≈ (♯ delayFun-resp-≈ f≋g (♭ x≈y))
 
   η : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ A ⊥ₛ
-  η A = record { _⟨$⟩_ = now ; cong = id λ x∼y → now-cong x∼y }
+  η A = record { _⟨$⟩_ = now ; cong = id λ x≡y → now-cong x≡y }
 
-  η↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → A [ x ∼ y ] → _↓_ {A} ((η A) ⟨$⟩ x) y
+  η↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → [ A ][ x ≡ y ] → [ A ][ ((η A) ⟨$⟩ x) ↓ y ]
-  η↓ {A} {x} {y} x∼y = now↓ x∼y
+  η↓ {A} {x} {y} x≡y = now↓ x≡y
 
-  η-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (η B ∘ f) ≋ (delayFun f ∘ η A)
+  η-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)
 
-  private
+  μ : ∀ {A : Setoid c (c ⊔ ℓ)} → ∣ (A ⊥ₛ) ⊥ₛ ∣ → ∣ (A ⊥ₛ) ∣
-    μ' : ∀ {A : Setoid c (c ⊔ ℓ)} → ∣ (A ⊥ₛ) ⊥ₛ ∣ → ∣ (A ⊥ₛ) ∣
+  μ {A} (now x) = x
-    μ' {A} (now x) = x
+  μ {A} (later x) = later (♯ μ {A} (♭ x))
-    μ' {A} (later x) = later (♯ μ' {A} (♭ x))
 
-    μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} → _↓_ {A ⊥ₛ} x y → A [ (μ' {A} x) ≈ y ]
+  μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} → [ A ⊥ₛ ][ x ↓ y ] → [ A ][ (μ {A} x) ≈ y ]
-    μ↓ {A} {now x} {y} (now↓ x≈y) = 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)
+  μ↓ {A} {later x} {y} (later↓ x↓y) = ≈-trans A (later≈ (♯ μ↓ x↓y)) (≈-sym A later-self)
 
-    -- TODO do delayFun and η in the same style as μ
+  μ-cong : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : (∣ A ∣ ⊥) ⊥} → [ A ⊥ₛ ][ x ≈ y ] → [ A ][ μ {A} x ≈ μ {A} y ]
+  μ-cong A {x} {now y} (↓≈ a≈b x↓a (now↓ y≈b)) = μ↓ (≡↓ (A ⊥ₛ) (≈-trans A a≈b (≈-sym A y≈b)) x↓a)
+  μ-cong A {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = ≈-sym A (μ↓ (≡↓ (A ⊥ₛ) (≈-trans A (≈-sym A a≈b) (≈-sym A x≈a)) (later↓ y↓b)))
+  μ-cong A {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ μ-cong A (↓≈ a≈b x↓a y↓b))
+  μ-cong A {later x} {later y} (later≈ x≈y) = later≈ (♯ μ-cong A (♭ x≈y))
 
-  μ : ∀ (A : Setoid c (c ⊔ ℓ)) → (A ⊥ₛ) ⊥ₛ ⟶ A ⊥ₛ
+  μₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → (A ⊥ₛ) ⊥ₛ ⟶ A ⊥ₛ
-  μ A = record { _⟨$⟩_ = μ' {A} ; cong = cong' }
+  μₛ A = record { _⟨$⟩_ = μ {A} ; cong = μ-cong A }
-    where
-      cong' : ∀ {x y : (∣ A ∣ ⊥) ⊥} → (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 : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (μₛ B ∘ liftFₛ (liftFₛ f)) ≋ (liftFₛ 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} {now y} nx≈ny = cong (liftFₛ 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 {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = later-eq (later≈ (♯ cong (liftFₛ f) (≈-sym A (μ↓ (≡↓ (A ⊥ₛ) (≈-trans A (≈-sym A a≈b) (≈-sym A x≈a)) y↓b)))))
-  μ-natural {A} {B} f {later x} {now y} (↓≈ a≈b (later↓ x↓a) (now↓ y≈b)) = ≈-sym (later-eq (later≈ (♯ ≈-sym (μ↓ (∼↓ (cong (delayFun f) (≈-trans a≈b (≈-sym y≈b))) (delayFun↓ (delayFun f) x↓a))))))
+  μ-natural {A} {B} f {later x} {now y} (↓≈ a≈b (later↓ x↓a) (now↓ y≈b)) = ≈-sym B (later-eq (later≈ (♯ ≈-sym B (μ↓ (≡↓ (B ⊥ₛ) (cong (liftFₛ f) (≈-trans A a≈b (≈-sym A y≈b))) (lift↓ (liftFₛ f) x↓a))))))
   μ-natural {A} {B} f {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ μ-natural f (↓≈ 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 : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} → _↓_ {A ⊥ₛ} x y → A [ (μ A) ⟨$⟩ x ≈ y ]
+  μ-assoc↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} → [ A ⊥ₛ ][ x ↓ y ] → [ A ][ (μₛ A) ⟨$⟩ x ≈ y ]
   μ-assoc↓ {A} {now x} {y} (now↓ x≈y) = x≈y
-  μ-assoc↓ {A} {later x} {y} (later↓ x↓y) = ≈-sym (later-eq (later≈ (♯ ≈-sym (μ-assoc↓ x↓y))))
+  μ-assoc↓ {A} {later x} {y} (later↓ x↓y) = ≈-sym A (later-eq (later≈ (♯ ≈-sym A (μ-assoc↓ x↓y))))
 
-
+  μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} {z : ∣ A ∣} → [ A ⊥ₛ ][ x ↓ y ] → [ A ][ y ↓ z ] → [ A ][ (μₛ A ⟨$⟩ x) ↓ z ]
-  -- TODO needs another μ↓-trans for when multiple μ's are concerned, i.e. a chain with 3 conditions...
+  μ↓-trans {A} {now x} {y} {z} (now↓ x≈y) y↓z = ≈↓ A (≈-sym A x≈y) y↓z
-  μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} {z : ∣ A ∣} → _↓_ {A ⊥ₛ} x y → _↓_ {A} y z → _↓_ {A} (μ A ⟨$⟩ x) z
-  μ↓-trans {A} {now x} {y} {z} (now↓ x≈y) y↓z = ≈↓ (≈-sym x≈y) y↓z
   μ↓-trans {A} {later x} {y} {z} (later↓ x↓y) y↓z = later↓ (μ↓-trans x↓y y↓z)
 
-  -- μ↓-trans² : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (∣ A ∣ ⊥))} {y : Delay (∣ A ∣ ⊥)} {z : ∣ A ∣ ⊥} → _↓_ {delaySetoid (A ⊥ₛ)} x y → _↓_ {A ⊥ₛ} y z → _↓_ {A ⊥ₛ} ((delayFun (μ A)) ⟨$⟩ x) z
+--   -- μ↓-trans² : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (∣ A ∣ ⊥))} {y : Delay (∣ A ∣ ⊥)} {z : ∣ A ∣ ⊥} → _↓_ {delaySetoid (A ⊥ₛ)} x y → _↓_ {A ⊥ₛ} y z → _↓_ {A ⊥ₛ} ((delayFun (μ A)) ⟨$⟩ x) z
-  -- μ↓-trans² {A} {now x} {y} {now x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {!   !} (μ↓-trans {!   !} {!  y↓z !}) (now↓ (∼-refl A)))
+--   -- μ↓-trans² {A} {now x} {y} {now x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {!   !} (μ↓-trans {!   !} {!  y↓z !}) (now↓ (∼-refl A)))
-  -- μ↓-trans² {A} {now x} {y} {later x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {!   !} {!   !} {!   !})
+--   -- μ↓-trans² {A} {now x} {y} {later x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {!   !} {!   !} {!   !})
-  -- μ↓-trans² {A} {later x} {y} {z} x↓y y↓z = {!   !}
+--   -- μ↓-trans² {A} {later x} {y} {z} x↓y y↓z = {!   !}
 
+  μ-assoc' : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ((∣ A ∣ ⊥)⊥)⊥} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼ (μₛ A ∘ μₛ (A ⊥ₛ)) ⟨$⟩ x ]
+  μ-assoc' {A} {now x} = ∼-refl A
+  μ-assoc' {A} {later x} = later∼ (♯ μ-assoc' {A} {♭ x})
 
-  μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ (delayFun (μ A))) ≋ (μ A ∘ μ (A ⊥ₛ))
+  -- TODO μ-assoc follows from this!!
-  μ-assoc {A} {now x} {now y} (↓≈ a≈b (now↓ x≈a) (now↓ y≈b)) = cong (μ A) (≈-trans x≈a (≈-trans a≈b (≈-sym y≈b)))
-  μ-assoc {A} {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = later-eq (later≈ (♯ cong (μ A) (≈-sym (μ↓ (∼↓ (≈-sym (≈-trans x≈a a≈b)) y↓b))))) -- y , liftF (μ A) (♭ x)
-  μ-assoc {A} {later x} {now y} (↓≈ {_} {_} {a} {b} (↓≈ c≈d a↓c b↓d) (later↓ x↓a) (now↓ y≈b)) = ≈-sym (later-eq (later≈ (♯ cong (μ A) {y} {liftF (μ A) (♭ x)} (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) {! delayFun↓ (μ A) {♭ x} x↓a  !})))) -- (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) (μ↓-trans {!  x↓a !} a↓c))
-  μ-assoc {A} {later x} {now y} (↓≈ (later≈ x≈y) (later↓ x↓a) (now↓ y≈b)) = {!   !}
-  μ-assoc {A} {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ μ-assoc (↓≈ a≈b x↓a y↓b))
-  μ-assoc {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ μ-assoc (♭ x≈y))
 
-  identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ A ∣ ⊥} {y : ∣ A ∣} → _↓_ {A} x y → _↓_ {A} ((μ A) ⟨$⟩ ((delayFun (η A)) ⟨$⟩ x)) y
+--   μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ (delayFun (μ A))) ≋ (μ A ∘ μ (A ⊥ₛ))
+--   μ-assoc {A} {now x} {now y} (↓≈ a≈b (now↓ x≈a) (now↓ y≈b)) = cong (μ A) (≈-trans x≈a (≈-trans a≈b (≈-sym y≈b)))
+--   μ-assoc {A} {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = later-eq (later≈ (♯ cong (μ A) (≈-sym (μ↓ (∼↓ (≈-sym (≈-trans x≈a a≈b)) y↓b))))) -- y , liftF (μ A) (♭ x)
+--   μ-assoc {A} {later x} {now y} (↓≈ {_} {_} {a} {b} (↓≈ c≈d a↓c b↓d) (later↓ x↓a) (now↓ y≈b)) = ≈-sym (later-eq (later≈ (♯ cong (μ A) {y} {liftF (μ A) (♭ x)} (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) {! delayFun↓ (μ A) {♭ x} x↓a  !})))) -- (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) (μ↓-trans {!  x↓a !} a↓c))
+--   μ-assoc {A} {later x} {now y} (↓≈ (later≈ x≈y) (later↓ x↓a) (now↓ y≈b)) = {!   !}
+--   μ-assoc {A} {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ μ-assoc (↓≈ a≈b x↓a y↓b))
+--   μ-assoc {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ μ-assoc (♭ x≈y))
+
+  identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ 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 ∘ delayFun (η A)) ≋ idₛ
+  identityˡ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ liftFₛ (η A)) ≋ idₛ
   identityˡ {A} {now x} {y} x≈y = x≈y
-  identityˡ {A} {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (∼-refl A) (later↓ (identityˡ↓ x↓a)) (now↓ (∼-trans A y∼b (∼-sym A a∼b)))
+  identityˡ {A} {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (≡-refl A) (later↓ (identityˡ↓ x↓a)) (now↓ (≡-trans A y∼b (≡-sym A a∼b)))
   identityˡ {A} {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ identityˡ (↓≈ a∼b x↓a y↓b))
   identityˡ {A} {later x} {.(later _)} (later≈ x≈y) = later≈ (♯ identityˡ (♭ x≈y))
 
-  identityʳ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ η (A ⊥ₛ)) ≋ idₛ
+  identityʳ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ η (A ⊥ₛ)) ≋ idₛ
   identityʳ {A} {now x} {y} x≈y = x≈y
   identityʳ {A} {later x} {y} x≈y = x≈y
 
@@ -249,14 +250,14 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
   delayMonad = record
     { F = record
       { F₀ = _⊥ₛ
-      ; F₁ = delayFun
+      ; F₁ = liftFₛ
-      ; identity = delayFun-id
+      ; identity = lift-id
-      ; homomorphism = delayFun-comp
+      ; homomorphism = λ {X} {Y} {Z} {f} {g} → lift-comp {X} {Y} {Z} {f} {g}
-      ; F-resp-≈ = delayFun-resp-≈
+      ; F-resp-≈ = λ {A} {B} {f} {g} → lift-resp-≈ {A} {B} {f} {g}
       }
     ; η = ntHelper (record { η = η ; commute = η-natural })
-    ; μ = ntHelper (record { η = μ ; commute = μ-natural })
+    ; μ = ntHelper (record { η = μₛ ; commute = μ-natural })
-    ; assoc = μ-assoc
+    ; assoc = {!   !}
     ; sym-assoc = {!   !}
     ; identityˡ = identityˡ
     ; identityʳ = identityʳ