The Delay Monad (as a Setoid)

In this module we will define the delay monad, together with two notions of equality between computations, strong and weak bisimilarity. We will show that the setoid with weak bisimilarity extends to a monad (so does the one with strong bisimilarity, but this is not relevant for the later developments)

module Monad.Instance.Setoids.Delay {c ℓ} where
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)

Defining the Delay Datatype

We start out by defining Delay as a mutual (co-)inductive type:

module _ (A : Set c) where
  mutual
    data Delay : Set c where
      now   : A      → Delay
      later : Delay′ → Delay
    record Delay′ : Set c where
      coinductive
      constructor dela
      field force : Delay
  open Delay′ public

  -- A non-terminating computation
  never : Delay
  never = later λ { .force → never }

  -- Removes a later constructor, if possible.
  drop-later : Delay → Delay
  drop-later (now   x) = now x
  drop-later (later x) = force x

First we define strong bisimilarity and show that it is an equivalence relation:

module Bisimilarity (A : Setoid c (c ⊔ ℓ)) where
  -- adapted from https://www.cse.chalmers.se/∼nad/listings/delay-monad/Delay-monad.Bisimilarity.html

  mutual
    data _∼_ : Delay ∣ A ∣ → Delay ∣ A ∣ → Set (c ⊔ ℓ) where
      now∼    : ∀ {x y} → [ A ][ x ≡ y ] → now x ∼ now y
      later∼  : ∀ {x y} → force x ∼′ force y → later x ∼ later y
    record _∼′_ (x y : Delay ∣ A ∣) : Set (c ⊔ ℓ) where
      coinductive
      constructor delay∼
      field force∼ : x ∼ y
  open _∼′_ public

  -- strong bisimilarity of now and later leads to a clash
  now∼later : ∀ {ℓ'}{Z : Set ℓ'}{x : ∣ A ∣}{y : Delay′ ∣ A ∣} → now x ∼ later y → Z
  now∼later ()

  ∼-refl  : ∀ {x : Delay ∣ A ∣} → x ∼ x
  ∼-refl {now x}   = now∼ (≡-refl A) 
  ∼-refl {later x} = later∼ λ { .force∼ → ∼-refl }

  ∼-sym  : ∀ {x y : Delay ∣ A ∣} → x ∼ y → y ∼ x
  ∼-sym (now∼ x≡y)     = now∼ (≡-sym A x≡y)
  ∼-sym (later∼ fx∼fy) = later∼ λ { .force∼ → ∼-sym (force∼ fx∼fy) }

  ∼-trans  : ∀ {x y z : Delay ∣ A ∣} → x ∼ y → y ∼ z → x ∼ z
  ∼-trans (now∼ x≡y)   (now∼ y≡z)   = now∼ (≡-trans A x≡y y≡z)
  ∼-trans (later∼ x∼y) (later∼ y∼z) = later∼ λ { .force∼ → ∼-trans (force∼ x∼y) (force∼ y∼z) }

