minor and add sergeys suggestion

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

@@ -1,7 +1,7 @@
 ```agda 
 {-# OPTIONS --allow-unsolved-metas --guardedness #-}
 
-open import Level
+open import Level renaming (zero to ℓ-zero; suc to ℓ-suc)
 open import Function.Equality as SΠ renaming (id to idₛ)
 open import Relation.Binary
 open import Data.Sum using (_⊎_; inj₁; inj₂)
@@ -12,6 +12,8 @@ open import Function using (id)
 open import Categories.Monad
 open import Categories.Category.Instance.Setoids
 open import Categories.NaturalTransformation hiding (id)
+open import Data.Product
+open import Data.Nat using (ℕ; suc; zero)
 
 module Monad.Instance.K.Instance.D {c ℓ} where
 
@@ -173,7 +175,20 @@ module Bisimilarity (A : Setoid c (c ⊔ ℓ)) where
 
   force≈ (≈′-trans x≈′y y≈′z) = ≈-trans (force≈ x≈′y) (force≈ y≈′z)
 
-open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_])
+  mutual
+    data _≲_ : Delay ∣ A ∣ → Delay ∣ A ∣ → Set (c ⊔ ℓ) where
+      ↓≲     : ∀ {y a} (y↓a : y ↓ a) → now a ≲ y
+      later≲ : ∀ {x y} (x≈y : force x ≲′ force y) → later x ≲ later y
+
+    record _≲′_ (x y : Delay ∣ A ∣) : Set (c ⊔ ℓ) where
+      coinductive
+      
+      field
+        force≲ : x ≲ y
+
+  open _≲′_ public
+
+open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_]; _≲_ to [_][_≲_]; _≲′_ to [_][_≲′_])
 
 
 module DelayMonad where
@@ -351,4 +366,54 @@ module DelayMonad where
     ; identityˡ = identityˡ
     ; identityʳ = identityʳ
     }
+
+module extra {A : Setoid c (c ⊔ ℓ)} where
+  ≲→≈  : {x y : Delay ∣ A ∣}  → [ A ][ x ≲ y ] → [ A ][ x ≈ y ]
+  ≲→≈′ : {x y : Delay ∣ A ∣} → [ A ][ x ≲′ y ] → [ A ][ x ≈′ y ]
+
+  ≲→≈ (↓≲ y↓a)     = ↓≈ (≡-refl A) (now↓ (≡-refl A)) y↓a
+  ≲→≈ (later≲ x≈y) = later≈ (≲→≈′ x≈y)
+
+  force≈ (≲→≈′ x≲′y) = ≲→≈ (force≲ x≲′y)
+
+  race : Delay ∣ A ∣ → Delay ∣ A ∣ → Delay ∣ A ∣
+  race′ : Delay′ ∣ A ∣ → Delay′ ∣ A ∣ → Delay′ ∣ A ∣
+
+  race (now a) _ = now a
+  race (later x) (now a) = now a
+  race (later x) (later y) = later (race′ x y)
+
+  force (race′ x y) = race (force x) (force y)
+
+  ≈→≲₀ : ∀ {x y a b} (x↓a : [ A ][ x ↓ a ]) (y↓b : [ A ][ y ↓ b ]) (a≡b : [ A ][ a ≡ b ]) → [ A ][ race x y ≲ y ]
+  ≈→≲₀ (now↓ x≡a) y↓b a≡b = ↓≲ (≡↓ A (≡-sym A (≡-trans A x≡a a≡b)) y↓b)
+  ≈→≲₀ (later↓ x↓a) (now↓ x≡y) a≡b = ↓≲ (now↓ (≡-refl A))
+  ≈→≲₀ (later↓ x↓a) (later↓ y↓b) a≡b = later≲ (record { force≲ = ≈→≲₀ x↓a y↓b a≡b })
+
+  ≈→≲ : {x y : Delay ∣ A ∣} → [ A ][ x ≈ y ] → [ A ][ race x y ≲ y ]
+  ≈′→≲′ : {x y : Delay ∣ A ∣} → [ A ][ x ≈′ y ] → [ A ][ race x y ≲′ y ]
+
+  ≈→≲ (↓≈ a≡b x↓a y↓b) = ≈→≲₀ x↓a y↓b a≡b
+  ≈→≲ (later≈ x≈y) = later≲ (≈′→≲′ x≈y)
+
+  force≲ (≈′→≲′ x≈′y) = ≈→≲ (force≈ x≈′y)
+
+  delta₀  : {x : Delay ∣ A ∣} {a : ∣ A ∣}  → (x↓a : [ A ][ x ↓ a ]) → ℕ
+  delta₀ {x} (now↓ x≡y) = zero
+  delta₀ (later↓ x↓a)   = suc (delta₀ x↓a)
+
+  delta  : {x y : Delay ∣ A ∣} → [ A ][ x ≲ y ] → Delay (∣ A ∣ × ℕ)
+  delta′ : {x y : Delay ∣ A ∣} → [ A ][ x ≲′ y ] → Delay′ (∣ A ∣ × ℕ)
+
+  delta (↓≲ {x}{a} x↓a) = now (a , delta₀ x↓a)
+  delta (later≲ x≲′y)   = later (delta′ x≲′y)
+
+  force (delta′ x≲′y) = delta (force≲ x≲′y)
+
+  ι : ∣ A ∣ × ℕ → Delay ∣ A ∣
+  ι′ : ∣ A ∣ × ℕ → Delay′ ∣ A ∣
+  force (ι′ p) = ι p
+  ι (x , zero)  = now x
+  ι (x , suc n) = later (ι′ (x , n))
+
 ```

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

