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

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

open import Prelude.Size

{a} {A : Size → Set a} where

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

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

------------------------------------------------------------------------
-- Lemmas stating that functions of certain types cannot be defined if
-- ∀ i → A i is inhabited

-- An abbreviation. (Note that, because pattern-matching lambdas like
-- the one in this definition are—at least at the time of
-- writing—compared by "name", Agda rejects the code that one gets if
-- this abbreviation is inlined below.)

later-now : (∀ i → A i) → ∀ {i} → Delay A i
later-now x = later λ { .force {j} → now (x j) }

-- If now (x ∞) is an expansion of later-now x for every
-- x : ∀ i → A i, then ∀ i → A i is uninhabited.

Now≳later-now = (x : ∀ i → A i) → now (x ∞) ≳ later-now x

now≳later-now→uninhabited : Now≳later-now → ¬ (∀ i → A i)
now≳later-now→uninhabited =
Now≳later-now  ↝⟨ (λ hyp x → case hyp x of λ ()) ⟩□
¬ (∀ i → A i)  □

-- If a variant of laterˡ⁻¹ for (fully defined) expansion can be
-- defined, then ∀ i → A i is uninhabited.

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

laterˡ⁻¹-≳→uninhabited : Laterˡ⁻¹-≳ → ¬ (∀ i → A i)
laterˡ⁻¹-≳→uninhabited =
Laterˡ⁻¹-≳     ↝⟨ (λ hyp _ → hyp (reflexive _)) ⟩
Now≳later-now  ↝⟨ now≳later-now→uninhabited ⟩□
¬ (∀ i → A i)  □

-- If the following variants of transitivity can be proved, then
-- ∀ i → A i 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-≈≳≳ → ¬ (∀ i → A i)
transitive-≈≳≳→uninhabited =
Transitivity-≈≳≳  ↝⟨ (λ trans → trans (laterʳ (reflexive _))) ⟩
Laterˡ⁻¹-≳        ↝⟨ laterˡ⁻¹-≳→uninhabited ⟩□
¬ (∀ i → A i)     □

transitive-≳≈≳→uninhabited : Transitivity-≳≈≳ → ¬ (∀ i → A i)
transitive-≳≈≳→uninhabited =
Transitivity-≳≈≳  ↝⟨ (λ trans x → later⁻¹ {y = λ { .force → later-now x }}
(trans (reflexive _) (laterʳ (reflexive _)))) ⟩
Now≳later-now     ↝⟨ now≳later-now→uninhabited ⟩□
¬ (∀ i → A i)     □

------------------------------------------------------------------------
-- Lemmas stating that certain size-preserving functions cannot be
-- defined if ∀ i → A i is inhabited, and related results

-- If 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, then ∀ i → A i is
-- uninhabited.
--
-- This lemma is used to prove all other similar results below
-- (directly or indirectly).

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

size-preserving-laterˡ⁻¹-∼≈→uninhabited :
Laterˡ⁻¹-∼≈ → ¬ (∀ i → A i)
size-preserving-laterˡ⁻¹-∼≈→uninhabited laterˡ⁻¹-∼≈ x =
where

mutual

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

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

contradiction i = now≉never (now≈never {i = i})

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

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

size-preserving-laterˡ⁻¹-∼≈⇔size-preserving-laterˡ⁻¹-∼≈′ :
Laterˡ⁻¹-∼≈ ⇔ Laterˡ⁻¹-∼≈′
size-preserving-laterˡ⁻¹-∼≈⇔size-preserving-laterˡ⁻¹-∼≈′ = record
{ to   = λ laterˡ⁻¹ x → laterˡ⁻¹ x ∘ transitive-∼ˡ (later λ { .force → now })
; from = λ laterˡ⁻¹ x → laterˡ⁻¹ x ∘ transitive-∼ˡ (later λ { .force → now })
}

-- The type Laterˡ⁻¹-∼≈′ is logically equivalent to the similar type
-- Laterʳ⁻¹-∼≈′.

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

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

-- The type Laterʳ⁻¹-∼≈′ is logically equivalent to the similar type
-- Laterʳ⁻¹-∼≳′.

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

size-preserving-laterʳ⁻¹-∼≈′⇔size-preserving-laterʳ⁻¹-∼≳′ :
Laterʳ⁻¹-∼≈′ ⇔ Laterʳ⁻¹-∼≳′
size-preserving-laterʳ⁻¹-∼≈′⇔size-preserving-laterʳ⁻¹-∼≳′ =
Laterʳ⁻¹-∼≈′  ↝⟨ record { to   = λ laterʳ⁻¹ {_} _ → ≈→-now ∘ laterʳ⁻¹ _
; from = λ laterʳ⁻¹ {_} _ → ≳→     ∘ laterʳ⁻¹ _
} ⟩□
Laterʳ⁻¹-∼≳′  □