Next we define weak-bisimilarity and proof some helper lemmas to finally show that it is an equivalence relation:

  data _↓_ : Delay ∣ A ∣ → ∣ A ∣ → Set (c ⊔ ℓ) where
    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 ]
  unique↓ (now↓ a≡x)    (now↓ a≡y)    = ≡-trans A (≡-sym A a≡x) a≡y
  unique↓ (later↓ fb↓x) (later↓ fb↓y) = unique↓ fb↓x fb↓y

  mutual
    data _≈_ : Delay ∣ A ∣ → Delay ∣ A ∣ → Set (c ⊔ ℓ) where
      ↓≈     : ∀ {x y a b} (a≡b : [ A ][ a ≡ b ]) (x↓a : x ↓ a) (y↓b : y ↓ b) → x ≈ y
      later≈ : ∀ {x y} (x≈y : force x ≈′ force y) → later x ≈ later y
    record _≈′_ (x y : Delay ∣ A ∣) : Set (c ⊔ ℓ) where
      coinductive
      constructor delay≈
      field force≈ : x ≈ y
  open _≈′_ public

  ≡↓ : ∀ {x y : ∣ A ∣} {z : Delay ∣ A ∣} → [ A ][ x ≡ y ] → z ↓ x → z ↓ 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 : Delay ∣ A ∣ } {a : ∣ A ∣} → x ≈ y → x ↓ a → y ↓ a
  ≈↓ (↓≈ c≡b (now↓ x≡c) y↓b)   (now↓ x≡a)    = ≡↓ (≡-trans A (≡-trans A (≡-sym A c≡b) (≡-sym A x≡c)) x≡a) y↓b
  ≈↓ (↓≈ c≡b (later↓ x↓c) y↓b) (later↓ x↓a)  = ≡↓ (≡-trans A (≡-sym A c≡b) (≡-sym A (unique↓ x↓a x↓c))) y↓b
  ≈↓ (later≈ fx≈fy)            (later↓ fx↓a) = later↓ (≈↓ (force≈ fx≈fy) fx↓a)

  ≈-refl  : ∀ {x : Delay ∣ A ∣} → x ≈ x
  ≈-refl {now x}   = ↓≈ (≡-refl A) (now↓ (≡-refl A)) (now↓ (≡-refl A))
  ≈-refl {later x} = later≈ λ { .force≈ → ≈-refl }


  ≈-sym  : ∀ {x y : Delay ∣ A ∣} → x ≈ y → y ≈ x
  ≈-sym (↓≈ a≡b x↓a y↓b) = ↓≈ (≡-sym A a≡b) y↓b x↓a
  ≈-sym (later≈ x≈y)     = later≈ λ { .force≈ → ≈-sym (force≈ x≈y) }


  ≈-trans  : ∀ {x y z : Delay ∣ A ∣} → x ≈ y → y ≈ z → x ≈ z
  ≈-trans (↓≈ a≡b x↓a y↓b) (↓≈ c≡d y↓c z↓d)           = ↓≈ (≡-trans A (≡-trans A a≡b (unique↓ y↓b y↓c)) c≡d) x↓a z↓d
  ≈-trans (↓≈ a≡b z↓a      (later↓ x↓b)) (later≈ x≈y) = ↓≈ a≡b z↓a (later↓ (≈↓ (force≈ x≈y) x↓b))
  ≈-trans (later≈ x≈y)     (↓≈ a≡b (later↓ y↓a) z↓b)  = ↓≈ a≡b (later↓ (≈↓ (≈-sym (force≈ x≈y)) y↓a)) z↓b
  ≈-trans (later≈ x≈y)     (later≈ y≈z)               = later≈ λ { .force≈ → ≈-trans (force≈ x≈y) (force≈ y≈z) } 

Additionally we can define a relation ≲ between computations where x ≲ y iff x terminates faster than y:

  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
      constructor delay≲
      field
        force≲ : x ≲ y
  open _≲′_ public

Delay is a Monad

First we define the functor action and the monad multiplication. The monad unit is of course the now constructor.

module DelayMonad where
  -- The functor action of Delay
  liftF : ∀ {A B : Set c} → (A → B) → Delay A → Delay B
  liftF f (now x)   = now (f x)
  liftF f (later x) = later λ { .force → liftF f (force x) }

  -- Monad multiplication
  μ : ∀ {A : Setoid c (c ⊔ ℓ)} → Delay (Delay ∣ A ∣) → Delay ∣ A ∣
  μ {A} (now x) = x
  μ {A} (later x) = later λ { .force → μ {A} (force x) }
open DelayMonad

Some helpers for reasoning with setoid morphisms:

open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_]; _≲_ to [_][_≲_]; _≲′_ to [_][_≲′_])
open _⟶_ using (cong) renaming (to to <_>)
-- pointwise equality between setoid morphisms:
_≐_ : ∀ {c' ℓ'} {A B : Setoid c' ℓ'} → A ⟶ B → A ⟶ B → Set (c' ⊔ ℓ')
_≐_ {c'} {ℓ'} {A} {B} f g = Setoid._≈_ (A ⇨ B) f g

Next we show that (Delay, _∼_) is a monad:

