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 (or exhaustive searchability) is

    compactβˆ™ A = (p : A β†’ 𝟚) β†’ Ξ£ aβ‚€ κž‰ A , p aβ‚€ ＝ ₁ β†’ (a : A) β†’ p a ＝ ₁

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.)

Our Agda proof below can be written rather concisely by expanding the
definitions. We deliberately don't do that, so that we have a rigorous
informal proof side-by-side with the formal proof. We proceed in a
series of trivial steps, hopefully in the most natural way (although
we had a convoluted path to this supposedly natural way).

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

open import MLTT.Spartan

open import UF.FunExt

module TypeTopology.PropTychonoff (fe : FunExt) where

open import TypeTopology.CompactTypes
open import MLTT.Two-Properties
open import UF.Base
open import UF.Subsingletons
open import UF.PropIndexedPiSigma
open import UF.Equiv
open import UF.EquivalenceExamples

\end{code}

A crucial lemma is

    prop-indexed-product : is-prop X β†’ (a : X) β†’ Ξ  Y β‰… Y a

This is proved in the module Prop-indexed-product. Although it has a
subtle proof, it should be intuitively clear, as X has at most one
element by hypothesis, and if the element is a:X then the product Ξ  Y
should be isomorphic to its only factor Y a.

With this observation, the following proof should be self-contained,
if we recall again the definition of compact set from the module
CompacTypes:

    compactβˆ™ A = (p : A β†’ 𝟚) β†’ Ξ£ aβ‚€ κž‰ A , p aβ‚€ ＝ ₁ β†’ (a : A) β†’ p a ＝ ₁

Recall also that such an aβ‚€ is called a universal witness for the predicate p.

\begin{code}

prop-tychonoff : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ }
               β†’ is-prop X
               β†’ ((x : X) β†’ compactβˆ™ (Y x))
               β†’ compactβˆ™ (Ξ  Y)
prop-tychonoff {𝓀} {π“₯} {X} {Y} X-is-prop Ξ΅ p = Ξ³
 where
  have : (type-of Ξ΅ ＝ ((x : X) β†’ compactβˆ™(Y x)))
       Γ— (type-of p ＝ (Ξ  Y β†’ 𝟚))
  have = refl , refl

  hip : (x : X) β†’ Ξ  Y ≃ Y x
  hip = prop-indexed-product (fe 𝓀 π“₯) X-is-prop

\end{code}

The essence of the first part of the proof is this:

\begin{code}

  crude : X β†’ compactβˆ™ (Ξ  Y)
  crude x = equiv-compactβˆ™ (≃-sym(hip x)) (Ξ΅ x)

\end{code}

But this is very crude for our purposes (or so it seems).  So we
instead proceed as follows.

The following is what we get from prop-indexed-product, abstractly:

\begin{code}

  f : (x : X) β†’ Ξ  Y β†’ Y x
  f x = pr₁ (hip x)

  hrf : (x : X) β†’ Ξ£ r κž‰ (Y x β†’ Ξ  Y), r ∘ f x ∼ id
  hrf x = prβ‚‚ (prβ‚‚ (hip x))

  h : (x : X) β†’ Y x β†’ Ξ  Y
  h x = pr₁ (hrf x)

  hf : (x : X) (Ο† : Ξ  Y) β†’ h x (f x Ο†) ＝ Ο†
  hf x = prβ‚‚ (hrf x)

\end{code}

We define a predicate q x : Y x β†’ 𝟚, for each x : X, from the
predicate p : Ξ  Y β†’ 𝟚 via (part of) the above isomorphism:

\begin{code}

  q : (x : X) β†’ Y x β†’ 𝟚
  q x y = p (h x y)

\end{code}

We argue that the following is a universal witness for the
searchability of the type Ξ  Y wrt the predicate p:

\begin{code}

  Ο†β‚€ : Ξ  Y
  Ο†β‚€ x = pr₁ (Ξ΅ x (q x))

\end{code}

By hypothesis, it satisfies:

\begin{code}

  Ο†β‚€-spec : (x : X) β†’ q x (Ο†β‚€ x) ＝ ₁ β†’ (y : Y x) β†’ q x y ＝ ₁
  Ο†β‚€-spec x = prβ‚‚ (Ξ΅ x (q x))

\end{code}

By expanding the definitions, this amounts to:

\begin{code}

  Ο†β‚€-specβ‚€ : (x : X) β†’ p (h x (Ο†β‚€ x)) ＝ ₁ β†’ (y : Y x) β†’ p (h x y) ＝ ₁
  Ο†β‚€-specβ‚€ = Ο†β‚€-spec

\end{code}

By the definition of f in prop-indexed-product (namely f x Ο† = Ο† x):

