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

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

open import Size

module Delay-monad.Sized.Bisimilarity.Negative
  {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; _∘_)

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

------------------------------------------------------------------------
-- 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 =
  contradiction 
  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 : Size  
    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-≈≳ˡ