derive WEM from the injectivity of the Dedekind reals

source/DedekindReals/Addition.lagda

@@ -370,7 +370,7 @@ open import Rationals.Multiplication renaming (_*_ to _ℚ*_)
   inhabited-left-z = ∥∥-rec ∃-is-prop I (binary-choice (inhabited-from-real-L x) (inhabited-from-real-R x))
    where
     I : (Σ a ꞉ ℚ , a < x) × (Σ b ꞉ ℚ , b > x) → ∃ p ꞉ ℚ , p ∈ L
-    I ((a , a<x) , b ,  x<b) = ∥∥-functor II (located-from-real x (ℚ- b) (ℚ- a) (ℚ<-swap a b (disjoint-from-real x a b (a<x , x<b))))
+    I ((a , a<x) , b ,  x<b) = ∥∥-functor II (ℝ-locatedness x (ℚ- b) (ℚ- a) (ℚ<-swap a b (disjoint-from-real x a b (a<x , x<b))))
      where
       II : ((ℚ- b) < x) ∔ (ℚ- a) > x → Σ p ꞉ ℚ , p ∈ L
       II (inl z) = (ℚ- b) , ∣ b , x<b , refl ∣
@@ -380,7 +380,7 @@ open import Rationals.Multiplication renaming (_*_ to _ℚ*_)
   inhabited-right-z = ∥∥-rec ∃-is-prop I (binary-choice (inhabited-from-real-L x) (inhabited-from-real-R x))
    where
     I : (Σ a ꞉ ℚ , a < x) × (Σ b ꞉ ℚ , b > x) → ∃ q ꞉ ℚ , q ∈ R
-    I ((a , a<x) , b , x<b) = ∥∥-functor II (located-from-real x (ℚ- b) (ℚ- a) (ℚ<-swap a b (disjoint-from-real x a b (a<x , x<b))))
+    I ((a , a<x) , b , x<b) = ∥∥-functor II (ℝ-locatedness x (ℚ- b) (ℚ- a) (ℚ<-swap a b (disjoint-from-real x a b (a<x , x<b))))
      where
       II : ((ℚ- b) < x) ∔ (ℚ- a) > x → Σ q ꞉ ℚ , q ∈ R
       II (inl z) = b      , ∣ ℚ- b , z , (ℚ-minus-minus b) ∣
@@ -454,7 +454,7 @@ open import Rationals.Multiplication renaming (_*_ to _ℚ*_)
       II = disjoint-from-real x q' p' (x<q' , p'<x)
 
   located-z : located L R
-  located-z p q p<q = ∥∥-functor I (located-from-real x (ℚ- q) (ℚ- p) (ℚ<-swap p q p<q))
+  located-z p q p<q = ∥∥-functor I (ℝ-locatedness x (ℚ- q) (ℚ- p) (ℚ<-swap p q p<q))
    where
     I : (ℚ- q) < x ∔ (ℚ- p) > x → p ∈ L ∔ q ∈ R
     I (inl -q<x) = inr ∣ (ℚ- q) , -q<x , ℚ-minus-minus q ∣
@@ -482,7 +482,7 @@ x - y = x + (- y)
         e'' = e ∙ ap (r ℚ+_) e'
         III : (p < 0ℚ) ∔ (p ＝ 0ℚ) ∔ (0ℚ < p) → p < 0ℝ
         III (inl p<0)       = p<0
-        III (inr (inl p＝0)) = 𝟘-elim (ℚ<-not-itself k (transport (_< k) i r<k))
+        III (inr (inl p＝0)) = 𝟘-elim (ℚ<-irrefl k (transport (_< k) i r<k))
          where
           i : r ＝ k
           i = r                  ＝⟨ ℚ-inverse-intro r k ⟩
@@ -492,7 +492,7 @@ x - y = x + (- y)
               p ℚ+ k             ＝⟨ ap (_ℚ+ k) p＝0 ⟩
               0ℚ ℚ+ k            ＝⟨ ℚ-zero-left-neutral k ⟩
               k ∎
