------------------------------------------------------------------------
-- Labelled transition systems
------------------------------------------------------------------------

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

module Labelled-transition-system where

open import Equality.Propositional
open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equivalence equality-with-J using (↔⇒≃)
open import Function-universe equality-with-J hiding (id; _∘_)
open import Univalence-axiom equality-with-J

-- Labelled transition systems were perhaps first defined by Robert M.
-- Keller (https://doi.org/10.1145/360248.360251). The definition
-- below is a variant with a field "is-silent", added by me.
--
-- I don't know who first came up with the concept of a weak
-- transition. The definitions of _⇒_, _[_]⇒_, _[_]⇒̂_ and _[_]⟶̂_ below
-- are based on definitions in "Enhancements of the bisimulation proof
-- method" by Pous and Sangiorgi.

record LTS ℓ : Set (lsuc ℓ) where
  infix  _[_]⟶_ _⇒_ _[_]⇒_ _[_]⇒̂_ _[_]⟶̂_
  field
    -- Processes.
    Proc : Set ℓ

    -- Labels.
    Label : Set ℓ

    -- Transitions.
    _[_]⟶_ : Proc → Label → Proc → Set ℓ

    -- Is the label silent?
    is-silent : Label → Bool

  -- Is the label silent?

  Silent : Label → Set
  Silent μ with is-silent μ
  ... | true  = ⊤
  ... | false = ⊥

  -- Silence can be decided.

  silent? : ∀ μ → Dec (Silent μ)
  silent? μ with is-silent μ
  ... | true  = yes _
  ... | false = no id

  -- Sequences of zero or more silent transitions.

  data _⇒_ : Proc → Proc → Set ℓ where
    done : ∀ {p} → p ⇒ p
    step : ∀ {p q r μ} → Silent μ → p [ μ ]⟶ q → q ⇒ r → p ⇒ r

  -- Weak transitions (one kind).

  data _[_]⇒_ (p : Proc) (μ : Label) (q : Proc) : Set ℓ where
    steps : ∀ {p′ q′} → p ⇒ p′ → p′ [ μ ]⟶ q′ → q′ ⇒ q → p [ μ ]⇒ q

  -- Weak transitions (another kind).

  data _[_]⇒̂_ (p : Proc) (μ : Label) (q : Proc) : Set ℓ where
    silent     : Silent μ → p ⇒ q → p [ μ ]⇒̂ q
    non-silent : ¬ Silent μ → p [ μ ]⇒ q → p [ μ ]⇒̂ q

  -- Weak transitions (yet another kind).

  data _[_]⟶̂_ (p : Proc) (μ : Label) : Proc → Set ℓ where
    done : Silent μ → p [ μ ]⟶̂ p
    step : ∀ {q} → p [ μ ]⟶ q → p [ μ ]⟶̂ q

  -- Functions that can be used to aid the instance resolution
  -- mechanism.

  infix -2 ⟶:_ ⇒:_ []⇒:_ ⇒̂:_ ⟶̂:_

  ⟶:_ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]⟶ q
  ⟶:_ = id

  ⇒:_ : ∀ {p q} → p ⇒ q → p ⇒ q
  ⇒:_ = id

  []⇒:_ : ∀ {p μ q} → p [ μ ]⇒ q → p [ μ ]⇒ q
  []⇒:_ = id

  ⇒̂:_ : ∀ {p μ q} → p [ μ ]⇒̂ q → p [ μ ]⇒̂ q
  ⇒̂:_ = id

  ⟶̂:_ : ∀ {p μ q} → p [ μ ]⟶̂ q → p [ μ ]⟶̂ q
  ⟶̂:_ = id

  -- An "equational" reasoning combinator that is not subsumed by the
  -- combinators in Equational-reasoning, because the types of the two
  -- main arguments and the result use three different relations.

  infixr -2 ⟶⇒→[]⇒

  ⟶⇒→[]⇒ : ∀ p μ {q r} → p [ μ ]⟶ q → q ⇒ r → p [ μ ]⇒ r
  ⟶⇒→[]⇒ _ _ = steps done

  syntax ⟶⇒→[]⇒ p μ p⟶q q⇒r = p [ μ ]⇒⟨ p⟶q ⟩ q⇒r

  -- Combinators that can be used to add visible type information to
  -- an expression.

  infix -1 step-with-action step-without-action

  step-with-action : ∀ p μ q → p [ μ ]⟶ q → p [ μ ]⟶ q
  step-with-action _ _ _ p⟶q = p⟶q

  step-without-action : ∀ p {μ} q → p [ μ ]⟶ q → p [ μ ]⟶ q
  step-without-action _ _ p⟶q = p⟶q

  syntax step-with-action    p μ q p⟶q = p [ μ ]⟶⟨ p⟶q ⟩ q
  syntax step-without-action p   q p⟶q = p      ⟶⟨ p⟶q ⟩ q

  -- Regular transitions can (sometimes) be turned into weak ones.

  ⟶→⇒ : ∀ {p μ q} → Silent μ → p [ μ ]⟶ q → p ⇒ q
  ⟶→⇒ s tr = step s tr done

  ⟶→[]⇒ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]⇒ q
  ⟶→[]⇒ tr = steps done tr done

  ⟶→⇒̂ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]⇒̂ q
  ⟶→⇒̂ {μ = μ} tr with silent? μ
  ... | yes s = silent s (⟶→⇒ s tr)
  ... | no ¬s = non-silent ¬s (⟶→[]⇒ tr)

  ⟶→⟶̂ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]⟶̂ q
  ⟶→⟶̂ = step

  -- Several transitivity-like properties.

  ⇒-transitive : ∀ {p q r} → p ⇒ q → q ⇒ r → p ⇒ r
  ⇒-transitive done             p⇒q = p⇒q
  ⇒-transitive (step s p⟶q q⇒r) r⇒s = step s p⟶q (⇒-transitive q⇒r r⇒s)

  ⇒[]⇒-transitive : ∀ {p q r μ} → p ⇒ q → q [ μ ]⇒ r → p [ μ ]⇒ r
  ⇒[]⇒-transitive p⇒q (steps q⇒r r⟶s s⇒t) =
    steps (⇒-transitive p⇒q q⇒r) r⟶s s⇒t

  []⇒⇒-transitive : ∀ {p q r μ} → p [ μ ]⇒ q → q ⇒ r → p [ μ ]⇒ r
  []⇒⇒-transitive (steps p⇒q q⟶r r⇒s) s⇒t =
    steps p⇒q q⟶r (⇒-transitive r⇒s s⇒t)

  ⇒⇒̂-transitive : ∀ {p q r μ} → p ⇒ q → q [ μ ]⇒̂ r → p [ μ ]⇒̂ r
  ⇒⇒̂-transitive p⇒q (silent s q⇒r) = silent s (⇒-transitive p⇒q q⇒r)
  ⇒⇒̂-transitive p⇒q (non-silent ¬s q⇒r) =
    non-silent ¬s (⇒[]⇒-transitive p⇒q q⇒r)

  ⇒̂⇒-transitive : ∀ {p q r μ} → p [ μ ]⇒̂ q → q ⇒ r → p [ μ ]⇒̂ r
  ⇒̂⇒-transitive (silent s p⇒q) q⇒r = silent s (⇒-transitive p⇒q q⇒r)
  ⇒̂⇒-transitive (non-silent ¬s p⇒q) q⇒r =
    non-silent ¬s ([]⇒⇒-transitive p⇒q q⇒r)

  -- More conversion functions.

  []⇒→⇒ : ∀ {p q μ} → Silent μ → p [ μ ]⇒ q → p ⇒ q
  []⇒→⇒ s (steps p⇒p′ p′⟶p″ p″⇒p‴) =
    ⇒-transitive p⇒p′ (step s p′⟶p″ p″⇒p‴)

  ⇒̂→⇒ : ∀ {p q μ} → Silent μ → p [ μ ]⇒̂ q → p ⇒ q
  ⇒̂→⇒ s (silent _ p⇒q)    = p⇒q
  ⇒̂→⇒ s (non-silent ¬s _) = ⊥-elim (¬s s)

  ⇒→⇒̂ : ∀ {p q μ} → p [ μ ]⇒ q → p [ μ ]⇒̂ q
  ⇒→⇒̂ {μ = μ} tr with silent? μ
  ... | yes s = silent s ([]⇒→⇒ s tr)
  ... | no ¬s = non-silent ¬s tr

  ⇒̂→[]⇒ : ∀ {p q μ} → ¬ Silent μ → p [ μ ]⇒̂ q → p [ μ ]⇒ q
  ⇒̂→[]⇒ ¬s (silent s _)      = ⊥-elim (¬s s)
  ⇒̂→[]⇒ _  (non-silent _ tr) = tr

  ⟶̂→⇒̂ : ∀ {p μ q} → p [ μ ]⟶̂ q → p [ μ ]⇒̂ q
  ⟶̂→⇒̂ (done s)  = silent s done
  ⟶̂→⇒̂ (step tr) = ⟶→⇒̂ tr

  ⟶̂→⇒ : ∀ {p q μ} → Silent μ → p [ μ ]⟶̂ q → p ⇒ q
  ⟶̂→⇒ s = ⇒̂→⇒ s ∘ ⟶̂→⇒̂

  -- Lemmas that can be used to show that relations are weak
  -- simulations of various kinds.

  module _
    {ℓ}
    {_%_ _%′_ : Proc → Proc → Set ℓ}
    {_[_]%_ : Proc → Label → Proc → Set ℓ}
    (left-to-right :
       ∀ {p q} → p % q → ∀ {p′ μ} →
       p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]% q′ × p′ %′ q′)
    (%′⇒% : ∀ {p q} → p %′ q → p % q)
    (%⇒⇒ : ∀ {p p′ μ} → Silent μ → p [ μ ]% p′ → p ⇒ p′)
    where

    is-weak⇒ :
      ∀ {p p′ q} →
      p % q → p ⇒ p′ →
      ∃ λ q′ → q ⇒ q′ × (p′ % q′)
    is-weak⇒ p%q done                = _ , done , p%q
    is-weak⇒ p%q (step s p⟶p′ p′⇒p″) =
      let q′ , q%q′  , p′%′q′ = left-to-right p%q p⟶p′
          q″ , q′⇒q″ , p″%q″  = is-weak⇒ (%′⇒% p′%′q′) p′⇒p″
      in q″ , ⇒-transitive (%⇒⇒ s q%q′) q′⇒q″ , p″%q″

    is-weak[]⇒ :
      ∀ {p p′ q μ} →
      (∀ {p p′} → p [ μ ]% p′ → p [ μ ]⇒ p′) →
      p % q → p [ μ ]⇒ p′ →
      ∃ λ q′ → q [ μ ]⇒ q′ × (p′ % q′)
    is-weak[]⇒ %⇒[]⇒ p%q (steps p⇒p′ p′⟶p″ p″⇒p‴) =
      let q′ , q⇒q′  , p′%q′  = is-weak⇒ p%q p⇒p′
          q″ , q′%q″ , p″%′q″ = left-to-right p′%q′ p′⟶p″
          q‴ , q″⇒q‴ , p‴%q‴  = is-weak⇒ (%′⇒% p″%′q″) p″⇒p‴
      in q‴
       , ⇒[]⇒-transitive q⇒q′ ([]⇒⇒-transitive (%⇒[]⇒ q′%q″) q″⇒q‴)
       , p‴%q‴

    is-weak⇒̂ :
      ∀ {p p′ q μ} →
      (∀ {p p′} → p [ μ ]% p′ → p [ μ ]⇒̂ p′) →
      p % q → p [ μ ]⇒̂ p′ →
      ∃ λ q′ → q [ μ ]⇒̂ q′ × (p′ % q′)
    is-weak⇒̂ _ q%r (silent s q⇒q′) =
      Σ-map id (Σ-map (silent s) id) (is-weak⇒ q%r q⇒q′)
    is-weak⇒̂ %⇒⇒̂ q%r (non-silent ¬s q⇒q′) =
      Σ-map id (Σ-map ⇒→⇒̂ id) (is-weak[]⇒ (⇒̂→[]⇒ ¬s ∘ %⇒⇒̂) q%r q⇒q′)

  -- If no action is silent, then _[_]⇒_ is pointwise isomorphic to
  -- _[_]⟶_.

  ⟶↔⇒ : (∀ μ → ¬ Silent μ) →
        ∀ {p μ q} → p [ μ ]⟶ q ↔ p [ μ ]⇒ q
  ⟶↔⇒ ¬silent = record
    { surjection = record
      { logical-equivalence = record
        { to   = ⟶→[]⇒
        ; from = λ
            { (steps (step s _ _) _ _) → ⊥-elim (¬silent _ s)
            ; (steps _ _ (step s _ _)) → ⊥-elim (¬silent _ s)
            ; (steps done tr done)     → tr
            }
        }
      ; right-inverse-of = λ
          { (steps (step s _ _) _ _) → ⊥-elim (¬silent _ s)
          ; (steps _ _ (step s _ _)) → ⊥-elim (¬silent _ s)
          ; (steps done tr done)     → refl
          }
      }
    ; left-inverse-of = λ _ → refl
    }

  -- If no action is silent, then _[_]⇒̂_ is pointwise logically
  -- equivalent to _[_]⟶_, and in the presence of extensionality they
  -- are pointwise isomorphic.

  ⟶↔⇒̂ : ∀ {k} →
        Extensionality? k lzero lzero →
        (∀ μ → ¬ Silent μ) →
        ∀ {p μ q} → p [ μ ]⟶ q ↝[ k ] p [ μ ]⇒̂ q
  ⟶↔⇒̂ ext ¬silent = generalise-ext? ⟶⇔⇒̂ ⟶↔⇒̂′ ext
    where
    ⟶⇔⇒̂ = record
      { to   = λ tr → non-silent (¬silent _) (_↔_.to (⟶↔⇒ ¬silent) tr)
      ; from = λ
          { (silent s _)      → ⊥-elim (¬silent _ s)
          ; (non-silent _ tr) → _↔_.from (⟶↔⇒ ¬silent) tr
          }
      }

    ⟶↔⇒̂′ = λ ext → record
      { surjection = record
        { logical-equivalence = ⟶⇔⇒̂
        ; right-inverse-of    = λ
            { (silent s _)      → ⊥-elim (¬silent _ s)
            ; (non-silent _ tr) →
                cong₂ non-silent
                      (apply-ext ext (⊥-elim ∘ ¬silent _))
                      (_↔_.right-inverse-of (⟶↔⇒ ¬silent) tr)
            }
        }
      ; left-inverse-of = λ _ → refl
      }

  -- Map-like functions.

  map-⇒′ :
    {F : Proc → Proc} →
    (∀ {p p′ μ} → Silent μ → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′} → p ⇒ p′ → F p ⇒ F p′
  map-⇒′ f done                = done
  map-⇒′ f (step s p⟶p′ p′⇒p″) =
    step s (f s p⟶p′) (map-⇒′ f p′⇒p″)

  map-⇒ :
    {F : Proc → Proc} →
    (∀ {p p′ μ} → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′} → p ⇒ p′ → F p ⇒ F p′
  map-⇒ f = map-⇒′ (λ _ → f)

  map-[]⇒′ :
    ∀ {μ} {F : Proc → Proc} →
    (∀ {p p′ μ} → Silent μ → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    (∀ {p p′} → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′} → p [ μ ]⇒ p′ → F p [ μ ]⇒ F p′
  map-[]⇒′ f g (steps p⇒p′ p′⟶p″ p″⇒p‴) =
    steps (map-⇒′ f p⇒p′) (g p′⟶p″) (map-⇒′ f p″⇒p‴)

  map-[]⇒ :
    {F : Proc → Proc} →
    (∀ {p p′ μ} → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′ μ} → p [ μ ]⇒ p′ → F p [ μ ]⇒ F p′
  map-[]⇒ f = map-[]⇒′ (λ _ → f) f

  map-⇒̂′ :
    ∀ {μ} {F : Proc → Proc} →
    (∀ {p p′ μ} → Silent μ → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    (∀ {p p′} → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′} → p [ μ ]⇒̂ p′ → F p [ μ ]⇒̂ F p′
  map-⇒̂′ f g (silent s p⇒p′)      = silent s (map-⇒′ f p⇒p′)
  map-⇒̂′ f g (non-silent ¬s p⇒p′) = non-silent ¬s (map-[]⇒′ f g p⇒p′)

  map-⇒̂ :
    {F : Proc → Proc} →
    (∀ {p p′ μ} → p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    ∀ {p p′ μ} → p [ μ ]⇒̂ p′ → F p [ μ ]⇒̂ F p′
  map-⇒̂ f = map-⇒̂′ (λ _ → f) f

  map-⟶̂ :
    ∀ {μ p p′} {F : Proc → Proc} →
    (p [ μ ]⟶ p′ → F p [ μ ]⟶ F p′) →
    p [ μ ]⟶̂ p′ → F p [ μ ]⟶̂ F p′
  map-⟶̂ f (done s)    = done s
  map-⟶̂ f (step p⟶p′) = step (f p⟶p′)

  -- Zip-like functions.

  module _
    {F : Proc → Proc → Proc}
    (f : ∀ {p p′ q μ} → p [ μ ]⟶ p′ → F p q [ μ ]⟶ F p′ q)
    (g : ∀ {p q q′ μ} → q [ μ ]⟶ q′ → F p q [ μ ]⟶ F p q′)
    where

    zip-⇒ : ∀ {p p′ q q′} → p ⇒ p′ → q ⇒ q′ → F p q ⇒ F p′ q′
    zip-⇒ done done                = done
    zip-⇒ done (step s q⟶q′ q′⇒q″) = step s (g q⟶q′) (zip-⇒ done q′⇒q″)
    zip-⇒ (step s p⟶p′ p′⇒p″) tr   = step s (f p⟶p′) (zip-⇒ p′⇒p″ tr)

    zip-[]⇒ˡ′ :
      ∀ {p p′ q q′ μ₁ μ₃} →
      (∀ {p p′ q} → p [ μ₁ ]⟶ p′ → F p q [ μ₃ ]⟶ F p′ q) →
      p [ μ₁ ]⇒ p′ → q ⇒ q′ → F p q [ μ₃ ]⇒ F p′ q′
    zip-[]⇒ˡ′ h (steps p⇒p′ p′⟶p″ p″⇒p‴) q⇒q′ =
      steps (zip-⇒ p⇒p′ q⇒q′) (h p′⟶p″) (zip-⇒ p″⇒p‴ done)

    zip-[]⇒ˡ : ∀ {p p′ q q′ μ} →
               p [ μ ]⇒ p′ → q ⇒ q′ → F p q [ μ ]⇒ F p′ q′
    zip-[]⇒ˡ = zip-[]⇒ˡ′ f

    zip-[]⇒ʳ′ :
      ∀ {p p′ q q′ μ₂ μ₃} →
      (∀ {p q q′} → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p q′) →
      p ⇒ p′ → q [ μ₂ ]⇒ q′ → F p q [ μ₃ ]⇒ F p′ q′
    zip-[]⇒ʳ′ h p⇒p′ (steps q⇒q′ q′⟶q″ q″⇒q‴) =
      steps (zip-⇒ p⇒p′ q⇒q′) (h q′⟶q″) (zip-⇒ done q″⇒q‴)

    zip-[]⇒ʳ : ∀ {p p′ q q′ μ} →
               p ⇒ p′ → q [ μ ]⇒ q′ → F p q [ μ ]⇒ F p′ q′
    zip-[]⇒ʳ = zip-[]⇒ʳ′ g

    zip-[]⇒ :
      ∀ {μ₁ μ₂ μ₃} →
      (∀ {p p′ q q′} →
       p [ μ₁ ]⟶ p′ → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p′ q′) →
      ∀ {p p′ q q′} →
      p [ μ₁ ]⇒ p′ → q [ μ₂ ]⇒ q′ → F p q [ μ₃ ]⇒ F p′ q′
    zip-[]⇒ h (steps p⇒p′ p′⟶p″ p″⇒p‴) (steps q⇒q′ q′⟶q″ q″⇒q‴) =
      steps (zip-⇒ p⇒p′ q⇒q′) (h p′⟶p″ q′⟶q″) (zip-⇒ p″⇒p‴ q″⇒q‴)

    zip-⇒̂ :
      ∀ {μ₁ μ₂ μ₃} →
      (Silent μ₁ → Silent μ₂ → Silent μ₃) →
      (∀ {p p′ q} → p [ μ₁ ]⟶ p′ → Silent μ₂ → F p q [ μ₃ ]⟶ F p′ q) →
      (∀ {p q q′} → Silent μ₁ → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p q′) →
      (∀ {p p′ q q′} →
       p [ μ₁ ]⟶ p′ → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p′ q′) →
      ∀ {p p′ q q′} →
      p [ μ₁ ]⇒̂ p′ → q [ μ₂ ]⇒̂ q′ → F p q [ μ₃ ]⇒̂ F p′ q′
    zip-⇒̂ fs hˡ hʳ h = λ where
      (silent s₁ tr₁)      (silent s₂ tr₂)      → silent (fs s₁ s₂) (zip-⇒ tr₁ tr₂)
      (silent s₁ tr₁)      (non-silent ¬s₂ tr₂) → ⇒→⇒̂ (zip-[]⇒ʳ′ (hʳ s₁)      tr₁ tr₂)
      (non-silent ¬s₁ tr₁) (silent s₂ tr₂)      → ⇒→⇒̂ (zip-[]⇒ˡ′ (flip hˡ s₂) tr₁ tr₂)
      (non-silent ¬s₁ tr₁) (non-silent ¬s₂ tr₂) → ⇒→⇒̂ (zip-[]⇒   h            tr₁ tr₂)

  zip-⟶̂ :
    ∀ {F : Proc → Proc → Proc} {μ₁ μ₂ μ₃} →
    (Silent μ₁ → Silent μ₂ → Silent μ₃) →
    (∀ {p p′ q} → p [ μ₁ ]⟶ p′ → Silent μ₂ → F p q [ μ₃ ]⟶ F p′ q) →
    (∀ {p q q′} → Silent μ₁ → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p q′) →
    (∀ {p p′ q q′} →
     p [ μ₁ ]⟶ p′ → q [ μ₂ ]⟶ q′ → F p q [ μ₃ ]⟶ F p′ q′) →
    ∀ {p p′ q q′} → p [ μ₁ ]⟶̂ p′ → q [ μ₂ ]⟶̂ q′ → F p q [ μ₃ ]⟶̂ F p′ q′
  zip-⟶̂ s f g h (done s₁)   (done s₂)   = done (s s₁ s₂)
  zip-⟶̂ s f g h (done s₁)   (step q⟶q′) = step (g s₁ q⟶q′)
  zip-⟶̂ s f g h (step p⟶p′) (done s₂)   = step (f p⟶p′ s₂)
  zip-⟶̂ s f g h (step p⟶p′) (step q⟶q′) = step (h p⟶p′ q⟶q′)

-- Transforms an LTS into one which uses weak transitions as
-- transitions.

weak : ∀ {ℓ} → LTS ℓ → LTS ℓ
weak lts = record
  { Proc      = Proc
  ; Label     = Label
  ; _[_]⟶_    = _[_]⇒̂_
  ; is-silent = is-silent
  }
  where
  open LTS lts

-- If no lts action is silent, then weak lts is equal to lts (assuming
-- extensionality and univalence).

weak≡id :
  ∀ {ℓ} →
  Extensionality ℓ (lsuc ℓ) →
  Univalence ℓ →
  (lts : LTS ℓ) →
  (∀ μ → ¬ LTS.Silent lts μ) →
  weak lts ≡ lts
weak≡id ext univ lts ¬silent =
  cong (λ _[_]⟶_ → record
          { Proc      = Proc
          ; Label     = Label
          ; _[_]⟶_    = _[_]⟶_
          ; is-silent = is-silent
          })
       (apply-ext ext λ p → apply-ext ext λ μ → apply-ext ext λ q →
          p [ μ ]⇒̂ q  ≡⟨ ≃⇒≡ univ $ ↔⇒≃ $ inverse $ ⟶↔⇒̂ (lower-extensionality _ _ ext) ¬silent ⟩∎
          p [ μ ]⟶ q  ∎)
  where
  open LTS lts

-- An LTS with no processes or labels.

empty : LTS lzero
empty = record
  { Proc      = ⊥
  ; Label     = ⊥
  ; _[_]⟶_    = λ ()
  ; is-silent = λ ()
  }

-- An LTS with a single process, a single (non-silent) label, and a
-- single transition.

one-loop : LTS lzero
one-loop = record
  { Proc      = ⊤
  ; Label     = ⊤
  ; _[_]⟶_    = λ _ _ _ → ⊤
  ; is-silent = λ _ → false
  }

-- An LTS with two distinct, but bisimilar, processes. There are
-- transitions between the two processes.

two-bisimilar-processes : LTS lzero
two-bisimilar-processes = record
  { Proc      = Bool
  ; Label     = ⊤
  ; _[_]⟶_    = λ _ _ _ → ⊤
  ; is-silent = λ _ → false
  }

-- A parametrised LTS for which bisimilarity is logically equivalent
-- to equality.

bisimilarity⇔equality : ∀ {ℓ} → Set ℓ → LTS ℓ
bisimilarity⇔equality A = record
  { Proc      = A
  ; Label     = A
  ; _[_]⟶_    = λ p μ q → p ≡ μ × p ≡ q
  ; is-silent = λ _ → false
  }