Martin Escardo and Tom de Jong, August 2024

Moved from the file InjectiveTypes.CounterExamples on 12 September 2024.

\begin{code}

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

open import UF.PropTrunc

module Apartness.Properties
        (pt : propositional-truncations-exist)
       where

open import MLTT.Spartan
open import Apartness.Definition
open import UF.ClassicalLogic
open import UF.FunExt
open import UF.Size
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

open Apartness pt
open PropositionalTruncation pt

\end{code}

We define an apartness relation to be nontrivial if it tells two points apart.

\begin{code}

has-two-points-apart : {X : 𝓀 Μ‡ } β†’ Apartness X π“₯ β†’ π“₯ βŠ” 𝓀 Μ‡
has-two-points-apart {𝓀} {π“₯} {X} (_β™―_ , Ξ±) = Ξ£ (x , y) κž‰ X Γ— X , (x β™― y)

Nontrivial-Apartness : 𝓀 Μ‡ β†’ (π“₯ : Universe) β†’ π“₯ ⁺ βŠ” 𝓀 Μ‡
Nontrivial-Apartness X π“₯ = Ξ£ a κž‰ Apartness X π“₯ , has-two-points-apart a

\end{code}

Assuming weak excluded middle, every type with two distinct points can be
equipped with a nontrivial apartness relation.

\begin{code}

WEM-gives-that-type-with-two-distinct-points-has-nontrivial-apartness
 : funext 𝓀 𝓀₀
 β†’ {X : 𝓀 Μ‡ }
 β†’ has-two-distinct-points X
 β†’ typal-WEM 𝓀
 β†’ Nontrivial-Apartness X 𝓀
WEM-gives-that-type-with-two-distinct-points-has-nontrivial-apartness
 {𝓀} fe {X} htdp wem = Ξ³
 where
  s : (x y z : X) β†’ x β‰  y β†’ (x β‰  z) + (y β‰  z)
  s x y z d =
   Cases (wem (x β‰  z))
    (Ξ» (a : Β¬ (x β‰  z))  β†’ inr (Ξ» {refl β†’ a d}))
    (Ξ» (b : ¬¬ (x β‰  z)) β†’ inl (three-negations-imply-one b))

  c : is-cotransitive _β‰ _
  c x y z d = ∣ s x y z d ∣

  Ξ³ : Nontrivial-Apartness X 𝓀
  Ξ³ = (_β‰ _ ,
      ((Ξ» x y β†’ negations-are-props fe) ,
       β‰ -is-irrefl ,
       (Ξ» x y β†’ β‰ -sym) , c)) ,
      htdp

WEM-gives-that-type-with-two-distinct-points-has-nontrivial-apartness⁺
 : funext 𝓀 𝓀₀
 β†’ {X : 𝓀 ⁺ Μ‡ }
 β†’ is-locally-small X
 β†’ has-two-distinct-points X
 β†’ typal-WEM 𝓀
 β†’ Nontrivial-Apartness X 𝓀
WEM-gives-that-type-with-two-distinct-points-has-nontrivial-apartness⁺
 {𝓀} fe {X} ls ((xβ‚€ , x₁) , d) wem = Ξ³
 where
  _β™―_ : X β†’ X β†’ 𝓀 Μ‡
  x β™― y = x β‰ βŸ¦ ls ⟧ y

  s : (x y z : X) β†’ x β™― y β†’ (x β™― z) + (y β™― z)
  s x y z a = Cases (wem (x β™― z)) (inr ∘ f) (inl ∘ g)
   where
    f : Β¬ (x β™― z) β†’ y β™― z
    f = contrapositive
         (Ξ» (e : y ＝⟦ ls ⟧ z) β†’ transport (x β™―_) (＝⟦ ls ⟧-gives-＝ e) a)

    g : ¬¬ (x β™― z) β†’ x β™― z
    g = three-negations-imply-one

  c : is-cotransitive _β™―_
  c x y z d = ∣ s x y z d ∣

  Ξ³ : Nontrivial-Apartness X 𝓀
  Ξ³ = (_β™―_ ,
       (Ξ» x y β†’ negations-are-props fe) ,
       (Ξ» x β†’ β‰ βŸ¦ ls ⟧-irrefl) ,
       (Ξ» x y β†’ β‰ βŸ¦ ls ⟧-sym) ,
       c) ,
      (xβ‚€ , x₁) , β‰ -gives-β‰ βŸ¦ ls ⟧ d

\end{code}

In particular, weak excluded middle yields a nontrivial apartness relation on
any universe.

\begin{code}

WEM-gives-non-trivial-apartness-on-universe
 : funext (𝓀 ⁺) 𝓀₀
 β†’ typal-WEM (𝓀 ⁺)
 β†’ Nontrivial-Apartness (𝓀 Μ‡ ) (𝓀 ⁺)
WEM-gives-non-trivial-apartness-on-universe fe =
 WEM-gives-that-type-with-two-distinct-points-has-nontrivial-apartness
  fe
  universe-has-two-distinct-points

\end{code}

Further properties of apartness relations can be found in the following file
InjectiveTypes.CounterExamples. In particular, it is shown that the universe
can't have any nontrivial apartness unless weak excluded middle holds.