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

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

module Delay-monad.Bisimilarity.Negative {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 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-≈≳ˡ  
  }