------------------------------------------------------------------------
-- The expansion relation
------------------------------------------------------------------------

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

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

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

open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J

open import Delay-monad
open import Delay-monad.Strong-bisimilarity as Strong
  using ([_]_∼_; _∼_; now; later; force)
open import Delay-monad.Weak-bisimilarity as Weak
  using ([_]_≈_; _≈_; now; later; laterˡ; laterʳ; force)

------------------------------------------------------------------------
-- The expansion relation

-- The expansion relation, defined using mixed induction and
-- coinduction.

infix  [_]_≳_ [_]_≳′_ _≳_ _≳′_ _≲_ _≲′_

mutual

  data [_]_≳_ (i : Size) : (x y : Delay A ∞) → Set a where
    now    : ∀ {x} → [ i ] now x ≳ now x
    later  : ∀ {x y} →
             [ i ] force x ≳′ force y →
             [ i ] later x ≳  later y
    laterˡ : ∀ {x y} →
             [ i ] force x ≳ y →
             [ i ] later x ≳ 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
_≳_  = [ ∞ ]_≳_
_≳′_ = [ ∞ ]_≳′_
_≲_  = flip _≳_
_≲′_ = flip _≳′_

------------------------------------------------------------------------
-- Conversion lemmas

-- Strong bisimilarity is contained in the expansion relation.

∼→≳ : ∀ {i x y} → [ i ] x ∼ y → [ i ] x ≳ y
∼→≳ now       = now
∼→≳ (later p) = later λ { .force → ∼→≳ (force p) }

-- The expansion relation is contained in weak bisimilarity.

≳→≈ : ∀ {i x y} → [ i ] x ≳ y → [ i ] x ≈ y
≳→≈ now        = now
≳→≈ (later  p) = later λ { .force → ≳→≈ (force p) }
≳→≈ (laterˡ p) = laterˡ (≳→≈ p)

-- In some cases weak bisimilarity is contained in the expansion
-- relation.

≈→≳-now : ∀ {i x y} → [ i ] x ≈ now y → [ i ] x ≳ now y
≈→≳-now now        = now
≈→≳-now (laterˡ p) = laterˡ (≈→≳-now p)

≈→≳-never : ∀ {i x} → [ i ] never ≈ x → [ i ] never ≳ x
≈→≳-never (later  p) = later λ { .force → ≈→≳-never (force p) }
≈→≳-never (laterˡ p) = ≈→≳-never p
≈→≳-never (laterʳ p) = later λ { .force → ≈→≳-never p }

-- In some cases the expansion relation is contained in strong
-- bisimilarity.

≳→∼-never : ∀ {i x} → [ i ] never ≳ x → [ i ] never ∼ x
≳→∼-never (later  p) = later λ { .force → ≳→∼-never (force p) }
≳→∼-never (laterˡ p) = ≳→∼-never p

------------------------------------------------------------------------
-- Some negative results

-- The computation never is not an expansion of now x.

never≵now : ∀ {i x} → ¬ [ i ] never ≳ now x
never≵now {i} = Weak.now≉never {i = i} ∘ Weak.symmetric ∘ ≳→≈

-- The computation now x is not an expansion of never.

now≵never : ∀ {i x} → ¬ [ i ] now x ≳ never
now≵never = Weak.now≉never ∘ ≳→≈

-- The expansion relation defined here is not pointwise propositional.

¬-≳-proposition : ¬ (∀ {x y} → Is-proposition (x ≳ y))
¬-≳-proposition =
  (∀ {x y} → Is-proposition (x ≳ y))  ↝⟨ (λ prop → _⇔_.to propositional⇔irrelevant (prop {x = never} {y = never})) ⟩
  Proof-irrelevant (never ≳ never)    ↝⟨ (λ irr → irr _ _) ⟩
  proof₁ ≡ proof₂                     ↝⟨ (λ ()) ⟩□
  ⊥₀                                  □
  where
  proof₁ : never ≳ never
  proof₁ = later λ { .force → proof₁ }

  proof₂ : never ≳ never
  proof₂ = laterˡ proof₁

------------------------------------------------------------------------
-- Sometimes one can remove later constructors

-- One can remove a later constructor to the right.

laterʳ⁻¹ : ∀ {i} {j : Size< i} {x y} →
           [ i ] x ≳ later y →
           [ j ] x ≳ force y
laterʳ⁻¹ (later  p) = laterˡ (force p)
laterʳ⁻¹ (laterˡ p) = laterˡ (laterʳ⁻¹ p)

-- One can remove one later constructor on each side.

later⁻¹ : ∀ {i} {j : Size< i} {x y} →
          [ i ] later x ≳ later y →
          [ j ] force x ≳ force y
