```------------------------------------------------------------------------
-- Alternative definitions of weak bisimilarity
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe --sized-types #-}

module Delay-monad.Bisimilarity.Alternative {a} {A : Set a} where

open import Equality.Propositional as E
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Function-universe equality-with-J hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J

-- An alternative definition of weak bisimilarity (discussed by
-- Capretta in "General Recursion via Coinductive Types", and
-- basically the one used in the paper "Partiality, Revisited: The
-- Partiality Monad as a Quotient Inductive-Inductive Type" by
-- Altenkirch, Danielsson and Kraus).
--
-- This definition is pointwise logically equivalent to the one above,

infix 4 _≈₂_

_≈₂_ : Delay A ∞ → Delay A ∞ → Set a
x ≈₂ y = ∀ z → x ⇓ z ⇔ y ⇓ z

-- If A is a set, then this alternative definition of weak
-- bisimilarity is propositional (assuming extensionality), unlike _≈_

≈₂-propositional :
E.Extensionality a a →
Is-set A → ∀ {x y} → Is-proposition (x ≈₂ y)
≈₂-propositional ext A-set =
Π-closure ext 1 λ _ →
⇔-closure ext 1 (Terminates-propositional A-set)
(Terminates-propositional A-set)

-- Another alternative definition of weak bisimilarity, basically the
-- one given by Capretta in "General Recursion via Coinductive Types".

infix 4 [_]_≈₃_ [_]_≈₃′_ _≈₃_

mutual

data [_]_≈₃_ (i : Size) : Delay A ∞ → Delay A ∞ → Set a where
both-terminate : ∀ {x y v} → x ⇓ v → y ⇓ v → [ i ] x ≈₃ y
later          : ∀ {x y} →
[ i ] force x ≈₃′ force y →
[ i ] later x ≈₃  later y

record [_]_≈₃′_ (i : Size) (x y : Delay A ∞) : Set a where
coinductive
field
force : {j : Size< i} → [ j ] x ≈₃ y

open [_]_≈₃′_ public

_≈₃_ : Delay A ∞ → Delay A ∞ → Set a
_≈₃_ = [ ∞ ]_≈₃_

-- If A is inhabited, then this definition is not propositional.

¬-≈₃-propositional : A → ¬ (∀ {x y} → Is-proposition (x ≈₃ y))
¬-≈₃-propositional x =
(∀ {x y} → Is-proposition (x ≈₃ y))  ↝⟨ (λ prop → prop) ⟩
Is-proposition (y ≈₃ y)              ↝⟨ (_\$ _) ∘ (_\$ _) ⟩
proof₁ ≡ proof₂                      ↝⟨ (λ ()) ⟩□
⊥                                    □
where
y : Delay A ∞
y = later λ { .force → now x }

proof₁ : y ≈₃ y
proof₁ = both-terminate (laterʳ now) (laterʳ now)

proof₂ : y ≈₃ y
proof₂ = later λ { .force → both-terminate now now }

-- The last definition of weak bisimilarity given above is pointwise
-- logically equivalent to _≈_. Note that the proof is
-- size-preserving.
--
-- (Given suitable notions of extensionality the two definitions are
-- not pointwise isomorphic, because given such assumptions there is
-- only one proof of never ≈₃ never, but multiple proofs of
-- never ≈ never. However, there is no Agda proof of this claim in
-- this module.)

≈⇔≈₃ : ∀ {i x y} → [ i ] x ≈ y ⇔ [ i ] x ≈₃ y
≈⇔≈₃ = record { to = to; from = from }
where
mutual

laterˡ′ : ∀ {i x x′ y} →
x′ ≡ force x →
[ i ] x′      ≈₃ y →
[ i ] later x ≈₃ y
laterˡ′ eq (both-terminate x⇓ y⇓) = both-terminate
(laterʳ (subst (_⇓ _) eq x⇓))
y⇓
laterˡ′ eq (later p)              = later (laterˡ″ eq p)

laterˡ″ : ∀ {i x x′ y} →
later x′ ≡ x →
[ i ] force x′ ≈₃′ y →
[ i ] x        ≈₃′ y
force (laterˡ″ refl p) = laterˡ′ refl (force p)

mutual

laterʳ′ : ∀ {i x y y′} →
y′ ≡ force y →
[ i ] x ≈₃ y′ →
[ i ] x ≈₃ later y
laterʳ′ eq (both-terminate x⇓ y⇓) = both-terminate
x⇓
(laterʳ (subst (_⇓ _) eq y⇓))
laterʳ′ eq (later p)              = later (laterʳ″ eq p)

laterʳ″ : ∀ {i x y y′} →
later y′ ≡ y →
[ i ] x ≈₃′ force y′ →
[ i ] x ≈₃′ y
force (laterʳ″ refl p) = laterʳ′ refl (force p)

to : ∀ {i x y} → [ i ] x ≈ y → [ i ] x ≈₃ y
to now        = both-terminate now now
to (later  p) = later λ { .force → to (force p) }
to (laterˡ p) = laterˡ′ refl (to p)
to (laterʳ p) = laterʳ′ refl (to p)

from⇓ : ∀ {i x y v} → x ⇓ v → y ⇓ v → [ i ] x ≈ y
from⇓ now        now        = now
from⇓ p          (laterʳ q) = laterʳ (from⇓ p q)
from⇓ (laterʳ p) q          = laterˡ (from⇓ p q)

from : ∀ {i x y} → [ i ] x ≈₃ y → [ i ] x ≈ y
from (both-terminate x⇓v y⇓v) = from⇓ x⇓v y⇓v
from (later p)                = later λ { .force → from (force p) }
```