Martin Escardo, December 2017 (but done much earlier on paper) As discussed in the module CompactTypes, Bishop's "limited principle of omniscience" amount to the compactness of the type ℕ, that is, Π p ꞉ ℕ → 𝟚 , (Σ n ꞉ ℕ , p n ≡ ₀) + (Π n ꞉ ℕ , p n ≡ ₁), which fails in contructive mathematics (here in the sense that it is independent - it is not provable, and its negation is also not provable). This is in general not a univalent proposition, because there may be many n:ℕ with p n ≡ ₀. In univalent mathematics, we may get a proposition by truncating the Σ to get the existential quantifier ∃ (see the Homotopy Type Theory book). Here instead we construct the truncation directly, and call it LPO. Using this and the module Prop-Tychonoff, we show that the function type LPO→ℕ is compact, despite the fact that LPO is undecided in our type theory. (We needed to add new helper lemmas in the module GenericConvergentSequence) \begin{code} {-# OPTIONS --without-K --exact-split --safe #-} open import UF-FunExt module LPO (fe : FunExt) where open import SpartanMLTT open import Two-Properties open import UF-Base open import UF-Subsingletons open import UF-Subsingletons-FunExt open import GenericConvergentSequence open import CompactTypes open import NaturalsOrder LPO : 𝓤₀ ̇ LPO = (x : ℕ∞) → decidable (Σ n ꞉ ℕ , x ≡ under n) LPO-is-prop : is-prop LPO LPO-is-prop = Π-is-prop (fe 𝓤₀ 𝓤₀) f where a : (x : ℕ∞) → is-prop (Σ n ꞉ ℕ , x ≡ under n) a x (n , p) (m , q) = to-Σ-≡ (under-lc (p ⁻¹ ∙ q) , ℕ∞-is-set (fe 𝓤₀ 𝓤₀)_ _) f : (x : ℕ∞) → is-prop (decidable (Σ n ꞉ ℕ , x ≡ under n)) f x = decidability-of-prop-is-prop (fe 𝓤₀ 𝓤₀) (a x) \end{code} We now show that LPO is logically equivalent to its traditional formulation by Bishop. However, the traditional formulation is not a univalent proposition in general, and not type equivalent (in the sense of UF) to our formulation. \begin{code} LPO-gives-compact-ℕ : LPO → compact ℕ LPO-gives-compact-ℕ lpo β = cases a b d where A = (Σ n ꞉ ℕ , β n ≡ ₀) + (Π n ꞉ ℕ , β n ≡ ₁) α : ℕ → 𝟚 α = force-decreasing β x : ℕ∞ x = (α , force-decreasing-is-decreasing β) d : decidable(Σ n ꞉ ℕ , x ≡ under n) d = lpo x a : (Σ n ꞉ ℕ , x ≡ under n) → A a (n , p) = inl (force-decreasing-is-not-much-smaller β n c) where c : α n ≡ ₀ c = ap (λ - → incl - n) p ∙ under-diagonal₀ n b : (¬ (Σ n ꞉ ℕ , x ≡ under n)) → A b u = inr g where v : (n : ℕ) → x ≡ under n → 𝟘 v = curry u g : (n : ℕ) → β n ≡ ₁ g n = force-decreasing-is-smaller β n e where c : x ≡ under n → 𝟘 c = v n l : x ≡ ∞ l = not-finite-is-∞ (fe 𝓤₀ 𝓤₀) v e : α n ≡ ₁ e = ap (λ - → incl - n) l compact-ℕ-gives-LPO : compact ℕ → LPO compact-ℕ-gives-LPO chlpo x = cases a b d where A = decidable (Σ n ꞉ ℕ , x ≡ under n) β : ℕ → 𝟚 β = incl x d : (Σ n ꞉ ℕ , β n ≡ ₀) + (Π n ꞉ ℕ , β n ≡ ₁) d = chlpo β a : (Σ n ꞉ ℕ , β n ≡ ₀) → A a (n , p) = inl (pr₁ g , pr₂(pr₂ g)) where g : Σ m ꞉ ℕ , (m ≤ n) × (x ≡ under m) g = under-lemma (fe 𝓤₀ 𝓤₀) x n p b : (Π n ꞉ ℕ , β n ≡ ₁) → A b φ = inr g where ψ : ¬ (Σ n ꞉ ℕ , β n ≡ ₀) ψ = uncurry (λ n → equal-₁-different-from-₀(φ n)) f : (Σ n ꞉ ℕ , x ≡ under n) → Σ n ꞉ ℕ , β n ≡ ₀ f (n , p) = (n , (ap (λ - → incl - n) p ∙ under-diagonal₀ n)) where l : incl x n ≡ incl (under n) n l = ap (λ - → incl - n) p g : ¬ (Σ n ꞉ ℕ , x ≡ under n) g = contrapositive f ψ \end{code} Now, if LPO is false, that is, an empty type, then the function type LPO → ℕ is isomorphic to the unit type 𝟙, and hence is compact. If LPO holds, that is, LPO is equivalent to 𝟙 because it is a univalent proposition, then the function type LPO → ℕ is isomorphic to ℕ, and hence the type LPO → ℕ is again compact by LPO. So in any case we have that the type LPO → ℕ is compact. However, LPO is an undecided proposition in our type theory, so that the nature of the function type LPO → ℕ is undecided. Nevertheless, we can show that it is compact, without knowing whether LPO holds or not! \begin{code} open import PropTychonoff [LPO→ℕ]-compact∙ : compact∙ (LPO → ℕ) [LPO→ℕ]-compact∙ = prop-tychonoff-corollary' fe LPO-is-prop f where f : LPO → compact∙ ℕ f lpo = compact-pointed-gives-compact∙ (LPO-gives-compact-ℕ lpo) 0 [LPO→ℕ]-compact : compact (LPO → ℕ) [LPO→ℕ]-compact = compact∙-gives-compact [LPO→ℕ]-compact∙ [LPO→ℕ]-Compact : Compact (LPO → ℕ) {𝓤} [LPO→ℕ]-Compact = compact-gives-Compact (LPO → ℕ) [LPO→ℕ]-compact \end{code} However, we cannot prove that the function type LPO→ℕ is discrete, as otherwise we would be able to decide the negation of LPO (added 14th Feb 2020): \begin{code} open import DiscreteAndSeparated open import NaturalNumbers-Properties [LPO→ℕ]-discrete-gives-¬LPO-decidable : is-discrete (LPO → ℕ) → decidable (¬ LPO) [LPO→ℕ]-discrete-gives-¬LPO-decidable = discrete-exponential-has-decidable-emptiness-of-exponent (fe 𝓤₀ 𝓤₀) (1 , 0 , positive-not-zero 0) \end{code} Another condition equivalent to LPO is that the obvious embedding under𝟙 : ℕ + 𝟙 → ℕ∞ has a section: \begin{code} has-section-under𝟙-gives-LPO : (Σ s ꞉ (ℕ∞ → ℕ + 𝟙) , under𝟙 ∘ s ∼ id) → LPO has-section-under𝟙-gives-LPO (s , ε) u = ψ (s u) refl where ψ : (z : ℕ + 𝟙) → s u ≡ z → decidable(Σ n ꞉ ℕ , u ≡ under n) ψ (inl n) p = inl (n , (u ≡⟨ (ε u) ⁻¹ ⟩ under𝟙 (s u) ≡⟨ ap under𝟙 p ⟩ under n ∎)) ψ (inr *) p = inr γ where γ : ¬ (Σ n ꞉ ℕ , u ≡ under n) γ (n , q) = ∞-is-not-finite n (∞ ≡⟨ (ap under𝟙 p)⁻¹ ⟩ under𝟙 (s u) ≡⟨ ε u ⟩ u ≡⟨ q ⟩ under n ∎) under𝟙-inverse : (u : ℕ∞) → decidable (Σ n ꞉ ℕ , u ≡ under n) → ℕ + 𝟙 {𝓤₀} under𝟙-inverse .(under n) (inl (n , refl)) = inl n under𝟙-inverse u (inr g) = inr * LPO-gives-has-section-under𝟙 : LPO → Σ s ꞉ (ℕ∞ → ℕ + 𝟙) , under𝟙 ∘ s ∼ id LPO-gives-has-section-under𝟙 lpo = s , ε where s : ℕ∞ → ℕ + 𝟙 s u = under𝟙-inverse u (lpo u) φ : (u : ℕ∞) (d : decidable (Σ n ꞉ ℕ , u ≡ under n)) → under𝟙 (under𝟙-inverse u d) ≡ u φ .(under n) (inl (n , refl)) = refl φ u (inr g) = (not-finite-is-∞ (fe 𝓤₀ 𝓤₀) (curry g))⁻¹ ε : under𝟙 ∘ s ∼ id ε u = φ u (lpo u) \end{code}