------------------------------------------------------------------------ -- 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-≈≳ˡ □ }