later⁻¹ (later  p) = force p
later⁻¹ (laterˡ p) = laterʳ⁻¹ p

-- The following size-preserving variant of laterʳ⁻¹ can be defined.
--
-- Several other later-removing lemmas cannot be defined (unless A is
-- uninhabited), see below.

laterˡʳ⁻¹ :
  ∀ {i} {x y : Delay′ A ∞} →
  [ i ] later x ≳ force y →
  [ i ] force x ≳ later y →
  [ i ] force x ≳ force y
laterˡʳ⁻¹ {i} p q = laterˡʳ⁻¹′ p q refl refl
  where
  laterˡʳ⁻¹″ :
    ∀ {x′ y′} {x y : Delay′ A ∞} →
    ({j : Size< i} → [ j ] x′ ≳ force y) →
    ({j : Size< i} → [ j ] force x ≳ y′) →
    later x ≡ x′ → later y ≡ y′ →
    [ i ] later x ≳ later y
  laterˡʳ⁻¹″ p q refl refl = later λ { .force → laterˡʳ⁻¹ p q }

  laterˡʳ⁻¹′ :
    ∀ {x′ y′} {x y : Delay′ A ∞} →
    [ i ] later x ≳ y′ →
    [ i ] x′ ≳ later y →
    x′ ≡ force x → y′ ≡ force y →
    [ i ] x′ ≳ y′
  laterˡʳ⁻¹′ (later  p) (later  q) x′≡  y′≡  = laterˡʳ⁻¹″ (force p) (force q)                x′≡ y′≡
  laterˡʳ⁻¹′ (later  p) (laterˡ q) x′≡  y′≡  = laterˡʳ⁻¹″ (force p) (λ { {_} → laterʳ⁻¹ q }) x′≡ y′≡
  laterˡʳ⁻¹′ (laterˡ p) _          refl refl = p

------------------------------------------------------------------------
-- The expansion relation is a partial order (up to weak bisimilarity)

-- The expansion relation is reflexive.

reflexive : ∀ {i} (x : Delay A ∞) → [ i ] x ≳ x
reflexive (now x)   = now
reflexive (later x) = later λ { .force → reflexive (force x) }

-- The expansion relation is antisymmetric (up to weak bisimilarity).

antisymmetric :
  ∀ {i} {x y : Delay A ∞} →
  [ i ] x ≳ y → [ i ] y ≳ x → [ i ] x ≈ y
antisymmetric p _ = ≳→≈ p

-- The expansion relation is transitive.

transitive : ∀ {i} {x y z : Delay A ∞} →
             x ≳ y → [ i ] y ≳ z → [ i ] x ≳ z
transitive {x = now x}   now now = now
transitive {x = later x} p   q   = trans-later p q
  where
  trans-later : ∀ {i x} {y z : Delay A ∞} →
                later x ≳ y → [ i ] y ≳ z → [ i ] later x ≳ z
  trans-later p          (later  q) = later λ { .force →
                                        transitive (later⁻¹ p) (force q) }
  trans-later p          (laterˡ q) = trans-later (laterʳ⁻¹ p) q
  trans-later (laterˡ p) q          = laterˡ (transitive p q)

-- Some size-preserving variants of transitivity.
--
-- Many size-preserving variants cannot be defined (unless A is
-- uninhabited), see below.

transitive-≳∼ :
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≳ y → [ i ] y ∼ z → [ i ] x ≳ z
transitive-≳∼ now        now       = now
transitive-≳∼ (later  p) (later q) = later λ { .force →
                                       transitive-≳∼ (force p) (force q) }
transitive-≳∼ (laterˡ p) q         = laterˡ (transitive-≳∼ p q)

transitive-∼≳ :
  ∀ {i} {x y z : Delay A ∞} →
  x ∼ y → [ i ] y ≳ z → [ i ] x ≳ z
transitive-∼≳ = transitive ∘ ∼→≳

transitive-≳≈ :
  ∀ {i} {x y z : Delay A ∞} →
  x ≳ y → [ i ] y ≈ z → [ i ] x ≈ z
transitive-≳≈ {x = now x}   now q = q
transitive-≳≈ {x = later x} p   q = trans-later p q
  where
  trans-later : ∀ {i x} {y z : Delay A ∞} →
                later x ≳ y → [ i ] y ≈ z → [ i ] later x ≈ z
  trans-later p          (later  q) = later λ { .force →
                                        transitive-≳≈ (later⁻¹ p) (force q) }
  trans-later (later  p) (laterʳ q) = later λ { .force →
                                        transitive-≳≈ (force p) (Weak.laterˡ⁻¹ q) }
  trans-later p          (laterˡ q) = trans-later (laterʳ⁻¹ p) q
  trans-later (laterˡ p) q          = laterˡ (transitive-≳≈ p q)

