```------------------------------------------------------------------------
-- A comparison of the classical definition of weak bisimilarity and
-- one of the coinductive ones
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module Bisimilarity.Weak.Comparison where

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

open import H-level equality-with-J
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

import Bisimilarity.Classical
import Bisimilarity.Coinductive
import Bisimilarity.Comparison as Comp
import Bisimilarity.Weak.Classical
import Bisimilarity.Weak.Coinductive
open import Labelled-transition-system

module _ {lts : LTS} where

open LTS lts

private
module Cl = Bisimilarity.Weak.Classical   lts
module Co = Bisimilarity.Weak.Coinductive lts

-- Classically weakly bisimilar processes are coinductively weakly
-- bisimilar.

cl⇒co : ∀ {ℓ i p q} → Cl.[ ℓ ] p ≈ q → Co.[ i ] p ≈ q
cl⇒co = Comp.cl⇒co

-- Coinductively weakly bisimilar processes are classically weakly
-- bisimilar.

co⇒cl : ∀ {ℓ p q} → p Co.≈ q → Cl.[ ℓ ] p ≈ q
co⇒cl = Comp.co⇒cl

-- The function cl⇒co is a left inverse of co⇒cl (up to pointwise
-- bisimilarity).

cl⇒co∘co⇒cl : ∀ {ℓ i p q}
(p≈q : p Co.≈ q) →
Co.[ i ] cl⇒co (co⇒cl {ℓ = ℓ} p≈q) ≡ p≈q
cl⇒co∘co⇒cl = Comp.cl⇒co∘co⇒cl

-- If there are two processes that are not equal, but weakly
-- bisimilar, then co⇒cl is not a left inverse of cl⇒co.

co⇒cl∘cl⇒co : ∀ {p q ℓ} →
p ≢ q → p Co.≈ q →
∃ λ (p≈p : Cl.[ ℓ ] p ≈ p) → co⇒cl (cl⇒co p≈p) ≢ p≈p
co⇒cl∘cl⇒co = Comp.co⇒cl∘cl⇒co

-- The two definitions of weak bisimilarity are logically
-- equivalent.

classical⇔coinductive :
∀ {ℓ p q} → Cl.[ ℓ ] p ≈ q ⇔ p Co.≈ q
classical⇔coinductive = Comp.classical⇔coinductive

-- The larger classical versions of weak bisimilarity are logically
-- equivalent to the smallest one.

larger⇔smallest : ∀ {ℓ p q} → Cl.[ ℓ ] p ≈ q ⇔ p Cl.≈ q
larger⇔smallest = Comp.larger⇔smallest

-- There is a split surjection from the classical definition of
-- bisimilarity to the coinductive one (assuming extensionality).

classical↠coinductive :
Co.Extensionality →
∀ {ℓ p q} → Cl.[ ℓ ] p ≈ q ↠ p Co.≈ q
classical↠coinductive = Comp.classical↠coinductive

-- There is at least one LTS for which there is a split surjection
-- from the coinductive definition of weak bisimilarity to the
-- classical one.

coinductive↠classical :
∀ {ℓ p q} →
Bisimilarity.Weak.Coinductive._≈_  empty   p q ↠
Bisimilarity.Weak.Classical.[_]_≈_ empty ℓ p q
coinductive↠classical {p = ()}

-- There is an LTS for which coinductive weak bisimilarity is
-- pointwise propositional (assuming extensionality and univalence).

coinductive-weak-bisimilarity-is-sometimes-propositional :
Univalence lzero →
let module Co = Bisimilarity.Weak.Coinductive one-loop in
Co.Extensionality → Is-proposition (tt Co.≈ tt)
coinductive-weak-bisimilarity-is-sometimes-propositional univ =
subst (λ lts → let module Co = Bisimilarity.Coinductive lts in
∀ p → Co.Extensionality → Is-proposition (p Co.∼ p))
(sym \$ weak≡id univ one-loop (λ _ ()))
(λ _ → Comp.coinductive-bisimilarity-is-sometimes-propositional)
_

-- However, classical weak bisimilarity is, for the same LTS, not
-- pointwise propositional (assuming univalence).

classical-weak-bisimilarity-is-not-propositional :
Univalence lzero →
let module Cl = Bisimilarity.Weak.Classical one-loop in
∀ {ℓ} → ¬ Is-proposition (Cl.[ ℓ ] tt ≈ tt)
classical-weak-bisimilarity-is-not-propositional univ {ℓ} =
subst (λ lts → let module Cl = Bisimilarity.Classical lts in
∀ p → ¬ Is-proposition (Cl.[ ℓ ] p ∼ p))
(sym \$ weak≡id univ one-loop (λ _ ()))
(λ _ → Comp.classical-bisimilarity-is-not-propositional)
_

-- Thus there is, in general, no split surjection from the coinductive
-- definition of weak bisimilarity to the classical one (assuming
-- extensionality and univalence).

¬coinductive↠classical :
Univalence lzero →
∀ {ℓ} →
Bisimilarity.Weak.Coinductive.Extensionality one-loop →
¬ (∀ {p q} → Bisimilarity.Weak.Coinductive._≈_  one-loop   p q ↠
Bisimilarity.Weak.Classical.[_]_≈_ one-loop ℓ p q)
¬coinductive↠classical univ {ℓ} =
subst (λ lts → Bisimilarity.Coinductive.Extensionality lts →
¬ (∀ {p q} → Bisimilarity.Coinductive._∼_  lts   p q ↠
Bisimilarity.Classical.[_]_∼_ lts ℓ p q))
(sym \$ weak≡id univ one-loop (λ _ ()))
Comp.¬coinductive↠classical

-- Note also that coinductive weak bisimilarity is not always
-- propositional (assuming univalence).

coinductive-weak-bisimilarity-is-not-propositional :
Univalence lzero →
let open Bisimilarity.Weak.Coinductive two-bisimilar-processes in
¬ (∀ {p q} → Is-proposition (p ≈ q))
coinductive-weak-bisimilarity-is-not-propositional univ =
subst (λ lts → let open Bisimilarity.Coinductive lts in
¬ (∀ {p q} → Is-proposition (p ∼ q)))
(sym \$ weak≡id univ two-bisimilar-processes (λ _ ()))
Comp.coinductive-bisimilarity-is-not-propositional

-- In fact, for every type A there is a pointwise split surjection
-- from a certain instance of weak bisimilarity to equality on A
-- (assuming univalence).

weak-bisimilarity↠equality :
Univalence lzero →
{A : Set} →
let open Bisimilarity.Weak.Coinductive (bisimilarity⇔equality A) in
{p q : A} → p ≈ q ↠ p ≡ q
weak-bisimilarity↠equality univ {A} =
subst (λ lts → let open Bisimilarity.Coinductive lts in
∀ {p q} → p ∼ q ↠ p ≡ q)
(sym \$ weak≡id univ (bisimilarity⇔equality A) (λ _ ()))
Comp.bisimilarity↠equality
```