Work on delay example

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

@@ -101,8 +101,53 @@ module Monad.Instance.K.Instance.Delay' {c ℓ} where
       ≈-trans a b (later c) a≈b b≈c = later-trans a≈b b≈c
 
   delay-setoid : Setoid c ℓ → Setoid c ℓ
-  delay-setoid A = record { Carrier = Delay Carrier ; _≈_ = _≈_ {A} ; isEquivalence = record { refl = λ {x} → ≈-refl x ; sym = λ {x y} → ≈-sym x y ; trans = λ {x y z} → ≈-trans x y z } }
+  delay-setoid A = record { Carrier = Delay Carrier ; _≈_ = _≈_ ; isEquivalence = record { refl = λ {x} → ≈-refl x ; sym = λ {x y} → ≈-sym x y ; trans = λ {x y z} → ≈-trans x y z } }
     where 
       open Setoid A using (Carrier)
-      open Equality
+      open Equality {A}
+
+  module Equality' {A : Setoid 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 _↓_ : Delay C → C → Set ℓ where
+      now↓ : ∀ {x y} (eq : x ∼ y) → now x ↓ y
+      later↓ : ∀ {x y} (eq : ♭ x ↓ y) → later x ↓ y
+
+    unique↓ : ∀ {c : Delay C} {x y : C} → c ↓ x → c ↓ y → x ∼ y
+    unique↓ (now↓ eq₁) (now↓ eq₂) = ∼-trans (∼-sym eq₁) eq₂
+    unique↓ (later↓ p) (later↓ q) = unique↓ p q
+
+    data _≈_ : Delay C → Delay C → Set (c ⊔ ℓ) where
+      ↓≈ : ∀ {x y a b} (a∼b : a ∼ b) (x↓z : x ↓ a) (y↓z : y ↓ b) → x ≈ y
+      later≈ : ∀ {x y} → (∞ (♭ x ≈ ♭ y)) → later x ≈ later y
+
+    refl' : ∀ {x} → x ≈ x
+    refl' {now x} = ↓≈ ∼-refl (now↓ ∼-refl) (now↓ ∼-refl)
+    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' (later≈ x≈y) = later≈ (♯ sym' (♭ x≈y))
+
+    -- TODO needed for trans'
+    ≈↓ : ∀ {x y : Delay C} {z : C} → x ≈ y → x ↓ z → y ↓ z
+    ≈↓ x≈y x↓z = {!   !}
+    -- ≈↓ (↓≈ a(now↓ refl) q) (now↓ refl) = q
+    -- ≈↓ (↓≈ (later↓ p) r) (later↓ q) with unique↓ p q
+    -- ≈↓ (↓≈ (later↓ p) r) (later↓ q) | refl = r
+    -- ≈↓ (later≈ p) (later↓ q) = later↓ (≈↓ (♭ p) q)
+
+    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
+    ...                                 | b∼c = ↓≈ (∼-trans (∼-trans a∼b b∼c) c∼d) x↓a z↓d
+    trans' (↓≈ a∼b x↓a (later↓ y↓b)) (later≈ x) = ↓≈ a∼b x↓a {!   !}
+    trans' (later≈ x) (↓≈ a∼b x↓a y↓b) = {!   !}
+    trans' (later≈ x) (later≈ y) = {!   !} 
+    
+  delay-setoid' : Setoid c ℓ → Setoid c (c ⊔ ℓ)
+  delay-setoid' A = record { Carrier = Delay Carrier ; _≈_ = _≈_ ; isEquivalence = record { refl = λ {x} → {!   !} ; sym = λ {x y} → {!   !} ; trans = λ {x y z} → {!   !} } }
+    where 
+      open Setoid A using (Carrier)
+      open Equality' {A}
 ```

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

@@ -49,6 +49,21 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
   never : ∀ {A : Set c} → Delay A
   node (never {A}) = inj₂ never
 
+  module Equality {A : Setoid c ℓ} where
+    open Setoid A using () renaming (Carrier to C; _≈_ to _∼_)
+    data _↓_ : Delay C → C → Set (c ⊔ ℓ) where
+      now↓ : ∀ {x y} (p : x ∼ y) → now x ↓ y
+      later↓ : ∀ {x y} (p : _↓_ x y) → later x ↓ y
+
+    data _≈_ : Delay C → Delay C → Set (c ⊔ ℓ) where
+      ↓≈ : ∀ {x y z} → x ↓ z → y ↓ z → x ≈ y
+      later-≈ : ∀ {x y} → x ≈ y → later x ≈ later y
+
+    refl : ∀ {x} → x ≈ x
+    refl {x} with node x 
+    ...             | inj₁ z = ↓≈ {!   !} {!   !}
+    ...             | inj₂ z = {!   !}
+
   -- first try
   delay-eq-strong : ∀ (A : Setoid c ℓ) → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ
   delay-eq-strong A x y with node x | node y
@@ -136,7 +151,7 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
       ...                             | inj₂ x    | inj₁ y | inj₂ z | eq₁    | eq₂ = trans' eq₁ eq₂
       ...                             | inj₁ x    | inj₁ y | inj₂ z | eq₁    | eq₂ = trans' (now-cong eq₁) eq₂ -- trans' (now-cong eq₁) eq₂
       ...                             | inj₂ x    | inj₂ y | inj₁ z | eq₁    | eq₂ = trans' eq₁ eq₂
-      ...                             | inj₁ x    | inj₂ y | inj₁ z | eq₁    | eq₂ = {! trans' eq₁ eq₂  !} -- now-inj {A} {x} {z} (trans' eq₁ eq₂)
+      ...                             | inj₁ x    | inj₂ y | inj₁ z | eq₁    | eq₂ = {!  !} -- now-inj {A} {x} {z} (trans' eq₁ eq₂)
       ...                             | inj₂ x    | inj₁ y | inj₁ z | eq₁    | eq₂ = trans' eq₁ (now-cong eq₂)
       ...                             | inj₁ x    | inj₁ y | inj₁ z | eq₁    | eq₂ = IsEquivalence.trans (Setoid.isEquivalence A) eq₁ eq₂
 ```