transitive-≈≲ :
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≈ y → y ≲ z → [ i ] x ≈ z
transitive-≈≲ p q = Weak.symmetric (transitive-≳≈ q (Weak.symmetric p))

-- Some special cases of symmetry hold.

symmetric-neverˡ : ∀ {i x} → [ i ] never ≳ x → [ i ] x ≳ never
symmetric-neverˡ (later  p) = later λ { .force →
                                symmetric-neverˡ (force p) }
symmetric-neverˡ (laterˡ p) = symmetric-neverˡ p

symmetric-neverʳ : ∀ {i x} → [ i ] x ≳ never → [ i ] never ≳ x
symmetric-neverʳ (later  p) = later λ { .force →
                                symmetric-neverʳ (force p) }
symmetric-neverʳ (laterˡ p) = later λ { .force → symmetric-neverʳ p }

------------------------------------------------------------------------
-- Lemmas stating that functions of certain types can be defined iff A
-- is uninhabited

-- A lemma used in several of the proofs below: If A is uninhabited,
-- then the expansion relation is trivial.

uninhabited→trivial : ∀ {i} → ¬ A → ∀ x y → [ i ] x ≳ y
uninhabited→trivial ¬A (now x)   _         = ⊥-elim (¬A x)
uninhabited→trivial ¬A (later x) (now y)   = ⊥-elim (¬A y)
uninhabited→trivial ¬A (later x) (later y) =
  later λ { .force → uninhabited→trivial ¬A (force x) (force y) }

-- There is a function that removes a later constructor to the left,
-- for computations of specific forms, iff A is uninhabited.

Laterˡ⁻¹′ = ∀ {x} →
            later (record { force = now x }) ≳
            later (record { force = now x }) →
            now x ≳ later (record { force = now x })

laterˡ⁻¹′⇔uninhabited : Laterˡ⁻¹′ ⇔ ¬ A
laterˡ⁻¹′⇔uninhabited = record
  { to = Laterˡ⁻¹′                        ↝⟨ (λ hyp _ → hyp) ⟩
         (∀ x → y x ≳ y x → now x ≳ y x)  ↝⟨ (λ hyp x → hyp x (reflexive _)) ⟩
         (∀ x → now x ≳ y x)              ↝⟨ (λ hyp x → now-x≵y x (hyp x)) ⟩□
         ¬ A                              □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ hyp {_} _ → hyp _ _) ⟩□
           Laterˡ⁻¹′        □
  }
  where
  module _ (x : A) where

    y : Delay A ∞
    y = later _

    now-x≵y : ¬ now x ≳ y
    now-x≵y ()

-- There is a function that removes a later constructor to the left
-- iff A is uninhabited.

Laterˡ⁻¹ = ∀ {x y} → later x ≳ y → force x ≳ y

laterˡ⁻¹⇔uninhabited : Laterˡ⁻¹ ⇔ ¬ A
laterˡ⁻¹⇔uninhabited = record
  { to = Laterˡ⁻¹   ↝⟨ (λ hyp → hyp) ⟩
         Laterˡ⁻¹′  ↝⟨ _⇔_.to laterˡ⁻¹′⇔uninhabited ⟩
         ¬ A        □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ hyp {_ _} _ → hyp _ _) ⟩□
           Laterˡ⁻¹         □
  }

-- The following variants of transitivity can be proved iff A is
-- uninhabited.

Transitivity-≈≳≳ = {x y z : Delay A ∞} → x ≈ y → y ≳ z → x ≳ z
Transitivity-≳≈≳ = {x y z : Delay A ∞} → x ≳ y → y ≈ z → x ≳ z

transitive-≈≳≳⇔uninhabited : Transitivity-≈≳≳ ⇔ ¬ A
transitive-≈≳≳⇔uninhabited = record
  { to = Transitivity-≈≳≳  ↝⟨ (λ trans → trans (laterʳ (Weak.reflexive _))) ⟩
         Laterˡ⁻¹          ↝⟨ _⇔_.to laterˡ⁻¹⇔uninhabited ⟩□
         ¬ A               □
  ; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)   ↝⟨ (λ hyp {_ _ _} _ _ → hyp _ _) ⟩□
           Transitivity-≈≳≳  □
  }