-        III (inr (inr 0<p)) = 𝟘-elim (ℚ<-not-itself k (ℚ<-trans k r k k<r r<k))
+        III (inr (inr 0<p)) = 𝟘-elim (ℚ<-irrefl k (ℚ<-trans k r k k<r r<k))
          where
           i : 0ℚ < r ℚ- k
           i = transport (0ℚ <_) e'' 0<p

source/DedekindReals/Order.lagda

@@ -88,7 +88,7 @@ weak-linearity x y z l = ∥∥-rec ∨-is-prop I l
     II ((r , r<q , rRx) , s , q<s , sLy) = ∥∥-rec ∨-is-prop IV III
      where
       III : (r < z) ∨ (z < s)
-      III = located-from-real z r s (ℚ<-trans r q s r<q q<s)
+      III = ℝ-locatedness z r s (ℚ<-trans r q s r<q q<s)
       IV : (r < z) ∔ (z < s) → (x < z) ∨ (z < y)
       IV (inl rLz) = ∣ inl ∣ r , rRx , rLz ∣ ∣
       IV (inr sRz) = ∣ inr ∣ s , sRz , sLy ∣ ∣
@@ -98,7 +98,7 @@ weak-linearity' x y z l = do
  (q , x<q , q<y) ← l
  (r , r<q , x<r) ← rounded-right-b (upper-cut-of x) (rounded-from-real-R x) q x<q
  (s , q<s , s<y) ← rounded-left-b (lower-cut-of y) (rounded-from-real-L y) q q<y
- t               ← located-from-real z r s (ℚ<-trans r q s r<q q<s)
+ t               ← ℝ-locatedness z r s (ℚ<-trans r q s r<q q<s)
  Cases t (λ r<z → ∣ inl ∣ r , x<r , r<z ∣ ∣)
          (λ z<s → ∣ inr ∣ s , z<s , s<y ∣ ∣)
 
@@ -141,7 +141,7 @@ apartness-gives-inequality x y apart e = ∥∥-rec 𝟘-is-prop I apart
 ℝ-not-less-is-greater-or-equal x y nl p pLy = ∥∥-rec (∈-is-prop (lower-cut-of x) p) I (rounded-left-b (lower-cut-of y) (rounded-from-real-L y) p pLy)
  where
   I : Σ q ꞉ ℚ , p < q < y → p < x
-  I (q , l , q<y) = ∥∥-rec (∈-is-prop (lower-cut-of x) p) II (located-from-real x p q l)
+  I (q , l , q<y) = ∥∥-rec (∈-is-prop (lower-cut-of x) p) II (ℝ-locatedness x p q l)
    where
     II : p < x ∔ q > x → p < x
     II (inl p<x) = p<x
@@ -158,10 +158,10 @@ apartness-gives-inequality x y apart e = ∥∥-rec 𝟘-is-prop I apart
     II = rounded-right-b (upper-cut-of y) (rounded-from-real-R y) q qRy
 
     III : Σ k ꞉ ℚ , k < q × k > y → q > x
-    III (k , k<q , kRy) = ∥∥-rec (∈-is-prop (upper-cut-of x) q) IV (located-from-real x k q k<q)
+    III (k , k<q , kRy) = ∥∥-rec (∈-is-prop (upper-cut-of x) q) IV (ℝ-locatedness x k q k<q)
      where
       IV : k < x ∔ q > x → q > x
-      IV (inl kLx) = 𝟘-elim (ℚ<-not-itself k (disjoint-from-real y k k (x≤y k kLx , kRy)))
+      IV (inl kLx) = 𝟘-elim (ℚ<-irrefl k (disjoint-from-real y k k (x≤y k kLx , kRy)))
       IV (inr qRx) = qRx
 
 <ℝ-irreflexive : (x : ℝ) → x ≮ x
