weak excluded middle implies WLPO

martinescardo · Aug 24, 2023 · 0c9be1f · 0c9be1f
1 parent e12fcf9
commit 0c9be1f
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/source/Taboos/WLPO.lagda b/source/Taboos/WLPO.lagda
@@ -71,3 +71,17 @@ WLPO-gives-ℕ∞-discrete fe wlpo u v =
 More discussion about WLPO is included in the modules
 TheTopologyOfTheUniverse and FailureOfTotalSeparatedness, among
 others.
+
+Notice that weak excluded middle implies WLPO.
+
+\begin{code}
+
+open import UF.ExcludedMiddle
+
+WEM-gives-WLPO : FunExt → WEM 𝓤₀ → WLPO
+WEM-gives-WLPO fe wem u = Cases (wem (u ＝ ∞) (ℕ∞-is-set (fe 𝓤₀ 𝓤₀)))
+                           (λ (p : (u ≠ ∞))
+                                 → inr p)
+                           (λ (ν : ¬ (u ≠ ∞))
+                                 → inl (ℕ∞-is-¬¬-separated (fe 𝓤₀ 𝓤₀) u ∞ ν))
+\end{code}