transitive-≳≈≳⇔uninhabited : Transitivity-≳≈≳ ⇔ ¬ A
transitive-≳≈≳⇔uninhabited = record
  { to = Transitivity-≳≈≳  ↝⟨ (λ trans {_ y} lx≳y → later⁻¹ {y = record { force = y }}
                                                            (trans lx≳y (laterʳ (Weak.reflexive _)))) ⟩
         Laterˡ⁻¹          ↝⟨ _⇔_.to laterˡ⁻¹⇔uninhabited ⟩□
         ¬ A               □
  ; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)   ↝⟨ (λ hyp {_ _ _} _ _ → hyp _ _) ⟩□
           Transitivity-≳≈≳  □
  }

------------------------------------------------------------------------
-- Lemmas stating that size-preserving functions of certain types can
-- be defined iff A is uninhabited

-- A variant of laterʳ⁻¹ in which one occurrence of the expansion
-- relation is replaced by strong bisimilarity, and both arguments are
-- specialised, can be made size-preserving iff A is uninhabited.

Laterʳ⁻¹-∼≳ = ∀ {i x} →
              [ i ] never ∼ later (record { force = now x }) →
              [ i ] never ≳ now x

size-preserving-laterʳ⁻¹-∼≳⇔uninhabited : Laterʳ⁻¹-∼≳ ⇔ ¬ A
size-preserving-laterʳ⁻¹-∼≳⇔uninhabited = record
  { to   = Laterʳ⁻¹-∼≳       ↝⟨ ≳→≈ ∘_ ⟩
           Weak.Laterʳ⁻¹-∼≈  ↝⟨ _⇔_.to Weak.size-preserving-laterʳ⁻¹-∼≈⇔uninhabited ⟩□
           ¬ A               □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _} _ → trivial _ _) ⟩□
           Laterʳ⁻¹-∼≳      □
  }

-- The function laterʳ⁻¹ can be made size-preserving iff A is
-- uninhabited.

Laterʳ⁻¹ = ∀ {i x y} → [ i ] x ≳ later y → [ i ] x ≳ force y

size-preserving-laterʳ⁻¹⇔uninhabited : Laterʳ⁻¹ ⇔ ¬ A
size-preserving-laterʳ⁻¹⇔uninhabited = record
  { to   = Laterʳ⁻¹     ↝⟨ _∘ ∼→≳ ⟩
           Laterʳ⁻¹-∼≳  ↝⟨ _⇔_.to size-preserving-laterʳ⁻¹-∼≳⇔uninhabited ⟩□
           ¬ A          □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _ _} _ → trivial _ _) ⟩□
           Laterʳ⁻¹         □
  }

-- There is a variant of transitive-∼≳ that preserves the size of the
-- first argument iff A is uninhabited.

Transitivity-∼≳ˡ = ∀ {i} {x y z : Delay A ∞} →
                   [ i ] x ∼ y → y ≳ z → [ i ] x ≳ z

size-preserving-transitivity-∼≳ˡ⇔uninhabited : Transitivity-∼≳ˡ ⇔ ¬ A
size-preserving-transitivity-∼≳ˡ⇔uninhabited = record
  { to   = Transitivity-∼≳ˡ  ↝⟨ (λ trans never∼lnx → trans never∼lnx (laterˡ now) ) ⟩
           Laterʳ⁻¹-∼≳       ↝⟨ _⇔_.to size-preserving-laterʳ⁻¹-∼≳⇔uninhabited ⟩□
           ¬ A               □
  ; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-∼≳ˡ  □
  }

-- There is a transitivity proof that preserves the size of the
-- first argument iff A is uninhabited.

Transitivityˡ = ∀ {i} {x y z : Delay A ∞} →
                [ i ] x ≳ y → y ≳ z → [ i ] x ≳ z

size-preserving-transitivityˡ⇔uninhabited : Transitivityˡ ⇔ ¬ A
size-preserving-transitivityˡ⇔uninhabited = record
  { to   = Transitivityˡ     ↝⟨ _∘ ∼→≳ ⟩
           Transitivity-∼≳ˡ  ↝⟨ _⇔_.to size-preserving-transitivity-∼≳ˡ⇔uninhabited ⟩□
           ¬ A               □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivityˡ    □
  }

-- There is a transitivity proof that preserves the size of both
-- arguments iff A is uninhabited.

Transitivity = ∀ {i} {x y z : Delay A ∞} →
               [ i ] x ≳ y → [ i ] y ≳ z → [ i ] x ≳ z

size-preserving-transitivity⇔uninhabited : Transitivity ⇔ ¬ A
size-preserving-transitivity⇔uninhabited = record
  { to   = Transitivity   ↝⟨ id ⟩
           Transitivityˡ  ↝⟨ _⇔_.to size-preserving-transitivityˡ⇔uninhabited ⟩□
           ¬ A            □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity     □
  }

