If all tight apartness relations on the Cantor type agree then WLPO i…

…mplies LPO (#337)

* If all tight apartness relations on the Cantor type agree then WLPO implies LPO

* Clean up

source/Apartness/Definition.lagda

@@ -101,6 +101,17 @@ module Apartness (pt : propositional-truncations-exist) where
  Apartness : 𝓤 ̇ → (𝓥 : Universe) → 𝓥 ⁺ ⊔ 𝓤 ̇
  Apartness X 𝓥 = Σ _♯_ ꞉ (X → X → 𝓥 ̇) , is-apartness _♯_
 
+ cotransitive-if-strongly-cotransitive : {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
+                                       → is-strongly-cotransitive _♯_
+                                       → is-cotransitive _♯_
+ cotransitive-if-strongly-cotransitive _♯_ sc x y z a = ∣ sc x y z a ∣
+
+ strong-apartness-is-apartness : {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
+                               → is-strong-apartness _♯_
+                               → is-apartness _♯_
+ strong-apartness-is-apartness _♯_ (p , i , s , c) =
+  p , i , s , cotransitive-if-strongly-cotransitive _♯_ c
+
  Tight-Apartness : 𝓤 ̇  → (𝓥 : Universe) → 𝓥 ⁺ ⊔ 𝓤 ̇
  Tight-Apartness X 𝓥 = Σ _♯_ ꞉ (X → X → 𝓥 ̇) , is-apartness _♯_ × is-tight _♯_
 

source/Apartness/Properties.lagda

@@ -12,8 +12,15 @@ module Apartness.Properties
         (pt : propositional-truncations-exist)
        where
 
-open import MLTT.Spartan
 open import Apartness.Definition
+open import MLTT.Spartan
+open import MLTT.Two-Properties
+open import NotionsOfDecidability.DecidableClassifier
+open import Taboos.LPO
+open import Taboos.WLPO
+open import TypeTopology.Cantor renaming (_♯_ to _♯[Cantor]_) hiding (_＝⟦_⟧_)
+open import TypeTopology.TotallySeparated
+open import UF.Base
 open import UF.ClassicalLogic
 open import UF.FunExt
 open import UF.Size
@@ -22,6 +29,7 @@ open import UF.Subsingletons-FunExt
 
 open Apartness pt
 open PropositionalTruncation pt
+open total-separatedness-via-apartness pt
 
 \end{code}
 
@@ -143,3 +151,115 @@ EM-gives-tight-apartness-is-≠ dne X (_♯_ , ♯-is-apartness , ♯-is-tight)
   III = I , II
 
 \end{code}
+
+Added 1 February 2025 by Tom de Jong.
+
+The above shows that classically any type can have at most one tight apartness
+(the one given by negation of equality). We show that the Cantor type (ℕ → 𝟚)
+cannot be shown to have at most one tight apartness relation in constructive
+mathematics: the statement that the Cantor type has at most one tight apartness
+relation implies (WLPO ⇒ LPO) which is a constructive taboo as there are
+(topological) models of intuitionistic set theory that validate WLPO but not
+LPO, see the fifth page and Theorem 5.1 of the paper below.
+
+Matt Hendtlass and Robert Lubarsky. 'Separating Fragments of WLEM, LPO, and MP'
+The Journal of Symbolic Logic. Vol. 81, No. 4, 2016, pp. 1315-1343.
+DOI: 10.1017/jsl.2016.38
+URL: https://www.math.fau.edu/people/faculty/lubarsky/separating-llpo.pdf
+
+\begin{code}
+
+At-Most-One-Tight-Apartness : (X : 𝓤 ̇  ) (𝓥 : Universe) → (𝓥 ⁺ ⊔ 𝓤) ̇
+At-Most-One-Tight-Apartness X 𝓥 = is-prop (Tight-Apartness X 𝓥)
+
+At-Most-One-Tight-Apartness-on-Cantor-gives-WLPO-implies-LPO
+ : Fun-Ext
+ → At-Most-One-Tight-Apartness Cantor 𝓤₀
+ → WLPO-variation₂ → LPO-variation
+At-Most-One-Tight-Apartness-on-Cantor-gives-WLPO-implies-LPO  fe hyp wlpo = VI
+ where
+  _♯_ = _♯[Cantor]_
+
+  has-root : Cantor → 𝓤₀ ̇
+  has-root α = Σ n ꞉ ℕ , α n ＝ ₀
+
+  P⁺ : (α : Cantor) → Σ b ꞉ 𝟚 , (b ＝ ₀ ↔ ¬¬ (has-root α))
+                              × (b ＝ ₁ ↔ ¬ (has-root α))
+  P⁺ α = boolean-value' (wlpo α)
+
+  P : Cantor → 𝟚
+  P α = pr₁ (P⁺ α)
+  P-specification₀ : (α : Cantor) → P α ＝ ₀ ↔ ¬¬ (has-root α)
+  P-specification₀ α = pr₁ (pr₂ (P⁺ α))
+  P-specification₁ : (α : Cantor) → P α ＝ ₁ ↔ ¬ (has-root α)
+  P-specification₁ α = pr₂ (pr₂ (P⁺ α))
+
+  P-of-𝟏-is-₁ : P 𝟏 ＝ ₁
+  P-of-𝟏-is-₁ = rl-implication (P-specification₁ 𝟏) I
+   where
+    I : ¬ has-root (λ n → ₁)
+    I (n , p) = one-is-not-zero p
+
+  P-differentiates-at-𝟏-specification : (α : Cantor)
+                                      → P α ≠ P 𝟏 ↔ ¬¬ (has-root α)
+  P-differentiates-at-𝟏-specification α = I , II
+   where
+    I : P α ≠ P 𝟏 → ¬¬ has-root α
+    I ν = lr-implication (P-specification₀ α) I₂
+     where
+      I₁ : P α ＝ ₁ → P α ＝ ₀
+      I₁ e = 𝟘-elim (ν (e ∙ P-of-𝟏-is-₁ ⁻¹))
+      I₂ : P α ＝ ₀
+      I₂ = 𝟚-equality-cases id I₁
+    II : ¬¬ has-root α → P α ≠ P 𝟏
+    II ν e = ν (lr-implication (P-specification₁ α) (e ∙ P-of-𝟏-is-₁))
+
+  I : (α : Cantor) → ¬¬ (has-root α) → α ♯₂ 𝟏
+  I α ν = ∣ P , rl-implication (P-differentiates-at-𝟏-specification α) ν ∣
+
+  II : (α : Cantor) → α ♯ 𝟏 ↔ has-root α
+  II α = II₁ , II₂
+   where
+    II₁ : α ♯ 𝟏 → has-root α
+    II₁ a = pr₁ has-root' , 𝟚-equality-cases id (λ p → 𝟘-elim (pr₂ has-root' p))
+     where
+      has-root' : Σ n ꞉ ℕ , α n ≠ ₁
+      has-root' = apartness-criterion-converse α 𝟏 a
+    II₂ : has-root α → α ♯ 𝟏
+    II₂ (n , p) = apartness-criterion α 𝟏
+                   (n , λ (q : α n ＝ ₁) → zero-is-not-one (p ⁻¹ ∙ q))
+
+  III : (α : Cantor) → α ♯₂ 𝟏 → α ♯ 𝟏
+  III α = Idtofun (eq α 𝟏)
+   where
+    eq : (α β : Cantor) → α ♯₂ β ＝ α ♯ β
+    eq α β =
+     happly
+      (happly
+       (ap pr₁
+           (hyp (_♯₂_ ,
+                 ♯₂-is-apartness ,
+                 ♯₂-is-tight (Cantor-is-totally-separated fe))
+                (_♯_ ,
+                 ♯-is-apartness fe pt ,
+                 ♯-is-tight fe)))
+       α)
+      β
+
+  IV : (α : Cantor) → ¬¬-stable (has-root α)
+  IV α ν = lr-implication (II α) (III α (I α ν))
+
+  recall : (α : Cantor) → type-of (wlpo α) ＝ is-decidable (¬ (has-root α))
+  recall α = refl
+
+  V : (α : Cantor) → is-decidable (has-root α)
+  V α = κ (wlpo α)
+   where
+    κ : is-decidable (¬ (has-root α)) → is-decidable (has-root α)
+    κ (inl p) = inr p
+    κ (inr q) = inl (IV α q)
+
+  VI : LPO-variation
+  VI = V
+
+\end{code}

source/Taboos/LPO.lagda

@@ -276,3 +276,37 @@ LPO-gives-WLPO fe lpo u =
 ¬WLPO-gives-¬LPO fe = contrapositive (LPO-gives-WLPO fe)
 
 \end{code}
+
+Added 1 February 2025 by Tom de Jong.
+The following type is logically equivalent to LPO but it should be noted that it
+is not a proposition.
+
+\begin{code}
+
+LPO-variation : 𝓤₀ ̇
+LPO-variation = (α : ℕ → 𝟚) → is-decidable (Σ n ꞉ ℕ , α n ＝ ₀)
+
+LPO-variation-implies-LPO : funext₀ → LPO-variation → LPO
+LPO-variation-implies-LPO fe lpovar = compact-ℕ-gives-LPO fe I
+ where
+  I : is-compact ℕ
+  I α = κ (lpovar α)
+   where
+    κ : is-decidable (Σ n ꞉ ℕ , α n ＝ ₀)
+      → (Σ n ꞉ ℕ , α n ＝ ₀) + (Π n ꞉ ℕ , α n ＝ ₁)
+    κ (inl r) = inl r
+    κ (inr ν) = inr (λ n → 𝟚-equality-cases
+                            (λ (e : α n ＝ ₀) → 𝟘-elim (ν (n , e)))
+                            id)
+
+LPO-implies-LPO-variation : funext₀ → LPO → LPO-variation
+LPO-implies-LPO-variation fe lpo α = I (LPO-gives-compact-ℕ fe lpo α)
+ where
+  I : (Σ n ꞉ ℕ , α n ＝ ₀) + (Π n ꞉ ℕ , α n ＝ ₁)
+    → is-decidable (Σ n ꞉ ℕ , α n ＝ ₀)
+  I (inl r) = inl r
+  I (inr ν) = inr (Π-not-implies-not-Σ
+                    (λ n (e : α n ＝ ₀) → 𝟘-elim
+                                           (zero-is-not-one (e ⁻¹ ∙ (ν n)))))
+
+\end{code}

source/Taboos/WLPO.lagda

@@ -157,13 +157,13 @@ a binary sequence is decidable.
 
 \begin{code}
 
-WLPO-variation : 𝓤₀ ̇
-WLPO-variation = (α : ℕ → 𝟚) → is-decidable ((n : ℕ) → α n ＝ α 0)
+WLPO-variation₁ : 𝓤₀ ̇
+WLPO-variation₁ = (α : ℕ → 𝟚) → is-decidable ((n : ℕ) → α n ＝ α 0)
 
-WLPO-variation-gives-WLPO-traditional
- : WLPO-variation
+WLPO-variation₁-gives-WLPO-traditional
+ : WLPO-variation₁
  → WLPO-traditional
-WLPO-variation-gives-WLPO-traditional wlpov α
+WLPO-variation₁-gives-WLPO-traditional wlpov α
  = 𝟚-equality-cases I II
  where
   I : α 0 ＝ ₀ → ((n : ℕ) → α n ＝ ₁) + ¬ ((n : ℕ) → α n ＝ ₁)
@@ -188,3 +188,42 @@ WLPO-variation-gives-WLPO-traditional wlpov α
 \end{code}
 
 TODO. The converse.
+
+Added 1 February 2025 by Tom de Jong.
+
+\begin{code}
+
+WLPO-variation₂ : 𝓤₀ ̇
+WLPO-variation₂ = (α : ℕ → 𝟚) → is-decidable (¬ (Σ n ꞉ ℕ , α n ＝ ₀))
+
+WLPO-traditional-gives-WLPO-variation₂ : WLPO-traditional → WLPO-variation₂
+WLPO-traditional-gives-WLPO-variation₂ wlpo α = κ (wlpo α)
+ where
+  κ : is-decidable (Π n ꞉ ℕ , α n ＝ ₁) → is-decidable (¬ (Σ n ꞉ ℕ , α n ＝ ₀))
+  κ (inl p) = inl (Π-not-implies-not-Σ I)
+   where
+    I : (n : ℕ) → α n ≠ ₀
+    I n e = zero-is-not-one (e ⁻¹ ∙ p n)
+  κ (inr q) = inr (¬¬-functor I (not-Π-implies-not-not-Σ II q))
+   where
+    I : (Σ n ꞉ ℕ , α n ≠ ₁) → (Σ n ꞉ ℕ , α n ＝ ₀)
+    I (n , ν) = n , 𝟚-equality-cases id (λ (e : α n ＝ ₁) → 𝟘-elim (ν e))
+    II : (n : ℕ) → ¬¬-stable (α n ＝ ₁)
+    II n = 𝟚-is-¬¬-separated (α n) ₁
+
+WLPO-variation₂-gives-traditional-WLPO : WLPO-variation₂ → WLPO-traditional
+WLPO-variation₂-gives-traditional-WLPO wlpovar α = κ (wlpovar α)
+ where
+  κ : is-decidable (¬ (Σ n ꞉ ℕ , α n ＝ ₀)) → is-decidable (Π n ꞉ ℕ , α n ＝ ₁)
+  κ (inl p) = inl (λ n → I n (II n))
+   where
+    I : (n : ℕ) → ¬ (α n ＝ ₀) → (α n ＝ ₁)
+    I n ν = 𝟚-equality-cases (λ (e : α n ＝ ₀) → 𝟘-elim (ν e)) id
+    II : (n : ℕ) → ¬ (α n ＝ ₀)
+    II = not-Σ-implies-Π-not p
+  κ (inr q) = inr (contrapositive I q)
+   where
+    I : (Π n ꞉ ℕ , α n ＝ ₁) → ¬ (Σ n ꞉ ℕ , α n ＝ ₀)
+    I h (n , e) = zero-is-not-one (e ⁻¹ ∙ h n)
+
+\end{code}

source/TypeTopology/Cantor.lagda

@@ -269,6 +269,18 @@ The apartness axioms are satisfied, and, moreover, the apartness is tight.
   III : (α ♯ γ) + (β ♯ γ)
   III = II I
 
+♯-is-strong-apartness : Fun-Ext → is-strong-apartness _♯_
+♯-is-strong-apartness fe = ♯-is-prop-valued fe ,
+                           ♯-is-irreflexive ,
+                           ♯-is-symmetric ,
+                           ♯-strongly-cotransitive
+
+♯-is-apartness : (fe : Fun-Ext)
+               → (pt : propositional-truncations-exist)
+               → is-apartness pt _♯_
+♯-is-apartness fe pt =
+ strong-apartness-is-apartness pt _♯_ (♯-is-strong-apartness fe)
+
 ♯-is-tight : Fun-Ext → is-tight _♯_
 ♯-is-tight fe α β ν = dfunext fe I
  where

source/TypeTopology/DecidabilityOfNonContinuity.lagda

@@ -1368,9 +1368,9 @@ being-modulus-of-constancy-is-decidable-for-all-functions-gives-WLPO
        → is-decidable (m is-modulus-of-constancy-of g))
  → WLPO
 being-modulus-of-constancy-is-decidable-for-all-functions-gives-WLPO ϕ
- = WLPO-traditional-gives-WLPO fe (WLPO-variation-gives-WLPO-traditional I)
+ = WLPO-traditional-gives-WLPO fe (WLPO-variation₁-gives-WLPO-traditional I)
  where
-  I : WLPO-variation
+  I : WLPO-variation₁
   I α = I₂
    where
     g : ℕ → ℕ

source/TypeTopology/SimpleTypes.lagda

@@ -151,4 +151,4 @@ cfdbce₂ s t c = tscd₀ (simple-types₂-totally-separated s)
                  (simple-types₂-pointed s)
                  c
 
-\end{code}
+\end{code}

source/TypeTopology/TotallySeparated.lagda

@@ -813,4 +813,6 @@ module total-separatedness-via-apartness
    α : (p : X → 𝟚) → p x ＝ p y
    α p = 𝟚-is-¬¬-separated (p x) (p y) (λ u → h (p , u))
 
+ ♯₂-is-tight = totally-separated-gives-totally-separated₃
+
 \end{code}