@@ -186,3 +186,33 @@ embedding-preserves-order p q l = I (use-rationals-density)
   I (k , p<k , k<q) = ∣ k , p<k , k<q ∣
 
 \end{code}
+
+Added by Martin Escardo 24th August 2023, adapted from Various.Dedekind.
+
+\begin{code}
+
+≤-ℝ-ℝ-antisym : (x y : ℝ) → x ≤ y → y ≤ x → x ＝ y
+≤-ℝ-ℝ-antisym = ℝ-equality-from-left-cut'
+
+♯-is-tight : (x y : ℝ) → ¬ (x ♯ y) → x ＝ y
+♯-is-tight x y ν = ≤-ℝ-ℝ-antisym x y III IV
+ where
+  I : x ≮ y
+  I ℓ = ν ∣ inl ℓ ∣
+
+  II : y ≮ x
+  II ℓ = ν ∣ inr ℓ ∣
+
+  III : x ≤ y
+  III = ℝ-not-less-is-greater-or-equal y x II
+
+  IV : y ≤ x
+  IV = ℝ-not-less-is-greater-or-equal x y I
+
+ℝ-is-¬¬-separated : (x y : ℝ) → ¬¬ (x ＝ y) → x ＝ y
+ℝ-is-¬¬-separated x y ϕ = ♯-is-tight x y (c ϕ)
+ where
+  c : ¬¬ (x ＝ y) → ¬ (x ♯ y)
+  c = contrapositive (apartness-gives-inequality x y)
+
+\end{code}

source/DedekindReals/Properties.lagda

@@ -36,7 +36,7 @@ open import Rationals.Limits fe pe pt
 open PropositionalTruncation pt
 
 trans→disjoint : (L R : 𝓟 ℚ) → disjoint L R → (q : ℚ) → ¬ (q ∈ L × q ∈ R)
-trans→disjoint L R d q (q∈L , q∈R) = ℚ<-not-itself q γ
+trans→disjoint L R d q (q∈L , q∈R) = ℚ<-irrefl q γ
  where
   γ : q < q
   γ = d q q (q∈L , q∈R)
@@ -110,7 +110,7 @@ disjoint→trans L R loc dis p q (p∈L , q∈R) = cases₃ γ₁ γ₂ γ₃ I
      = ∨-elim ∃-is-prop γ₂ γ₃ IV
      where
       IV : (u < x) ∨ (x < v)
-      IV = located-from-real x u v u<v
+      IV = ℝ-locatedness x u v u<v
 
       γ₂ : (u < x) → ∃ (u , v) ꞉ ℚ × ℚ , (u < x < v) × (v - u < ε)
       γ₂ u<x = γ₁ n u q u<x x<q V (transport (_< ε) α l)

source/DedekindReals/Type.lagda

@@ -141,8 +141,8 @@ in-lower-cut q ((L , R) , _) = q ∈ L
 in-upper-cut : ℚ → ℝ → 𝓤₀ ̇
 in-upper-cut q ((L , R) , _) = q ∈ R
 
-located-from-real : (((L , R) , _) : ℝ) → (p q : ℚ) → p < q → p ∈ L ∨ q ∈ R
-located-from-real ((L , R) , _ , _ , _ , _ , _ , located-y) = located-y
+ℝ-locatedness : (((L , R) , _) : ℝ) → (p q : ℚ) → p < q → p ∈ L ∨ q ∈ R
+ℝ-locatedness ((L , R) , _ , _ , _ , _ , _ , located-y) = located-y
 
 inhabited-from-real-L : (((L , R) , i) : ℝ) → inhabited-left L
 inhabited-from-real-L ((L , R) , inhabited-L , _) = inhabited-L
@@ -203,7 +203,7 @@ instance
  _<_<_ {{Strict-Order-Chain-ℝ-ℚ-ℝ}} p q r = (p < q) × (q < r)
 
 ℚ<-not-itself-from-ℝ : (p : ℚ) → (x : ℝ) → ¬ (p < x < p)
