minor

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

@@ -22,7 +22,7 @@ open import Categories.NaturalTransformation using (ntHelper)
 open import Function.Base using (id)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_)
-open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
+open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax; _×_)
 ```
 -->
 
@@ -50,19 +50,37 @@ module Monad.Instance.K.Instance.DelayRecord {c ℓ} where
   node (never {A}) = inj₂ never
 
   module Equality {A : Setoid c ℓ} where
-    open Setoid A using () renaming (Carrier to C; _≈_ to _∼_)
+    open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≈_]; refl to ≈-refl)
-    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
+    record _↓_ (x : Delay ∣ A ∣) (y : ∣ A ∣) : Set (c ⊔ ℓ) where
-      ↓≈ : ∀ {x y z} → x ↓ z → y ↓ z → x ≈ y
+      coinductive
-      later-≈ : ∀ {x y} → x ≈ y → later x ≈ later y
+      field
+        now↓ : ∀ {z} → (node x ≡ inj₁ z) → [ A ][ y ≈ z ]
+        -- later↓ : ∀ {z} → (node x ≡ inj₂ z) → z ↓ y → x ↓ y
+
+    -- data _↓_ : Delay ∣ A ∣ → ∣ A ∣ → Set (c ⊔ ℓ) where
+    --   now↓ : ∀ {x y} (p : node x ≡ inj₁ y) → x ↓ y
+    --   later↓ : ∀ {x y z} (p : node x ≡ inj₂ y) (q : _↓_ y z) → x ↓ z
+    --   -- later↓ : ∀ {x y} (p : _↓_ x y) → later x ↓ y
+
+    record _≈_ (x y : Delay ∣ A ∣) : Set (c ⊔ ℓ) where
+      coinductive
+      field
+        ↓≈ : ∀ {z} → (x ↓ z × y ↓ z)
+
+    open _≈_
 
     refl : ∀ {x} → x ≈ x
-    refl {x} with node x 
+    ↓≈ (refl {x}) {z} = record { now↓ = λ {y} eq → {!   !} } , {!   !}
-    ...             | inj₁ z = ↓≈ {!   !} {!   !}
+
-    ...             | inj₂ z = {!   !}
+    -- data _≈_ : Delay ∣ A ∣ → Delay ∣ A ∣ → Set (c ⊔ ℓ) where
+    --   ↓≈ : ∀ {x y z} → x ↓ z → y ↓ z → x ≈ y
+    --   later-≈ : ∀ {x y a b} → node x ≡ inj₂ a → node y ≡ inj₂ b → a ≈ b → x ≈ y
+
+    -- refl : ∀ {x} → x ≈ x
+    -- refl {x} with node x in eqx
+    -- ...             | inj₁ z = ↓≈ (now↓ eqx) (now↓ eqx)
+    -- ...             | inj₂ z = later-≈ eqx eqx {!   !}
 
   -- first try
   delay-eq-strong : ∀ (A : Setoid c ℓ) → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ

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

@@ -36,6 +36,13 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
     {x : ∣ X ∣} {y : ∣ Y ∣} → (X ⊎ₛ Y) [ inj₁ x ∼ inj₂ y ] → Z
   conflict X Y ()
   
+  iter' : ∀ {A X : Set ℓ} → (X → A ⊥ ⊎ X) → A ⊥ ⊎ X → A ⊥
+  iter' {A} {X} f (inj₁ x) = x
+  iter' {A} {X} f (inj₂ y) = later (♯ iter' {A} {X} f (f y))
+
+  -- TODO works!!
+  _# : ∀ {A X : Set ℓ} → (X → A ⊥ ⊎ X) → X → A ⊥
+  (f #) x = iter' f (inj₂ x)
 
   iter : ∀ {A X : Setoid ℓ ℓ} → (∣ X ∣ → (∣ A ∣ ⊥ ⊎ ∣ X ∣)) → ∣ X ∣ → ∣ A ∣ ⊥
   iter {A} {X} f x with f x