@@ -14,6 +14,7 @@ open import FreeObject
 open import Categories.FreeObjects.Free
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Categories.Category.Instance.Properties.Setoids.Choice using ()
+open import Data.Product.Relation.Binary.Pointwise.NonDependent
 ``` 
 -->
 
@@ -176,7 +177,13 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
     helper₁ (later x) = inj₂ (force x)
     -- -- setoid-morphism that preserves strong-bisimilarity
     helper : Delayₛ' A ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ' A
-    helper = record { _⟨$⟩_ = helper₁ ; cong = {!   !} }
+    helper = record { _⟨$⟩_ = helper₁ ; cong = strong-cong }
+      where
+        strong-cong : ∀ {x y : Delay ∣ A ∣} → [ A ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ helper₁ x ≡ helper₁ y ]
+        strong-cong {.(now _)} {.(now _)} (now∼ x≡y) = cong (inj₁ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong f x≡y)
+        strong-cong {.(later _)} {.(later _)} (later∼ x∼y) = cong (inj₂ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (force∼ x∼y)
+
+  <<_>> = Elgot-Algebra-Morphism.h
 
   freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
   freeAlgebra A = record 
@@ -184,6 +191,30 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
     ; η = ηₛ A
     ; _* = delay-lift 
     ; *-lift = λ {B} f {x} {y} x≡y → ≡-trans ⟦ B ⟧ (Elgot-Algebra.#-Fixpoint B (now∼ x≡y)) (≡-refl ⟦ B ⟧) 
-    ; *-uniq = λ {B} f g eq {x} {y} x≡y → {!  !} -- TODO pattern match x and y
+    ; *-uniq = λ {B} f g eq {x} {y} x≡y → *-uniq' {B} f g eq {x} {y} x≡y
     }
+    where
+      *-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g : Elgot-Algebra-Morphism (delay-algebras A) B) (eq : (<< g >> ∘ (ηₛ A)) ≋ f) {x y : Delay ∣ A ∣} → [ A ][ x ≈ y ] → [_][_≡_] (⟦ B ⟧) ((<< g >>) ⟨$⟩ x) ((<< delay-lift f >>) ⟨$⟩ y)
+      *-uniq' {B} f g eq {now x} {now y} x≡y = ≡-trans ⟦ B ⟧ (eq {x} {y} (now-inj x≡y)) (≡-refl ⟦ B ⟧)
+      *-uniq' {B} f g eq {now x} {later y} x≡y = {!   !}
+      *-uniq' {B} f g eq {later x} {now y} x≡y = {!   !}
+      *-uniq' {B} f g eq {later x} {later y} x≡y = {!   !} 
+
+
+
+  -- TODO stability might be proven more general, since Setoids is CCC (whatever is easier)
+
+  delay-stability : ∀ (Y : Setoid ℓ ℓ) (X : Setoid ℓ ℓ) (B : Elgot-Algebra) (f : X ×ₛ Y ⟶ ⟦ B ⟧) → X ×ₛ Delayₛ Y ⟶ ⟦ B ⟧
+  delay-stability Y X B f = {!   !}
+
+  isStableFreeElgotAlgebra : ∀ (A : Setoid ℓ ℓ) → IsStableFreeElgotAlgebra (freeAlgebra A)
+  isStableFreeElgotAlgebra A = record 
+    { [_,_]♯ = λ {X} B f → delay-stability A X B f
+    ; ♯-law = {!   !} 
+    ; ♯-preserving = {!   !} 
+    ; ♯-unique = {!   !} 
+    }
+
+  delayK : MonadK
+  delayK = record { freealgebras = freeAlgebra ; stable = isStableFreeElgotAlgebra }
 ```