-ℚ<-not-itself-from-ℝ p x (l₁ , l₂) = ℚ<-not-itself p (disjoint-from-real x p p (l₁ , l₂))
+ℚ<-not-itself-from-ℝ p x (l₁ , l₂) = ℚ<-irrefl p (disjoint-from-real x p p (l₁ , l₂))
 
 embedding-ℚ-to-ℝ : ℚ → ℝ
 embedding-ℚ-to-ℝ x = (L , R) , inhabited-left'
@@ -320,7 +320,7 @@ instance
         use-located : q' ∈ Ly ∨ q ∈ Ry
         use-located = located-y q' q q'<q
         III : q' ∈ Ly ∔ q ∈ Ry → q ∈ Ry
-        III (inl q'-Ly) = 𝟘-elim (ℚ<-not-itself q' from-above)
+        III (inl q'-Ly) = 𝟘-elim (ℚ<-irrefl q' from-above)
          where
           get-contradiction : q' ∈ Lx
           get-contradiction = Ly⊆Lx q' q'-Ly
@@ -340,7 +340,7 @@ instance
         use-located : q' ∈ Lx ∨ q ∈ Rx
         use-located = located-x q' q q'<q
         III : q' ∈ Lx ∔ q ∈ Rx → q ∈ Rx
-        III (inl q'-Lx) = 𝟘-elim (ℚ<-not-itself q' from-above)
+        III (inl q'-Lx) = 𝟘-elim (ℚ<-irrefl q' from-above)
          where
           get-contradiction : q' ∈ Ly
           get-contradiction = Lx⊆Ly q' q'-Lx

source/InjectiveTypes/CounterExamples.lagda

@@ -30,13 +30,16 @@ module InjectiveTypes.CounterExamples
         (pt : propositional-truncations-exist)
        where
 
+open PropositionalTruncation pt
+
 open import MLTT.Spartan
 open import UF.Embeddings
 open import UF.ExcludedMiddle
 open import UF.FunExt
 open import UF.Miscelanea
 open import UF.Retracts
 open import UF.Subsingletons
+open import UF.Subsingletons-FunExt
 open import UF.UA-FunExt
 open import Taboos.Decomposability ua
 
@@ -109,7 +112,8 @@ conclusion.
 
 \begin{code}
 
-simple-type₂-injective-gives-WEM : (X : 𝓤₀ ̇) → simple-type₂ X → ainjective-type X 𝓤 𝓤 → WEM 𝓤
+simple-type₂-injective-gives-WEM : (X : 𝓤₀ ̇)
+                                 → simple-type₂ X → ainjective-type X 𝓤 𝓤 → WEM 𝓤
 simple-type₂-injective-gives-WEM X s X-ainj =
  𝟚-injective-gives-WEM (retract-of-ainjective 𝟚 X X-ainj (simple-types₂-disconnected s))
 
@@ -140,49 +144,158 @@ universe 𝓤₁.
 
 \begin{code}
 
-open import DedekindReals.Type fe' pe pt renaming (0ℝ to 0ᴿ ; 1ℝ to 1ᴿ)
+open import DedekindReals.Type fe' pe pt
 open import DedekindReals.Order fe' pe pt
 open import Notation.Order
 
 ℝ-ainjective-gives-Heaviside-function : ainjective-type ℝ 𝓤₁ 𝓤₁
                                       → Σ H ꞉ (ℝ → ℝ) ,
-                                            ((x : ℝ) → (x < 0ᴿ → H x ＝ 0ᴿ)
-                                                     × (x ≥ 0ᴿ → H x ＝ 1ᴿ))
+                                            ((x : ℝ) → (x < 0ℝ → H x ＝ 0ℝ)
+                                                     × (x ≥ 0ℝ → H x ＝ 1ℝ))
 ℝ-ainjective-gives-Heaviside-function ℝ-ainj = H , γ
  where
