```------------------------------------------------------------------------
-- Some negative results related to weak bisimilarity and expansion
------------------------------------------------------------------------

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

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

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

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

open import Delay-monad
open import Delay-monad.Bisimilarity
open import Delay-monad.Termination

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

-- The computation now x is an expansion of
-- later (record { force = now x }) for every x : A iff A is
-- uninhabited.

Now≳later-now = (x : A) → now x ≳ later (record { force = now x })

now≳later-now⇔uninhabited : Now≳later-now ⇔ ¬ A
now≳later-now⇔uninhabited = record
{ to   = Now≳later-now  ↝⟨ (λ hyp x → case hyp x of λ ()) ⟩□
¬ A            □
; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≳ y)  ↝⟨ (λ hyp _ → hyp _ _) ⟩□
Now≳later-now    □
}

-- A variant of laterˡ⁻¹ for (fully defined) expansion can be defined
-- iff A is uninhabited.

Laterˡ⁻¹-≳ = ∀ {x} {y : Delay A ∞} → later x ≳ y → force x ≳ y

laterˡ⁻¹-≳⇔uninhabited : Laterˡ⁻¹-≳ ⇔ ¬ A
laterˡ⁻¹-≳⇔uninhabited = record
{ to   = Laterˡ⁻¹-≳     ↝⟨ (λ hyp _ → hyp (reflexive _)) ⟩
Now≳later-now  ↝⟨ _⇔_.to now≳later-now⇔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ʳ (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ʳ (reflexive _)))) ⟩
Laterˡ⁻¹-≳        ↝⟨ _⇔_.to laterˡ⁻¹-≳⇔uninhabited ⟩□
¬ A               □
; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≳ y)   ↝⟨ (λ hyp {_ _ _} _ _ → hyp _ _) ⟩□
Transitivity-≳≈≳  □
}

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

-- A variant of laterˡ⁻¹ in which one occurrence of weak bisimilarity
-- is replaced by strong bisimilarity, and both arguments are
-- specialised, can be made size-preserving iff A is uninhabited.
--
-- This lemma is used to prove all other similar results below
-- (directly or indirectly), with the exception that an alternative,
-- more direct proof is also given for one of the results.

Laterˡ⁻¹-∼≈ = ∀ {i} {x : A} →
[ i ] later (λ { .force → now x }) ∼ never →
[ i ] now x                        ≈ never

size-preserving-laterˡ⁻¹-∼≈⇔uninhabited : Laterˡ⁻¹-∼≈ ⇔ ¬ A
size-preserving-laterˡ⁻¹-∼≈⇔uninhabited = record
{ to   = Laterˡ⁻¹-∼≈  ↝⟨ (λ laterˡ⁻¹-∼≈ x → contradiction (laterˡ⁻¹-∼≈ {_}) x ∞) ⟩□
¬ A          □
; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _} _ → trivial _ _) ⟩□
Laterˡ⁻¹-∼≈      □
}
where

module _ (laterˡ⁻¹-∼≈ : Laterˡ⁻¹-∼≈) (x : A) where

mutual

now≈never : ∀ {i} → [ i ] now x ≈ never
now≈never = laterˡ⁻¹-∼≈ (later now∼never)

now∼never : ∀ {i} → [ i ] now x ∼′ never
force now∼never {j = j} = ⊥-elim (contradiction j)

contradiction : Size → ⊥
contradiction i = now≉never (now≈never {i = i})

-- A variant of Laterˡ⁻¹-∼≈ which it is sometimes easier to work with.

Laterˡ⁻¹-∼≈′ = ∀ {i} {x : A} →
[ i ] later (record { force = now x }) ∼ never →
[ i ] now x                            ≈ never

size-preserving-laterˡ⁻¹-∼≈′⇔uninhabited : Laterˡ⁻¹-∼≈′ ⇔ ¬ A
size-preserving-laterˡ⁻¹-∼≈′⇔uninhabited =
Laterˡ⁻¹-∼≈′  ↝⟨ record { to   = _∘ transitive-∼ʳ (later λ { .force → now })
; from = _∘ transitive-∼ʳ (later λ { .force → now })
} ⟩
Laterˡ⁻¹-∼≈   ↝⟨ size-preserving-laterˡ⁻¹-∼≈⇔uninhabited ⟩□
¬ A           □

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

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

size-preserving-laterʳ⁻¹-∼≈⇔uninhabited : Laterʳ⁻¹-∼≈ ⇔ ¬ A
size-preserving-laterʳ⁻¹-∼≈⇔uninhabited =
Laterʳ⁻¹-∼≈   ↝⟨ record { to   = λ laterʳ⁻¹ → symmetric ∘ laterʳ⁻¹ ∘ symmetric
; from = λ laterˡ⁻¹ → symmetric ∘ laterˡ⁻¹ ∘ symmetric
} ⟩
Laterˡ⁻¹-∼≈′  ↝⟨ size-preserving-laterˡ⁻¹-∼≈′⇔uninhabited ⟩□
¬ A           □

-- A variant of laterʳ⁻¹ for expansion 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 : A} →
[ i ] never ∼ later (record { force = now x }) →
[ i ] never ≳ now x

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ʳ⁻¹-∼≳      □
}

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

Laterˡ⁻¹-≈ = ∀ {i x} {y : Delay A ∞} →
[ i ] later x ≈ y → [ i ] force x ≈ 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ˡ⁻¹-≈       □
}

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

Laterʳ⁻¹-≈ = ∀ {i} {x : Delay A ∞} {y} →
[ i ] x ≈ later y → [ i ] x ≈ force y

size-preserving-laterʳ⁻¹-≈⇔uninhabited : Laterʳ⁻¹-≈ ⇔ ¬ A
size-preserving-laterʳ⁻¹-≈⇔uninhabited =
Laterʳ⁻¹-≈  ↝⟨ record { to   = λ laterʳ⁻¹ → symmetric ∘ laterʳ⁻¹ ∘ symmetric
; from = λ laterˡ⁻¹ → symmetric ∘ laterˡ⁻¹ ∘ symmetric
} ⟩
Laterˡ⁻¹-≈  ↝⟨ size-preserving-laterˡ⁻¹-≈⇔uninhabited ⟩□

¬ A         □

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

Laterʳ⁻¹-≳ = ∀ {i} {x : Delay A ∞} {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ʳ⁻¹-≳       □
}

-- A variant of ⇓-respects-≈ in which _≈_ is replaced by _∼_ can be
-- made size-preserving in the second argument iff A is uninhabited.

⇓-Respects-∼ʳ = ∀ {i x y} {z : A} →
x ⇓ z → [ i ] x ∼ y → Terminates i y z

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

-- The lemma ⇓-respects-≈ can be made size-preserving in the second
-- argument iff A is uninhabited.

⇓-Respects-≈ʳ = ∀ {i x y} {z : A} →
x ⇓ z → [ i ] x ≈ y → Terminates i y z

size-preserving-⇓-respects-≈ʳ⇔uninhabited : ⇓-Respects-≈ʳ ⇔ ¬ A
size-preserving-⇓-respects-≈ʳ⇔uninhabited = record
{ to   = ⇓-Respects-≈ʳ  ↝⟨ (λ resp x⇓z → resp x⇓z ∘ ∼→) ⟩
⇓-Respects-∼ʳ  ↝⟨ _⇔_.to size-preserving-⇓-respects-∼ʳ⇔uninhabited ⟩□
¬ A            □
; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
⇓-Respects-≈ʳ    □
}

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

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

size-preserving-transitivity-≈∼ʳ⇔uninhabited : Transitivity-≈∼ʳ ⇔ ¬ A
size-preserving-transitivity-≈∼ʳ⇔uninhabited = record
{ to   = Transitivity-≈∼ʳ  ↝⟨ (λ trans → trans) ⟩
⇓-Respects-∼ʳ     ↝⟨ _⇔_.to size-preserving-⇓-respects-∼ʳ⇔uninhabited ⟩□
¬ A               □
; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≈∼ʳ  □
}

-- There is a transitivity-like proof, taking strong bisimilarity and
-- weak bisimilarity 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 =
Transitivity-∼≈ˡ  ↝⟨ record { to   = λ trans {_ _ _ _} p q →
symmetric (trans (symmetric q) (symmetric p))
; from = λ trans {_ _ _ _} p q →
symmetric (trans (symmetric q) (symmetric p))
} ⟩
Transitivity-≈∼ʳ  ↝⟨ size-preserving-transitivity-≈∼ʳ⇔uninhabited ⟩□

¬ A               □

-- There is a transitivity-like proof, taking strong bisimilarity and
-- expansion to expansion, 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 for weak bisimilarity that preserves
-- the size of the second argument iff A is uninhabited.

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

size-preserving-transitivity-≈ʳ⇔uninhabited : Transitivity-≈ʳ ⇔ ¬ A
size-preserving-transitivity-≈ʳ⇔uninhabited = record
{ to   = Transitivity-≈ʳ  ↝⟨ (λ trans → trans) ⟩
⇓-Respects-≈ʳ    ↝⟨ _⇔_.to size-preserving-⇓-respects-≈ʳ⇔uninhabited ⟩□
¬ A              □
; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≈ʳ  □
}

-- There is a transitivity proof for 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 =
Transitivity-≈ˡ  ↝⟨ record { to   = λ trans {_ _ _ _} p q →
symmetric (trans (symmetric q) (symmetric p))
; from = λ trans {_ _ _ _} p q →
symmetric (trans (symmetric q) (symmetric p))
} ⟩
Transitivity-≈ʳ  ↝⟨ size-preserving-transitivity-≈ʳ⇔uninhabited ⟩□

¬ A              □

-- There is a transitivity proof for expansion 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 fully size-preserving transitivity proof for weak
-- bisimilarity 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-≈   ↝⟨ (λ trans → trans) ⟩
Transitivity-≈ˡ  ↝⟨ _⇔_.to size-preserving-transitivity-≈ˡ⇔uninhabited ⟩
¬ A              □
; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≈   □
}

-- The following two lemmas provide an alternative proof of one
-- direction of the previous lemma (with a small change to one of the
-- types).

-- If there is a transitivity proof for weak bisimilarity that is
-- size-preserving in both arguments, then weak bisimilarity is
-- trivial.

size-preserving-transitivity-≈→trivial :
(∀ {i} x {y z : Delay A ∞} →
[ i ] x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z) →
∀ {i} (x y : Delay A ∞) → [ i ] x ≈ y
size-preserving-transitivity-≈→trivial _≈⟨_⟩ʷ_ x y =
(x                         ≈⟨ laterʳ (x ∎ʷ) ⟩ʷ
(later (λ { .force → x })  ≈⟨ later (λ { .force → size-preserving-transitivity-≈→trivial _≈⟨_⟩ʷ_ x y }) ⟩ʷ
(later (λ { .force → y })  ≈⟨ laterˡ (y ∎ʷ) ⟩ʷ
(y                         ∎ʷ))))
where
_∎ʷ = reflexive

-- If there is a transitivity proof for weak bisimilarity that is
-- size-preserving in both arguments, then the carrier type A is not
-- inhabited.

size-preserving-transitivity-≈→uninhabited :
(∀ {i} x {y z : Delay A ∞} →
[ i ] x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z) →
¬ A
size-preserving-transitivity-≈→uninhabited trans x =
now≉never (size-preserving-transitivity-≈→trivial trans (now x) never)

-- There is a fully size-preserving transitivity proof for expansion
-- 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 transitivity-like proof, taking expansion and weak
-- bisimilarity 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-≳≈ˡ  ↝⟨ _∘ ∼→ ⟩
Transitivity-∼≈ˡ  ↝⟨ _⇔_.to size-preserving-transitivity-∼≈ˡ⇔uninhabited ⟩
¬ A               □
; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≳≈ˡ  □
}

-- There is a transitivity-like proof, taking expansion and weak
-- bisimilarity to weak bisimilarity, 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 transitivity-like proof, taking weak bisimilarity and
-- the converse of expansion to weak bisimilarity, that preserves the
-- size of the second argument iff A is uninhabited.

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

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

-- There is a transitivity-like proof, taking weak bisimilarity and
-- the converse of expansion to weak bisimilarity, 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 =
Transitivity-≈≲  ↝⟨ record { to   = λ trans x≳y y≈z → symmetric (trans (symmetric y≈z) x≳y)
; from = λ trans x≈y y≲z → symmetric (trans y≲z (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 _))) ⟩
Laterʳ⁻¹-≈        ↝⟨ _⇔_.to size-preserving-laterʳ⁻¹-≈⇔uninhabited ⟩
¬ A               □
; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≈≳ˡ  □
}
```