-- If Laterʳ⁻¹-∼≳′ is inhabited, then ∀ i → A i is uninhabited.

size-preserving-laterʳ⁻¹-∼≳′→uninhabited : Laterʳ⁻¹-∼≳′ → ¬ (∀ i → A i)
size-preserving-laterʳ⁻¹-∼≳′→uninhabited =
Laterʳ⁻¹-∼≳′   ↝⟨ _⇔_.from size-preserving-laterʳ⁻¹-∼≈′⇔size-preserving-laterʳ⁻¹-∼≳′ ⟩
Laterʳ⁻¹-∼≈′   ↝⟨ _⇔_.from size-preserving-laterˡ⁻¹-∼≈′⇔size-preserving-laterʳ⁻¹-∼≈′ ⟩
Laterˡ⁻¹-∼≈′   ↝⟨ _⇔_.from size-preserving-laterˡ⁻¹-∼≈⇔size-preserving-laterˡ⁻¹-∼≈′ ⟩
Laterˡ⁻¹-∼≈    ↝⟨ size-preserving-laterˡ⁻¹-∼≈→uninhabited ⟩□
¬ (∀ i → A i)  □

-- Having a size-preserving variant of laterˡ⁻¹ is logically
-- equivalent to having a size-preserving variant of laterʳ⁻¹ (for
-- weak bisimilarity).

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

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

size-preserving-laterˡ⁻¹-≈⇔size-preserving-laterʳ⁻¹-≈ :
Laterˡ⁻¹-≈ ⇔ Laterʳ⁻¹-≈
size-preserving-laterˡ⁻¹-≈⇔size-preserving-laterʳ⁻¹-≈ = record
{ to   = λ laterʳ⁻¹ → symmetric ∘ laterʳ⁻¹ ∘ symmetric
; from = λ laterˡ⁻¹ → symmetric ∘ laterˡ⁻¹ ∘ symmetric
}

-- If laterˡ⁻¹ can be made size-preserving, then ∀ i → A i is
-- uninhabited.

size-preserving-laterˡ⁻¹-≈→uninhabited : Laterˡ⁻¹-≈ → ¬ (∀ i → A i)
size-preserving-laterˡ⁻¹-≈→uninhabited =
Laterˡ⁻¹-≈     ↝⟨ (λ laterˡ⁻¹ _ → laterˡ⁻¹ ∘ ∼→) ⟩
Laterˡ⁻¹-∼≈    ↝⟨ size-preserving-laterˡ⁻¹-∼≈→uninhabited ⟩□
¬ (∀ i → A i)  □

-- If laterʳ⁻¹ can be made size-preserving for expansion, then
-- ∀ i → A i is uninhabited.

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

size-preserving-laterʳ⁻¹-≳→uninhabited : Laterʳ⁻¹-≳ → ¬ (∀ i → A i)
size-preserving-laterʳ⁻¹-≳→uninhabited =
Laterʳ⁻¹-≳     ↝⟨ (λ laterʳ⁻¹ {_} _ p → laterʳ⁻¹ (∼→ p)) ⟩
Laterʳ⁻¹-∼≳′   ↝⟨ size-preserving-laterʳ⁻¹-∼≳′→uninhabited ⟩□
¬ (∀ i → A i)  □

-- If a variant of ⇓-respects-≈ in which _≈_ is replaced by _∼_ can be
-- made size-preserving in the second argument, then ∀ i → A i is
-- uninhabited.

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

size-preserving-⇓-respects-∼ʳ→uninhabited :
⇓-Respects-∼ʳ → ¬ (∀ i → A i)
size-preserving-⇓-respects-∼ʳ→uninhabited =
⇓-Respects-∼ʳ  ↝⟨ (λ resp _ → resp (laterʳ now)) ⟩
Laterˡ⁻¹-∼≈    ↝⟨ size-preserving-laterˡ⁻¹-∼≈→uninhabited ⟩□
¬ (∀ i → A i)  □

-- If ⇓-respects-≈ can be made size-preserving in the second argument,
-- then ∀ i → A i is uninhabited.

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

size-preserving-⇓-respects-≈ʳ→uninhabited :
⇓-Respects-≈ʳ → ¬ (∀ i → A i)
size-preserving-⇓-respects-≈ʳ→uninhabited =
⇓-Respects-≈ʳ  ↝⟨ (λ trans x⇓z → trans x⇓z ∘ ∼→) ⟩
⇓-Respects-∼ʳ  ↝⟨ size-preserving-⇓-respects-∼ʳ→uninhabited ⟩□
¬ (∀ i → A i)  □