module DelayMonad∼ where
  private
    Delay∼ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
    Delay∼ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } }

    -- now is a setoid morphism
    η∼ : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ Delay∼ A
    η∼ A = record { to = now ; cong = nowF∼-cong }  
      where
      nowF∼-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → [ A ][ x ≡ y ] → [ A ][ now x ∼ now y ]
      nowF∼-cong {A} {x} {y} x≡y = now∼ x≡y

    -- μ is a setoid morphism
    μ∼ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delay∼ (Delay∼ A) ⟶ Delay∼ A
    μ∼ A = record { to = μ {A} ; cong = μ∼-cong A }
      where
        μ∼-cong : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delay∼ A ][ x ∼ y ] → [ A ][ μ {A} x ∼ μ {A} y ]
        μ∼-cong A {.(now _)}   {.(now _)}   (now∼ x∼y)   = x∼y
        μ∼-cong A {.(later _)} {.(later _)} (later∼ x∼y) = later∼ λ { .force∼ → μ∼-cong A (force∼ x∼y) }

    -- liftF is a setoid-morphism
    liftF∼ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delay∼ A ⟶ Delay∼ B
    liftF∼ {A} {B} f = record { to = liftF < f > ; cong = liftF∼-cong }
      where
      liftF∼-cong : ∀ {x y} → [ A ][ x ∼ y ] → [ B ][ liftF < f > x ∼ liftF < f > y ]
      liftF∼-cong {.(now _)}   {.(now _)}   (now∼ x≡y)   = cong (η∼ B) (cong f x≡y)
      liftF∼-cong {.(later _)} {.(later _)} (later∼ x∼y) = later∼ λ { .force∼ → liftF∼-cong (force∼ x∼y) }

    -- η∼ is natural
    η∼-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (η∼ B ∘ f) ≐ (liftF∼ f ∘ η∼ A)
    η∼-natural {A} {B} f {x} = cong (η∼ B) (cong f (≡-refl A))
    
    -- μ∼ is natural
    μ∼-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (μ∼ B ∘ liftF∼ (liftF∼ f)) ≐ (liftF∼ f ∘ μ∼ A)
    μ∼-natural {A} {B} f {now x}   = ∼-refl B
    μ∼-natural {A} {B} f {later x} = later∼ λ { .force∼ → μ∼-natural {A} {B} f {force x} }

    -- liftF is a homomorphism
    liftF∼-comp : ∀ {A B C : Setoid c (c ⊔ ℓ)} {f : A ⟶ B} {g : B ⟶ C} {x : Delay ∣ A ∣} → [ C ][ liftF (< g > ∘′ < f >) x ∼ (liftF < g > ∘′ liftF < f >) x ]
    liftF∼-comp {A} {B} {C} {f} {g} {now x}   = cong (η∼ C) (cong g (cong f (≡-refl A)))
    liftF∼-comp {A} {B} {C} {f} {g} {later x} = later∼ λ { .force∼ → liftF∼-comp {A} {B} {C} {f} {g} {force x} }

    -- liftF preserves identities
    liftF∼-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (liftF∼ (idₛ A)) ≐ (idₛ (Delay∼ A))
    liftF∼-id {A} {now x} = ∼-refl A
    liftF∼-id {A} {later x} = later∼ λ { .force∼ → liftF∼-id {A} }

    -- liftF respects strong bisimilarity
    liftF∼-resp : ∀ {A B : Setoid c (c ⊔ ℓ)} {f g : A ⟶ B} → f ≐ g → liftF∼ f ≐ liftF∼ g
    liftF∼-resp {A} {B} {f} {g} f≐g {now x}   = cong (η∼ B) f≐g
    liftF∼-resp {A} {B} {f} {g} f≐g {later x} = later∼ λ { .force∼ → liftF∼-resp {A} {B} {f} {g} f≐g }

    -- μ∼ is associative
    μ∼-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μ∼ A ∘ (liftF∼ (μ∼ A))) ⟨$⟩ x ∼ (μ∼ A ∘ μ∼ (Delay∼ A)) ⟨$⟩ x ]
    μ∼-assoc {A} {now x}   = ∼-refl A
    μ∼-assoc {A} {later x} = later∼ λ { .force∼ → μ∼-assoc {A} {force x} }

    -- η∼ is a left identity of μ∼
    identityˡ∼ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay ∣ A ∣} → [ A ][ (μ∼ A ∘ liftF∼ (η∼ A)) ⟨$⟩ x ∼ x ]
    identityˡ∼ {A} {now x}   = ∼-refl A
    identityˡ∼ {A} {later x} = later∼ λ { .force∼ → identityˡ∼ {A} {force x} }

    -- η∼ is a right identity of μ∼
    identityʳ∼ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ∼ A ∘ η∼ (Delay∼ A)) ≐ idₛ (Delay∼ A)
    identityʳ∼ {A} {now x}   = ∼-refl A
    identityʳ∼ {A} {later x} = ∼-refl A

  delayMonad∼ : Monad (Setoids c (c ⊔ ℓ))
  delayMonad∼ = record
    { F         = record
      { F₀           = Delay∼
      ; F₁           = liftF∼
      ; identity     = liftF∼-id
      ; homomorphism = λ {X} {Y} {Z} {f} {g} → liftF∼-comp {X} {Y} {Z} {f} {g}
      ; F-resp-≈     = λ {A} {B} {f} {g} → liftF∼-resp {A} {B} {f} {g}
      }
    ; η         = ntHelper (record { η = η∼ ; commute = η∼-natural })
    ; μ         = ntHelper (record { η = μ∼ ; commute = μ∼-natural })
    ; assoc     = λ {A} {x} → μ∼-assoc {A} {x}
    ; sym-assoc = λ {A} {x} → ∼-sym A (μ∼-assoc {A} {x})
    ; identityˡ = identityˡ∼
    ; identityʳ = identityʳ∼
    }