-  j : (Σ x ꞉ ℝ , x < 0ᴿ) + (Σ x ꞉ ℝ , x ≥ 0ᴿ) → ℝ
+  j : (Σ x ꞉ ℝ , x < 0ℝ) + (Σ x ꞉ ℝ , x ≥ 0ℝ) → ℝ
   j = cases pr₁ pr₁
 
   j-is-embedding : is-embedding j
   j-is-embedding = disjoint-cases-embedding pr₁ pr₁
-                    (pr₁-is-embedding (λ x → <-is-prop x 0ᴿ))
-                    (pr₁-is-embedding (λ x → ≤-is-prop 0ᴿ x))
+                    (pr₁-is-embedding (λ x → <-is-prop x 0ℝ))
+                    (pr₁-is-embedding (λ x → ≤-is-prop 0ℝ x))
                     d
    where
     d : disjoint-images pr₁ pr₁
-    d (x , l) (x , b) refl = <ℝ-irreflexive x (ℝ<-≤-trans x 0ᴿ x l b)
+    d (x , l) (x , b) refl = <ℝ-irreflexive x (ℝ<-≤-trans x 0ℝ x l b)
 
-  h : (Σ x ꞉ ℝ , x < 0ᴿ) + (Σ x ꞉ ℝ , x ≥ 0ᴿ) → ℝ
-  h = cases (λ _ → 0ᴿ) (λ _ → 1ᴿ)
+  h : (Σ x ꞉ ℝ , x < 0ℝ) + (Σ x ꞉ ℝ , x ≥ 0ℝ) → ℝ
+  h = cases (λ _ → 0ℝ) (λ _ → 1ℝ)
 
   H : ℝ → ℝ
   H = pr₁ (ℝ-ainj j j-is-embedding h)
 
   H-extends-h-along-j : ∀ u → H (j u) ＝ h u
   H-extends-h-along-j = pr₂ (ℝ-ainj j j-is-embedding h)
 
-  γ : (x : ℝ) → (x < 0ᴿ → H x ＝ 0ᴿ)
-              × (x ≥ 0ᴿ → H x ＝ 1ᴿ)
+  γ : (x : ℝ) → (x < 0ℝ → H x ＝ 0ℝ)
+              × (x ≥ 0ℝ → H x ＝ 1ℝ)
   γ x = I , II
    where
-    I : x < 0ᴿ → H x ＝ 0ᴿ
+    I : x < 0ℝ → H x ＝ 0ℝ
     I l = H-extends-h-along-j (inl (x , l))
 
-    II : x ≥ 0ᴿ → H x ＝ 1ᴿ
+    II : x ≥ 0ℝ → H x ＝ 1ℝ
     II b = H-extends-h-along-j (inr (x , b))
 
 \end{code}
 