-- Having a transitivity-like proof, taking weak bisimilarity and
-- strong bisimilarity to weak bisimilarity, that preserves the size
-- of the second argument, is logically equivalent to having a
-- transitivity-like proof, taking strong bisimilarity and weak
-- bisimilarity to weak bisimilarity, that preserves the size of the
-- first argument.

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

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

size-preserving-transitivity-≈∼ʳ⇔size-preserving-transitivity-∼≈ˡ :
Transitivity-≈∼ʳ ⇔ Transitivity-∼≈ˡ
size-preserving-transitivity-≈∼ʳ⇔size-preserving-transitivity-∼≈ˡ =
record
{ to   = λ trans p q → symmetric (trans (symmetric q) (symmetric p))
; from = λ trans p q → symmetric (trans (symmetric q) (symmetric p))
}

-- If there is a transitivity-like proof, taking weak bisimilarity and
-- strong bisimilarity to weak bisimilarity, that preserves the size
-- of the second argument, then ∀ i → A i is uninhabited.

size-preserving-transitivity-≈∼ʳ→uninhabited :
Transitivity-≈∼ʳ → ¬ (∀ i → A i)
size-preserving-transitivity-≈∼ʳ→uninhabited =
Transitivity-≈∼ʳ  ↝⟨ (λ trans → trans) ⟩
⇓-Respects-∼ʳ     ↝⟨ size-preserving-⇓-respects-∼ʳ→uninhabited ⟩
¬ (∀ i → A i)     □

-- If there is a transitivity-like proof, taking strong bisimilarity
-- and expansion to expansion, that preserves the size of the first
-- argument, then ∀ i → A i is uninhabited.

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

size-preserving-transitivity-∼≳ˡ→uninhabited :
Transitivity-∼≳ˡ → ¬ (∀ i → A i)
size-preserving-transitivity-∼≳ˡ→uninhabited =
Transitivity-∼≳ˡ  ↝⟨ (λ trans _ p → trans p (laterˡ now)) ⟩
Laterʳ⁻¹-∼≳′      ↝⟨ size-preserving-laterʳ⁻¹-∼≳′→uninhabited ⟩
¬ (∀ i → A i)     □

-- Having a transitivity proof for weak bisimilarity that preserves
-- the size of the first argument is logically equivalent to having
-- one that preserves the size of the second argument.

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

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

size-preserving-transitivity-≈ˡ⇔size-preserving-transitivity-≈ʳ :
Transitivity-≈ˡ ⇔ Transitivity-≈ʳ
size-preserving-transitivity-≈ˡ⇔size-preserving-transitivity-≈ʳ = record
{ to   = λ trans p q → symmetric (trans (symmetric q) (symmetric p))
; from = λ trans p q → symmetric (trans (symmetric q) (symmetric p))
}

-- If there is a transitivity proof for weak bisimilarity that
-- preserves the size of the second argument, then ∀ i → A i is
-- uninhabited.

size-preserving-transitivity-≈ʳ→uninhabited :
Transitivity-≈ʳ → ¬ (∀ i → A i)
size-preserving-transitivity-≈ʳ→uninhabited =
Transitivity-≈ʳ  ↝⟨ (λ trans → trans) ⟩
⇓-Respects-≈ʳ    ↝⟨ size-preserving-⇓-respects-≈ʳ→uninhabited ⟩□
¬ (∀ i → A i)    □

-- If there is a transitivity proof for expansion that preserves the
-- size of the first argument, then ∀ i → A i is uninhabited.

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

size-preserving-transitivity-≳ˡ→uninhabited :
Transitivity-≳ˡ → ¬ (∀ i → A i)
size-preserving-transitivity-≳ˡ→uninhabited =
Transitivity-≳ˡ   ↝⟨ (λ trans → trans ∘ ∼→) ⟩
Transitivity-∼≳ˡ  ↝⟨ size-preserving-transitivity-∼≳ˡ→uninhabited ⟩□
¬ (∀ i → A i)     □

-- If there is a fully size-preserving transitivity proof for weak
-- bisimilarity, then ∀ i → A i is uninhabited.

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

size-preserving-transitivity-≈→uninhabited :
Transitivity-≈ → ¬ (∀ i → A i)
size-preserving-transitivity-≈→uninhabited =
Transitivity-≈   ↝⟨ (λ trans → trans) ⟩
Transitivity-≈ʳ  ↝⟨ size-preserving-transitivity-≈ʳ→uninhabited ⟩□
¬ (∀ i → A i)    □