open DelayMonad∼
open Monad delayMonad∼ using () renaming (F to Delay∼; η to η∼; μ to μ∼; assoc to assoc∼; sym-assoc to sym-assoc∼; identityˡ to identityˡ∼; identityʳ to identityʳ∼)

Then showing that (Delay, _≈_) is a monad is easy, since the monad laws follow from strong bisimilarity:

module DelayMonad≈ where
  private
    Delay≈ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
    Delay≈ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_≈_] A ; isEquivalence = record { refl = ≈-refl A ; sym = ≈-sym A ; trans = ≈-trans A } }

  -- Strong bisimilarity implies weak bisimilarity
  ∼⇒≈ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay ∣ 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≈ λ { .force≈ → ∼⇒≈ (force∼ x∼y) }

  -- force x is weakly bisimilar to later x
  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}

  -- now is injective
  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))

  private
    -- now is a setoid morphism
    η≈ : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ Delay≈ A
    η≈ A = record { to = now ; cong = now≈-cong }  
      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))

    -- liftF≈ is a setoid morphism
    liftF≈ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delay≈ A ⟶ Delay≈ B
    liftF≈ {A} {B} f = record { to = liftF < f > ; cong = liftF≈-cong f }
      where
      lift↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : Delay ∣ A ∣} {b : ∣ A ∣} → [ A ][ x ↓ b ] → [ B ][ (liftF (< f >) x) ↓ (f ⟨$⟩ b) ]
      lift↓ {A} {B} f {now x}   {b} (now↓ x≡a)   = now↓ (cong f x≡a)
      lift↓ {A} {B} f {later x} {b} (later↓ x↓b) = later↓ (lift↓ f x↓b)
      liftF≈-cong : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x y : Delay ∣ A ∣} → [ A ][ x ≈ y ] → [ B ][ liftF < f > x ≈ liftF < f > y ]
      liftF≈-cong {A} {B} f {now x}   {now y}   (↓≈ a≡b (now↓ x≡a) (now↓ y≡b))     = ↓≈ (cong f a≡b) (now↓ (cong f x≡a)) (now↓ (cong f y≡b))
      liftF≈-cong {A} {B} f {now x}   {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b))   = ↓≈ (cong f a≡b) (now↓ (cong f x≡a)) (later↓ (lift↓ f y↓b))
      liftF≈-cong {A} {B} f {later x} {now y}   (↓≈ a≡b (later↓ x↓a) (now↓ y≡b))   = ↓≈ (cong f a≡b) (later↓ (lift↓ f x↓a)) (now↓ (cong f y≡b))
      liftF≈-cong {A} {B} f {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ λ { .force≈ → liftF≈-cong f (↓≈ a≡b x↓a y↓b) }
      liftF≈-cong {A} {B} f {later x} {later y} (later≈ x≈y)                       = later≈ λ { .force≈ → liftF≈-cong f (force≈ x≈y) }

    -- liftF≈ respects weak bisimilarity
    liftF≈-resp : ∀ {A B : Setoid c (c ⊔ ℓ)} {f g : A ⟶ B} → f ≐ g → liftF≈ f ≐ liftF≈ g
    liftF≈-resp {A} {B} {f} {g} f≐g {now x}   = cong (η≈ B) f≐g
    liftF≈-resp {A} {B} {f} {g} f≐g {later x} = later≈ λ { .force≈ → liftF≈-resp {A} {B} {f} {g} f≐g }

    -- μ is a setoid morphism
    μ≈ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delay≈ (Delay≈ A) ⟶ Delay≈ A
    μ≈ A = record { to = μ {A} ; cong = μ-cong A }
      where
      μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} → [ Delay≈ A ][ x ↓ y ] → [ A ][ (μ {A} x) ≈ y ]
      μ↓ {A} {now x}   {y}       (now↓ x≡y)   = x≡y
      μ↓ {A} {later x} {later y} (later↓ x↓y) = later≈ λ { .force≈ → μ↓ {A} {force x} {force y} (≡↓ (Delay≈ A) (≈-sym A later-self) 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)))
        where
        μ↓-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)
      μ-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≈ λ { .force≈ → μ-cong A (↓≈ a≡b x↓a y↓b) }
      μ-cong A {later x} {later y} (later≈ x≈y)                       = later≈ λ { .force≈ → μ-cong A (force≈ x≈y) }

  delayMonad≈ : Monad (Setoids c (c ⊔ ℓ))
  delayMonad≈ = record
    { F         = record
      { F₀           = Delay≈
      ; F₁           = liftF≈
      ; identity     = ∼⇒≈ Delay∼.identity
      ; homomorphism = λ {X} {Y} {Z} {f} {g} → ∼⇒≈ (Delay∼.homomorphism {X} {Y} {Z} {f} {g})
      ; F-resp-≈     = λ {A} {B} {f} {g} → liftF≈-resp {A} {B} {f} {g}
      }
    ; η         = ntHelper (record { η = η≈ ; commute = λ f → ∼⇒≈ (NaturalTransformation.commute η∼ f) })
    ; μ         = ntHelper (record { η = μ≈ ; commute = λ f {x} → ∼⇒≈ (NaturalTransformation.commute μ∼ f {x}) })
    ; assoc     = λ {A} {x} → ∼⇒≈ (μ-assoc∼' {A} {x})
    ; sym-assoc = λ {A} {x} → ≈-sym A (∼⇒≈ (μ-assoc∼' {A} {x}))
    ; identityˡ = ∼⇒≈ identityˡ∼
    ; identityʳ = ∼⇒≈ identityʳ∼
    }
    where
    -- Associativity needs this simple type variation to work:
    μ-assoc∼' : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μ≈ A ∘ (liftF≈ (μ≈ A))) ⟨$⟩ x ∼ (μ≈ A ∘ μ≈ (Delay≈ A)) ⟨$⟩ x ]
    μ-assoc∼' {A} {now x}   = ∼-refl A
    μ-assoc∼' {A} {later x} = later∼ (λ { .force∼ → μ-assoc∼' {A} {force x} })

open DelayMonad≈
open Monad delayMonad≈ using () renaming (F to Delay≈; η to η≈; μ to μ≈; assoc to assoc≈; sym-assoc to sym-assoc≈; identityˡ to identityˡ≈; identityʳ to identityʳ≈)

-- Universe polymorphic definition of natural numbers together with the setoid on ℕ with propositional equality
module nat {ℓ} where
  data ℕ : Set ℓ where
    zero : ℕ
    suc  : ℕ → ℕ

  ℕ-setoid : Setoid ℓ ℓ
  ℕ-setoid = record 
    { Carrier       = ℕ 
    ; _≈_           = _≡_ 
    ; isEquivalence = Eq.isEquivalence 
    }

  suc-inj : ∀ {n m} → suc n ≡ suc m → n ≡ m
  suc-inj Eq.refl = Eq.refl

open nat

Finally some extra lemmas and definitions concerning ≲ and ≈.

module extra {A : Setoid c (c ⊔ ℓ)} where
  -- ≲ implies weak bisimilarity
  ≲→≈  : {x y : Delay ∣ A ∣}  → [ A ][ x ≲ y ] → [ A ][ x ≈ y ]
  ≲→≈ (↓≲ y↓a)     = ↓≈ (≡-refl A) (now↓ (≡-refl A)) y↓a
  ≲→≈ (later≲ x≲y) = later≈ λ { .force≈ → ≲→≈ (force≲ x≲y) } 

  -- Race two computations and return the first one finished (preferring the left one)
  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 λ { .force → race (force x) (force y) }

  -- If x and y are strongly bisimilar then racing is symmetric
  race-sym∼ : ∀ {x y} → [ A ][ x ∼ y ] → [ A ][ race x y ∼ race y x ]
  race-sym∼ {now x}   {now y}   x∼y =        x∼y
  race-sym∼ {now x}   {later y} x∼y          = ∼-refl A
  race-sym∼ {later x} {now y}   x∼y          = ∼-refl A
  race-sym∼ {later x} {later y} (later∼ x∼y) = later∼ λ { .force∼ → race-sym∼ (force∼ x∼y) }

  -- If x and y are weakly bisimilar then racing is symmetric
  race-sym≈ : ∀ {x y} → [ A ][ x ≈ y ] → [ A ][ race x y ∼ race y x ]
  race-sym≈ {now x}   {now y}   (↓≈ a≡b (now↓ x≡a) (now↓ y≡b))     = now∼ (≡-trans A x≡a (≡-trans A a≡b (≡-sym A y≡b)))
  race-sym≈ {now x}   {later y} x≈y                                = ∼-refl A
  race-sym≈ {later x} {now y}   x≈y                                = ∼-refl A
  race-sym≈ {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later∼ λ { .force∼ → race-sym≈ (↓≈ a≡b x↓a y↓b) }
  race-sym≈ {later x} {later y} (later≈ x≈y)                       = later∼ λ { .force∼ → race-sym≈ (force≈ x≈y) }

  -- If x and y are weakly bisimilar then `race x y ≲ y`
  ≈→≲ : {x y : Delay ∣ A ∣} → [ A ][ x ≈ y ] → [ A ][ race x y ≲ y ]
  ≈→≲ (later≈ x≈y)     = later≲ λ { .force≲ → ≈→≲ (force≈ x≈y) }
  ≈→≲ (↓≈ a≡b x↓a y↓b) = ≈→≲₀ x↓a y↓b a≡b
    where
    ≈→≲₀ : ∀ {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 })

  -- Returns the steps a terminating computation has to take
  delta₀  : {x : Delay ∣ A ∣} {a : ∣ A ∣} → (x↓a : [ A ][ x ↓ a ]) → ℕ {c}
  delta₀ (now↓ x≡y)     = zero
  delta₀ (later↓ x↓a)   = suc (delta₀ x↓a)

  -- If we know that x terminates before y we can run x and remember the amount of steps
  delta  : {x y : Delay ∣ A ∣} → [ A ][ x ≲ y ] → Delay (∣ A ∣ × ℕ {c})
  delta (↓≲ {x} {a} x↓a) = now (a , delta₀ x↓a)
  delta (later≲ x≲′y)    = later λ { .force → delta (force≲ x≲′y) }

  -- Adds `n` later constructors to a computation
  ι : ∣ A ∣ × ℕ {c} → Delay ∣ A ∣
  ι (x , zero)  = now x
  ι (x , suc n) = later λ { .force → ι (x , n) }

  -- ι is a setoid morphism (wrt strong bisimilarity)
  ι∼ : (A ×ₛ (ℕ-setoid {c})) ⟶ Delay∼.₀ A
  ι∼ = record { to = ι ; cong = ι-cong }
    where
      ι-cong : ∀ {x y} → [ A ×ₛ (ℕ-setoid {c}) ][ x ≡ y ] → [ A ][ ι x ∼ ι y ]
      ι-cong {x , zero}  {y , zero}  (x≡y , n≡m) = now∼ x≡y
      ι-cong {x , suc n} {y , suc m} (x≡y , n≡m) = later∼ λ { .force∼ → ι-cong (x≡y , (suc-inj n≡m)) }

  -- Properties of _≲_
  delta-prop₁  : {x y : Delay ∣ A ∣} (x≲y : [ A ][ x ≲ y ]) → [ A ][ liftF proj₁ (delta x≲y) ∼ x ]
  delta-prop₁ {.(now _)}   {x}          (↓≲ x↓a)     = now∼ (≡-refl A)
  delta-prop₁ {.(later _)} {.(later _)} (later≲ x≲y) = later∼ λ { .force∼ → delta-prop₁ (force≲ x≲y) }

  delta-prop₂ : {x y : Delay ∣ A ∣} (x≲y : [ A ][ x ≲ y ]) → [ A ][ μ {A} (liftF ι (delta x≲y)) ∼ y ]
  delta-prop₂ (later≲ x≲y) = later∼ λ { .force∼ → delta-prop₂ (force≲ x≲y) }
  delta-prop₂ (↓≲ x↓a)     = ∼-sym A (ι↓ x↓a)
    where
      ι↓ :  {x : Delay ∣ A ∣}{a : ∣ A ∣} → (x↓a : [ A ][ x ↓ a ]) → [ A ][ x ∼ ι (a , delta₀ x↓a) ]
      ι↓ {.(now _)}   {a} (now↓ x≡y)   = now∼ x≡y
      ι↓ {.(later _)} {a} (later↓ x↓a) = later∼ (record { force∼ = ι↓ x↓a })