+But we can do better than that and derive weak excluded middle from
+the injectivity of ℝ.
+
+\begin{code}
+
+open import Rationals.Type
+open import Rationals.Order
+
+ℝ-ainjective-gives-WEM : ainjective-type ℝ (𝓤₁ ⊔ 𝓥) 𝓤₁ → WEM 𝓥
+ℝ-ainjective-gives-WEM ℝ-ainj P P-is-prop = XI
+ where
+  j : (ℝ × P) + (ℝ × ¬ P) → ℝ
+  j = cases pr₁ pr₁
+
+  j-is-embedding : is-embedding j
+  j-is-embedding = disjoint-cases-embedding pr₁ pr₁
+                    (pr₁-is-embedding
+                      (λ _ → P-is-prop))
+                    (pr₁-is-embedding
+                      (λ _ → holds-is-prop (¬ P , negations-are-props fe')))
+                    d
+   where
+    d : disjoint-images pr₁ pr₁
+    d (x , p) (x , ν) refl = ν p
+
+  h : (ℝ × P) + (ℝ × ¬ P) → ℝ
+  h = cases (λ _ → 0ℝ) (λ _ → 1ℝ)
+
+  H : ℝ → ℝ
+  H = pr₁ (ℝ-ainj j j-is-embedding h)
+
+  H-extends-h-along-j : ∀ u → H (j u) ＝ h u
+  H-extends-h-along-j = pr₂ (ℝ-ainj j j-is-embedding h)
+
+  x₀ : ℝ
+  x₀ = 0ℝ -- Arbitrary choice. Any number will do.
+
+  I : P → H x₀ ＝ 0ℝ
+  I p = H-extends-h-along-j (inl (x₀ , p))
+
+  II : ¬ P → H x₀ ＝ 1ℝ
+  II ν = H-extends-h-along-j (inr (x₀ , ν))
+
+  I-II : H x₀ ≠ 0ℝ → H x₀ ≠ 1ℝ → 𝟘
+  I-II u v = contrapositive II v (contrapositive I u)
+
+  I-II₀ : H x₀ ≠ 1ℝ → H x₀ ＝ 0ℝ
+  I-II₀ v = ℝ-is-¬¬-separated (H x₀) 0ℝ (λ u → I-II u v)
+
+  I-II₁ : H x₀ ≠ 0ℝ → H x₀ ＝ 1ℝ
+  I-II₁ u = ℝ-is-¬¬-separated (H x₀) 1ℝ (I-II u)
+
+  III : (1/4 < H x₀) ∨ (H x₀ < 1/2)
+  III = ℝ-locatedness (H x₀) 1/4 1/2 1/4<1/2
+
+  IV : 1/4 < H x₀ → H x₀ ＝ 1ℝ
+  IV l = I-II₁ IV₀
+   where
+     IV₀ : H x₀ ≠ 0ℝ
+     IV₀ e = ℚ<-irrefl 1/4 IV₃
+      where
+       IV₁ : 1/4 < 0ℝ
+       IV₁ = transport (1/4 <_) e l
+       IV₂ : 1/4 < 0ℚ
+       IV₂ = IV₁
+       IV₃ : 1/4 < 1/4
+       IV₃ = ℚ<-trans 1/4 0ℚ 1/4 IV₂ 0<1/4
+
+  V : H x₀ < 1/2 → H x₀ ＝ 0ℝ
+  V l = I-II₀ V₀
+   where
+     V₀ : H x₀ ≠ 1ℝ
+     V₀ e = ℚ<-irrefl 1/2 V₃
+      where
+       V₁ : 1ℝ < 1/2
+       V₁ = transport (_< 1/2) e l
+       V₂ : 1ℚ < 1/2
+       V₂ = V₁
+       V₃ : 1/2 < 1/2
+       V₃ = ℚ<-trans 1/2 1ℚ 1/2 1/2<1 V₂
+
+  VI : H x₀ ＝ 0ℝ → ¬¬ P
+  VI e ν = apartness-gives-inequality 0ℝ 1ℝ
+           ℝ-zero-apart-from-one
+            (0ℝ   ＝⟨ e ⁻¹ ⟩
+             H x₀ ＝⟨ II ν ⟩
+             1ℝ   ∎)
+
+  VII : H x₀ ＝ 1ℝ → ¬ P
+  VII e p = apartness-gives-inequality 0ℝ 1ℝ
+             ℝ-zero-apart-from-one
+             (0ℝ   ＝⟨ (I p)⁻¹ ⟩
+             H x₀  ＝⟨ e ⟩
+             1ℝ    ∎)
+
+  VIII : H x₀ < 1/2 → ¬¬ P
+  VIII l = VI (V l)
+
+  IX :  1/4 ℚ<ℝ H x₀ → ¬ P
+  IX l = VII (IV l)
+
+  X : ¬ P ∨ ¬¬ P
+  X = ∨-functor IX VIII III
+
+  XI : ¬ P + ¬¬ P
+  XI = exit-∥∥ (decidability-of-prop-is-prop fe' (negations-are-props fe')) X
+
+\end{code}
+
 The injectivity of ℕ∞, the conatural numbers, or generic convergent
 sequence, gives WLPO. Like in the previous example, we first use
 injectivity to define a non-continuous function.