\begin{code}

  Ο†β‚€-spec₁ : (x : X) β†’ p (h x (f x Ο†β‚€)) ＝ ₁ β†’ (y : Y x) β†’ p (h x y) ＝ ₁
  Ο†β‚€-spec₁ = Ο†β‚€-specβ‚€

\end{code}

(So we can't abstract away the definition/proof of
prop-indexed-product.)

In particular, with y = f x Ο†, we get:

\begin{code}

  Ο†β‚€-spec₁-particular-case : (x : X)
                           β†’ p (h x (f x Ο†β‚€)) ＝ ₁
                           β†’ (Ο† : Ξ  Y) β†’ p (h x (f x Ο†)) ＝ ₁
  Ο†β‚€-spec₁-particular-case x r Ο† = Ο†β‚€-spec₁ x r (f x Ο†)

\end{code}

Using the fact that g x (f x Ο†) = Ο† for any x:X, we get:

\begin{code}

  Ο†β‚€-is-universal-witness-assuming-X : X β†’ p Ο†β‚€ ＝ ₁ β†’ (Ο† : Ξ  Y) β†’ p Ο† ＝ ₁
  Ο†β‚€-is-universal-witness-assuming-X x r Ο† =
     p Ο†             ＝⟨ ap p ((hf x Ο†)⁻¹) ⟩
     p (h x (f x Ο†)) ＝⟨ Ο†β‚€-spec₁-particular-case x s Ο† ⟩
     ₁               ∎
   where
    s = p (h x (f x Ο†β‚€)) ＝⟨ ap p (hf 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β†’πŸ˜ : (X β†’ 𝟘) β†’ p Ο†β‚€ ＝ ₁ β†’ (Ο† : Ξ  Y) β†’ p Ο† ＝ ₁
  Ο†β‚€-is-universal-witness-assuming-Xβ†’πŸ˜ u r Ο† = p Ο†  ＝⟨ ap p claim ⟩
                                               p Ο†β‚€ ＝⟨ r ⟩
                                               ₁    ∎

   where
    claim : Ο† ＝ Ο†β‚€
    claim = dfunext (fe 𝓀 π“₯) (Ξ» x β†’ unique-from-𝟘 (u x))
\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β†’πŸ˜:

\begin{code}

  Claimβ‚‚ : p Ο†β‚€ ＝ ₁ β†’ (Ο† : Ξ  Y) β†’ (X β†’ 𝟘) β†’ p Ο† ＝ ₁
  Claimβ‚‚ r Ο† u = Ο†β‚€-is-universal-witness-assuming-Xβ†’πŸ˜ 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

  Ξ³ : Ξ£ Ο†β‚€ κž‰ Ξ  Y , (p Ο†β‚€ ＝ ₁ β†’ (Ο† : Ξ  Y) β†’ p Ο† ＝ ₁)
  Ξ³ = Ο†β‚€ , Ο†β‚€-is-universal-witness

\end{code}

And we are done.

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 : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                         β†’ is-prop X
                         β†’ compactβˆ™ Y
                         β†’ compactβˆ™ (X β†’ Y)
prop-tychonoff-corollary X-is-prop Ξ΅ = prop-tychonoff 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' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                          β†’ is-prop X
                          β†’ (X β†’ compactβˆ™ Y)
                          β†’ compactβˆ™ (X β†’ Y)
prop-tychonoff-corollary' = prop-tychonoff

\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.ExcludedMiddle

compact-prop-tychonoff-gives-WEM : ((X : 𝓀 Μ‡ ) (Y : X β†’ π“₯ Μ‡ )
                                       β†’ is-prop X
                                       β†’ ((x : X) β†’ compact (Y x))
                                       β†’ compact (Ξ  Y))
                                 β†’ WEM 𝓀
compact-prop-tychonoff-gives-WEM {𝓀} {π“₯} Ο„ X X-is-prop = Ξ΄ Ξ³
 where
  Y : X β†’ π“₯ Μ‡
  Y x = 𝟘

  negation-compact : compact (X β†’ 𝟘 {π“₯})
  negation-compact = Ο„ X Y X-is-prop (Ξ» p β†’ 𝟘-compact)

  Ξ³ : decidable (X β†’ 𝟘 {π“₯})
  Ξ³ = compact-decidable (X β†’ 𝟘) negation-compact

  Ξ΄ : decidable (X β†’ 𝟘 {π“₯}) β†’ decidable (Β¬ X)
  δ (inl f) = inl (𝟘-elim ∘ f)
  Ξ΄ (inr Ο•) = inr (contrapositive (Ξ» f β†’ 𝟘-elim ∘ f) Ο•)

\end{code}