-- If there is a fully size-preserving transitivity proof for
-- expansion, then ∀ i → A i is uninhabited.

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

size-preserving-transitivity-≳→uninhabited :
Transitivity-≳ → ¬ (∀ i → A i)
size-preserving-transitivity-≳→uninhabited =
Transitivity-≳   ↝⟨ (λ trans → trans) ⟩
Transitivity-≳ˡ  ↝⟨ size-preserving-transitivity-≳ˡ→uninhabited ⟩□
¬ (∀ i → A i)    □

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

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

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

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

-- If there is a transitivity-like proof, taking expansion and weak
-- bisimilarity to weak bisimilarity, that preserves the size of the
-- first argument, then ∀ i → A i is uninhabited.

size-preserving-transitivity-≳≈ˡ→uninhabited :
Transitivity-≳≈ˡ → ¬ (∀ i → A i)
size-preserving-transitivity-≳≈ˡ→uninhabited =
Transitivity-≳≈ˡ  ↝⟨ _∘ ∼→ ⟩
Transitivity-∼≈ˡ  ↝⟨ _⇔_.from size-preserving-transitivity-≈∼ʳ⇔size-preserving-transitivity-∼≈ˡ ⟩
Transitivity-≈∼ʳ  ↝⟨ size-preserving-transitivity-≈∼ʳ→uninhabited ⟩□
¬ (∀ i → A i)     □

-- There is a transitivity-like proof, taking expansion and weak
-- bisimilarity to weak bisimilarity, that preserves the size of both
-- arguments, iff there is a transitivity-like proof, taking weak
-- bisimilarity and the converse of expansion to weak bisimilarity,
-- that also preserves the size of both arguments.

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

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

size-preserving-transitivity-≳≈⇔size-preserving-transitivity-≈≲ :
Transitivity-≳≈ ⇔ Transitivity-≈≲
size-preserving-transitivity-≳≈⇔size-preserving-transitivity-≈≲ =
record
{ to   = λ trans x≈y y≲z → symmetric (trans y≲z (symmetric x≈y))
; from = λ trans x≳y y≈z → symmetric (trans (symmetric y≈z) x≳y)
}

-- If there is a transitivity-like proof, taking expansion and weak
-- bisimilarity to weak bisimilarity, that preserves the size of both
-- arguments, then ∀ i → A i is uninhabited.

size-preserving-transitivity-≳≈→uninhabited :
Transitivity-≳≈ → ¬ (∀ i → A i)
size-preserving-transitivity-≳≈→uninhabited =
Transitivity-≳≈   ↝⟨ (λ trans → trans) ⟩
Transitivity-≳≈ˡ  ↝⟨ size-preserving-transitivity-≳≈ˡ→uninhabited ⟩□
¬ (∀ i → A i)     □

-- If there is a transitivity-like proof, taking weak bisimilarity and
-- expansion to weak bisimilarity, that preserves the size of the
-- first argument, then ∀ i → A i is uninhabited.

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

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

------------------------------------------------------------------------
-- Lemmas stating that certain types are inhabited if A ∞ is
-- uninhabited

-- If A ∞ is uninhabited, then Now≳later-now is inhabited.

uninhabited→now≳later-now : ¬ A ∞ → Now≳later-now
uninhabited→now≳later-now =
¬ A ∞            ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≳ y)  ↝⟨ (λ trivial _ → trivial _ _) ⟩□
Now≳later-now    □

-- If A ∞ is uninhabited, then a variant of laterˡ⁻¹ for (fully
-- defined) expansion can be defined.

uninhabited→laterˡ⁻¹-≳ : ¬ A ∞ → Laterˡ⁻¹-≳
uninhabited→laterˡ⁻¹-≳ =
¬ A ∞            ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _} _ → trivial _ _) ⟩□
Laterˡ⁻¹-≳       □

-- If A ∞ is uninhabited, then a transitivity-like proof taking weak
-- bisimilarity and expansion to expansion can be defined.

