Martin Escardo 29 April 2014.
A proposition-indexed product of pointed compact sets is itself
compact. But the assumption that a proposition-indexed product of
compact sets is compact gives weak excluded middle (negative
propositions are decidable).
The definition of compactness-pointedness (or exhaustive
searchability) is
compact∙ X = (p : X → 𝟚) → Σ x₀ ꞉ X , p x₀ ＝ ₁ → (x : X) → p x ＝ ₁
We refer to such an x₀ as a universal witness.
With excluded middle for propositions, the above claim is not
surprising, because
(𝟘 → Y) = Y^𝟘 ≃ 𝟙 (which is always compact),
(𝟙 → Y) = Y^𝟙 ≃ Y (which is compact if Y is),
and excluded middle for a proposition X amounts to X = 𝟘 or X = 𝟙, so
that
Y^X is compact∙ if Y is compact∙ and X is a proposition.
The point is that
(1) We can reach this conclusion without excluded middle.
(2) This also holds for dependent products:
Π x : X , Y x is compact∙ if X is a proposition and Y x is
compact∙ for every x : X.
(This product is also written (x : X) → Y x or Π Y in Agda.)
\begin{code}
{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
module TypeTopology.PropTychonoff where
open import MLTT.Two-Properties
open import TypeTopology.CompactTypes
open import UF.Equiv
open import UF.FunExt
open import UF.PropIndexedPiSigma
open import UF.Subsingletons
prop-tychonoff : funext 𝓤 𝓥
→ {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ is-prop X
→ ((x : X) → is-compact∙ (Y x))
→ is-compact∙ (Π Y)
prop-tychonoff {𝓤} {𝓥} fe {X} {Y} X-is-prop ε p = γ
where
have-ε : (x : X) → is-compact∙ (Y x)
have-ε = ε
have-p : Π Y → 𝟚
have-p = p
𝕗 : (x : X) → Π Y ≃ Y x
𝕗 = prop-indexed-product fe X-is-prop
\end{code}
The essence of the first part of the proof is this:
\begin{code}
crude : X → is-compact∙ (Π Y)
crude x = compact∙-types-are-closed-under-equiv (≃-sym (𝕗 x)) (ε x)
\end{code}
But this is very crude for our purposes (or so it seems). So we
instead proceed as follows. We first introduct some abbreviations.
\begin{code}
f : (x : X) → Π Y → Y x
f x = ⌜ 𝕗 x ⌝
f-explicitly : (x : X) (φ : Π Y) → f x φ ＝ φ x
f-explicitly x φ = refl
f⁻¹ : (x : X) → Y x → Π Y
f⁻¹ x = ⌜ 𝕗 x ⌝⁻¹
\end{code}
We define a predicate q x : Y x → 𝟚, for each x : X, from the
predicate p : Π Y → 𝟚 via the above equivalence:
\begin{code}
q : (x : X) → Y x → 𝟚
q x y = p (f⁻¹ x y)
\end{code}
We argue that the following is a universal witness for the
searchability of the type Π Y w.r.t. the predicate p:
\begin{code}
φ₀ : Π Y
φ₀ x = universal-witness (ε x) (q x)
\end{code}
By hypothesis, it satisfies:
\begin{code}
φ₀-universality : (x : X) → q x (φ₀ x) ＝ ₁ → (y : Y x) → q x y ＝ ₁
φ₀-universality x = witness-universality (ε x) (q x)
\end{code}
By expanding the definitions, this amounts to:
\begin{code}
φ₀-universality₀ : (x : X) → p (f⁻¹ x (φ₀ x)) ＝ ₁ → (y : Y x) → p (f⁻¹ x y) ＝ ₁
φ₀-universality₀ = φ₀-universality
\end{code}
Because f x φ = φ x, the above amounts to the following:
\begin{code}
φ₀-universality₁ : (x : X) → p (f⁻¹ x (f x φ₀)) ＝ ₁ → (y : Y x) → p (f⁻¹ x y) ＝ ₁
φ₀-universality₁ = φ₀-universality₀
\end{code}
In particular, choosing y = f x φ, we get:
\begin{code}
φ₀-universality₁-particular-case : (x : X)
→ p (f⁻¹ x (f x φ₀)) ＝ ₁
→ (φ : Π Y) → p (f⁻¹ x (f x φ)) ＝ ₁
φ₀-universality₁-particular-case x r φ = φ₀-universality₁ x r (f x φ)
\end{code}
This in turn gives
\begin{code}
φ₀-is-universal-witness-assuming-X
: X → p φ₀ ＝ ₁ → (φ : Π Y) → p φ ＝ ₁
φ₀-is-universal-witness-assuming-X x r φ =
p φ ＝⟨ ap p ((inverses-are-retractions' (𝕗 x) φ)⁻¹) ⟩
p (f⁻¹ x (f x φ)) ＝⟨ φ₀-universality₁-particular-case x s φ ⟩
₁ ∎
where
s = p (f⁻¹ x (f x φ₀)) ＝⟨ ap p (inverses-are-retractions' (𝕗 x) φ₀) ⟩
p φ₀ ＝⟨ r ⟩
₁ ∎
\end{code}
Notice that the point x : X vanishes from the conclusion, and so we
are able to omit it from the hypothesis, which is crucial for what
follows.
We get the same conclusion if X is empty:
\begin{code}
φ₀-is-universal-witness-assuming-X-empty
: (X → 𝟘) → p φ₀ ＝ ₁ → (φ : Π Y) → p φ ＝ ₁
φ₀-is-universal-witness-assuming-X-empty u r φ =
p φ ＝⟨ ap p (dfunext fe (λ x → unique-from-𝟘 (u x))) ⟩
p φ₀ ＝⟨ r ⟩
₁ ∎
\end{code}
So we would get what we want if we had excluded middle, because X is a
proposition and the above shows that both X and X → 𝟘 give the desired
conclusion that φ₀ is a universal witness. But excluded middle is not
needed.
We shuffle the arguments of φ₀-is-universal-witness-assuming-X:
\begin{code}
claim₀ : p φ₀ ＝ ₁ → (φ : Π Y) → X → p φ ＝ ₁
claim₀ r φ x = φ₀-is-universal-witness-assuming-X x r φ
\end{code}
We then take the contrapositive of the conclusion X → p φ ＝ ₁, and
use the fact that if a point of the two-point type 𝟚 is ₀, then it is
not ₁:
\begin{code}
Claim₁ : p φ₀ ＝ ₁ → (φ : Π Y) → p φ ＝ ₀ → (X → 𝟘)
Claim₁ r φ = contrapositive (claim₀ r φ) ∘ equal-₀-different-from-₁
\end{code}
This concludes the first part of the argument.
We now shuffle the arguments of φ₀-is-universal-witness-assuming-X-empty:
\begin{code}
Claim₂ : p φ₀ ＝ ₁ → (φ : Π Y) → (X → 𝟘) → p φ ＝ ₁
Claim₂ r φ u = φ₀-is-universal-witness-assuming-X-empty u r φ
\end{code}
Combining the two last claims, we get:
\begin{code}
Claim₃ : p φ₀ ＝ ₁ → (φ : Π Y) → p φ ＝ ₀ → p φ ＝ ₁
Claim₃ r φ = Claim₂ r φ ∘ Claim₁ r φ
\end{code}
Finally, we do case analysis on the value of p φ:
\begin{code}
φ₀-is-universal-witness : p φ₀ ＝ ₁ → (φ : Π Y) → p φ ＝ ₁
φ₀-is-universal-witness r φ = 𝟚-equality-cases (Claim₃ r φ) id
\end{code}
And we are done:
\begin{code}
γ : Σ φ₀ ꞉ Π Y , (p φ₀ ＝ ₁ → (φ : Π Y) → p φ ＝ ₁)
γ = φ₀ , φ₀-is-universal-witness
\end{code}
TODO. 9 Sep 2015. We can generalize from X being a subsingleton (or
proposition) to X being subfinite (embedded into a finite type).
A particular case is the following:
\begin{code}
prop-tychonoff-corollary : funext 𝓤 𝓥
→ {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ is-prop X
→ is-compact∙ Y
→ is-compact∙ (X → Y)
prop-tychonoff-corollary fe X-is-prop ε = prop-tychonoff fe X-is-prop (λ x → ε)
\end{code}
This holds even for undecided X (such as X = LPO), or when we have no
idea whether X or (X → 𝟘), and hence whether (X → Y) is 𝟙 or Y (or
none, if this is undecided)!
Better (9 Sep 2015):
\begin{code}
prop-tychonoff-corollary' : funext 𝓤 𝓥
→ {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ is-prop X
→ (X → is-compact∙ Y)
→ is-compact∙ (X → Y)
prop-tychonoff-corollary' fe = prop-tychonoff fe
\end{code}
So the function type (LPO → ℕ) is compact! (See the module LPO for a
proof.)
The Tychonoff theorem for prop-indexed products of compact types
doesn't hold. To see this, first notice that a proposition is
compact iff it is decidable. Now, the empty type 𝟘 is compact
(but not compact∙), and if 𝟘^P, that is, ¬P, where compact for a
proposition P, this would imply that ¬P is decidable for every
proposition P, which is weak excluded middle, which is not provable.
\begin{code}
open import UF.ClassicalLogic
compact-prop-tychonoff-gives-WEM' : ((X : 𝓤 ̇ ) (Y : X → 𝓥 ̇ )
→ is-prop X
→ ((x : X) → is-compact (Y x))
→ is-compact (Π Y))
→ WEM' 𝓤
compact-prop-tychonoff-gives-WEM' {𝓤} {𝓥} τ X X-is-prop = δ γ
where
Y : X → 𝓥 ̇
Y x = 𝟘
negation-compact : is-compact (X → 𝟘 {𝓥})
negation-compact = τ X Y X-is-prop (λ p → 𝟘-compact)
γ : is-decidable (X → 𝟘 {𝓥})
γ = compact-types-are-decidable (X → 𝟘) negation-compact
δ : is-decidable (X → 𝟘 {𝓥}) → is-decidable (¬ X)
δ (inl f) = inl (𝟘-elim ∘ f)
δ (inr ϕ) = inr (contrapositive (λ f → 𝟘-elim ∘ f) ϕ)
\end{code}
If we further assume function extensionality, we get WEM from WEM',
and hence we can replace the conclusion of the above fact by WEM.