-- There is a variant of transitive-≳≈ that preserves the size of the
-- first argument iff A is uninhabited.

Transitivity-≳≈ˡ = ∀ {i} {x y z : Delay A ∞} →
                   [ i ] x ≳ y → y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≳≈ˡ⇔uninhabited : Transitivity-≳≈ˡ ⇔ ¬ A
size-preserving-transitivity-≳≈ˡ⇔uninhabited = record
  { to   = Transitivity-≳≈ˡ       ↝⟨ _∘ ∼→≳ ⟩
           Weak.Transitivity-∼≈ˡ  ↝⟨ _⇔_.to Weak.size-preserving-transitivity-∼≈ˡ⇔uninhabited ⟩
           ¬ A                    □
  ; from = ¬ A               ↝⟨ Weak.uninhabited→trivial ⟩
           (∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≳≈ˡ  □
  }

-- There is a variant of transitive-≳≈ that preserves the size of both
-- arguments iff A is uninhabited.

Transitivity-≳≈ = ∀ {i} {x y z : Delay A ∞} →
                  [ i ] x ≳ y → [ i ] y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≳≈⇔uninhabited : Transitivity-≳≈ ⇔ ¬ A
size-preserving-transitivity-≳≈⇔uninhabited = record
  { to   = Transitivity-≳≈   ↝⟨ id ⟩
           Transitivity-≳≈ˡ  ↝⟨ _⇔_.to size-preserving-transitivity-≳≈ˡ⇔uninhabited ⟩
           ¬ A               □
  ; from = ¬ A              ↝⟨ Weak.uninhabited→trivial ⟩
           (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≳≈  □
  }

-- There is a variant of transitive-≈≲ that preserves the size of the
-- second argument iff A is uninhabited.

Transitivity-≈≲ʳ = ∀ {i} {x y z : Delay A ∞} →
                   x ≈ y → [ i ] z ≳ y → [ i ] x ≈ z

size-preserving-transitivity-≈≲ʳ⇔uninhabited : Transitivity-≈≲ʳ ⇔ ¬ A
size-preserving-transitivity-≈≲ʳ⇔uninhabited =
  Transitivity-≈≲ʳ  ↝⟨ record { to   = λ trans x≳y y≈z → Weak.symmetric (trans (Weak.symmetric y≈z) x≳y)
                              ; from = λ trans x≈y y≲z → Weak.symmetric (trans y≲z (Weak.symmetric x≈y))
                              } ⟩
  Transitivity-≳≈ˡ  ↝⟨ size-preserving-transitivity-≳≈ˡ⇔uninhabited ⟩□
  ¬ A               □

-- There is a variant of transitive-≈≲ that preserves the size of both
-- arguments iff A is uninhabited.

Transitivity-≈≲ = ∀ {i} {x y z : Delay A ∞} →
                  [ i ] x ≈ y → [ i ] z ≳ y → [ i ] x ≈ z

size-preserving-transitivity-≈≲⇔uninhabited : Transitivity-≈≲ ⇔ ¬ A
size-preserving-transitivity-≈≲⇔uninhabited =
  Transitivity-≈≲  ↝⟨ record { to   = λ trans x≳y y≈z → Weak.symmetric (trans (Weak.symmetric y≈z) x≳y)
                             ; from = λ trans x≈y y≲z → Weak.symmetric (trans y≲z (Weak.symmetric x≈y))
                             } ⟩
  Transitivity-≳≈  ↝⟨ size-preserving-transitivity-≳≈⇔uninhabited ⟩□
  ¬ A              □

-- There is a transitivity-like proof taking weak bisimilarity and
-- expansion to weak bisimilarity that preserves the size of the first
-- argument iff A is uninhabited.

Transitivity-≈≳ˡ = ∀ {i} {x y z : Delay A ∞} →
                   [ i ] x ≈ y → y ≳ z → [ i ] x ≈ z

size-preserving-transitivity-≈≳ˡ⇔uninhabited : Transitivity-≈≳ˡ ⇔ ¬ A
size-preserving-transitivity-≈≳ˡ⇔uninhabited = record
  { to   = Transitivity-≈≳ˡ  ↝⟨ (λ trans x≈ly → trans x≈ly (laterˡ (reflexive _))) ⟩
           Weak.Laterʳ⁻¹     ↝⟨ _⇔_.to Weak.size-preserving-laterʳ⁻¹⇔uninhabited ⟩
           ¬ A               □
  ; from = ¬ A               ↝⟨ Weak.uninhabited→trivial ⟩
           (∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≈≳ˡ  □
  }