uninhabited→transitivity-≈≳≳ : ¬ A ∞ → Transitivity-≈≳≳
uninhabited→transitivity-≈≳≳ =
¬ A ∞             ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≳ y)   ↝⟨ (λ trivial {_ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≈≳≳  □

-- If A ∞ is uninhabited, then a transitivity-like proof taking
-- expansion and weak bisimilarity to expansion can be defined.

uninhabited→transitivity-≳≈≳ : ¬ A ∞ → Transitivity-≳≈≳
uninhabited→transitivity-≳≈≳ =
¬ A ∞             ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≳ y)   ↝⟨ (λ trivial {_ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≳≈≳  □

-- If A ∞ is uninhabited, then Laterˡ⁻¹-∼≈ is inhabited.

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

-- If A ∞ is uninhabited, then laterˡ⁻¹ can be made size-preserving.

uninhabited→size-preserving-laterˡ⁻¹ : ¬ A ∞ → Laterˡ⁻¹-≈
uninhabited→size-preserving-laterˡ⁻¹ =
¬ A ∞            ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _} _ → trivial _ _) ⟩□
Laterˡ⁻¹-≈       □

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

uninhabited→size-preserving-⇓-respects-∼ʳ : ¬ A ∞ → ⇓-Respects-∼ʳ
uninhabited→size-preserving-⇓-respects-∼ʳ =
¬ A ∞            ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
⇓-Respects-∼ʳ    □

-- If A ∞ is uninhabited, then ⇓-respects-≈ can be made
-- size-preserving in the second argument.

uninhabited→size-preserving-⇓-respects-≈ʳ : ¬ A ∞ → ⇓-Respects-≈ʳ
uninhabited→size-preserving-⇓-respects-≈ʳ =
¬ A ∞            ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
⇓-Respects-≈ʳ    □

-- If A ∞ is uninhabited, then there is a transitivity-like proof,
-- taking weak bisimilarity and strong bisimilarity to weak
-- bisimilarity, that preserves the size of the second argument.

uninhabited→size-preserving-transitivity-≈∼ʳ : ¬ A ∞ → Transitivity-≈∼ʳ
uninhabited→size-preserving-transitivity-≈∼ʳ =
¬ A ∞             ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≈∼ʳ  □

-- If A ∞ is uninhabited, then there is a transitivity-like proof,
-- taking strong bisimilarity and expansion to expansion, that
-- preserves the size of the first argument.

uninhabited→size-preserving-transitivity-∼≳ˡ : ¬ A ∞ → Transitivity-∼≳ˡ
uninhabited→size-preserving-transitivity-∼≳ˡ =
¬ A ∞             ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≳ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-∼≳ˡ  □

-- If A ∞ is uninhabited, then there is a transitivity proof for weak
-- bisimilarity that preserves the size of the second argument.

uninhabited→size-preserving-transitivity-≈ʳ : ¬ A ∞ → Transitivity-≈ʳ
uninhabited→size-preserving-transitivity-≈ʳ =
¬ A ∞            ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≈ʳ  □

-- If A ∞ is uninhabited, then there is a transitivity proof for
-- expansion that preserves the size of the first argument.

uninhabited→size-preserving-transitivity-≳ˡ : ¬ A ∞ → Transitivity-≳ˡ
uninhabited→size-preserving-transitivity-≳ˡ =
¬ A ∞            ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≳ˡ  □

-- If A ∞ is uninhabited, then there is a fully size-preserving
-- transitivity proof for weak bisimilarity.

uninhabited→size-preserving-transitivity-≈ : ¬ A ∞ → Transitivity-≈
uninhabited→size-preserving-transitivity-≈ =
¬ A ∞            ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≈   □

-- If A ∞ is uninhabited, then there is a fully size-preserving
-- transitivity proof for expansion.

uninhabited→size-preserving-transitivity-≳ : ¬ A ∞ → Transitivity-≳
uninhabited→size-preserving-transitivity-≳ =
¬ A ∞            ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≳   □

-- If A ∞ is uninhabited, then there is a transitivity-like proof,
-- taking expansion and weak bisimilarity to weak bisimilarity, that
-- preserves the size of the first argument.

uninhabited→size-preserving-transitivity-≳≈ˡ : ¬ A ∞ → Transitivity-≳≈ˡ
uninhabited→size-preserving-transitivity-≳≈ˡ =
¬ A ∞             ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≳≈ˡ  □

-- If A ∞ is uninhabited, then there is a transitivity-like proof,
-- taking expansion and weak bisimilarity to weak bisimilarity, that
-- preserves the size of both arguments.

uninhabited→size-preserving-transitivity-≳≈ : ¬ A ∞ → Transitivity-≳≈
uninhabited→size-preserving-transitivity-≳≈ =
¬ A ∞            ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≳≈  □

-- If A ∞ is uninhabited, then there is a transitivity-like proof,
-- taking weak bisimilarity and expansion to weak bisimilarity, that
-- preserves the size of the first argument.

uninhabited→size-preserving-transitivity-≈≳ˡ : ¬ A ∞ → Transitivity-≈≳ˡ
uninhabited→size-preserving-transitivity-≈≳ˡ =
¬ A ∞             ↝⟨ uninhabited→trivial ⟩
(∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
Transitivity-≈≳ˡ  □
```