Martin Escardo 29 April 2014.

A prop-indexed product of searchable sets is itself searchable. 

The definition of the searchability of a type A is

    searchable A = (p : A → ₂) → Σ \(a₀ : A) → p a₀ ≡ ₁ → (a : A) → p a ≡ ₁

With excluded middle for propositions, the above claim is not
surprising, because

    (0 → Y) = Y^0 = 1 (which is always searchable),
    (1 → Y) = Y^1 = Y (which is searchable if Y is),

and excluded middle for a proposition X amounts to X=0 or X=1, so
that 

    Y^X is searchable if Y is searchable 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 searchable if X is a proposition and Y x is
        searchable for every x:X.

        (This product is written (x : X) → Y x 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 #-} 

module Prop-Tychonoff where

open import SpartanMLTT
open import Two
open import Searchable
open import Sets
open import Prop-indexed-product
open import Equivalence

\end{code}

Let Z = ((x : X) → Y x).

A crucial lemma is 

    prop-indexed-product : isProp X → (a : X) → Z ≅ 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 Z
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 searchable set from the module
Searchable:

    searchable 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 : U} {Y : X  U}  isProp X 
                ((x : X)  searchable(Y x))  searchable((x : X)  Y x)
prop-tychonoff {X} {Y} hp ε p = z₀ , z₀-is-universal-witness 
 where
  -- hp : isProp X
  --  ε : (x : X) → searchable(Y x)
  --  p : Z → ₂

  Z = (x : X)  Y x

  hip : (x : X)  Z  Y x
  hip = prop-indexed-product hp

  -- The essence of the first part of the proof is this:
  not-useful : X  searchable Z
  not-useful x = equiv-searchable (≃-sym(hip x)) (ε x)
  -- 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:
  f : (x : X)  Z  Y x
  f x = pr₁(hip x)

  hrf : (x : X)  hasRetraction(f x)
  hrf x = pr₂(pr₂(hip x))

  h : (x : X)  Y x  Z
  h x = pr₁(hrf x)

  hf : (x : X) (z : Z)  h x (f x z)  z
  hf x = pr₂(hrf x)

  -- We define a predicate q x: Y x → ₂, for each x:X, from the
  -- predicate p:Z→₂ via (part of) the above isomorphism:
  q : (x : X)  Y x  𝟚
  q x y = p(h x y)

  -- We argue that the following is a universal witness for the
  -- searchability of the type Z wrt the predicate p:
  z₀ : Z
  z₀ x = pr₁(ε x (q x))

  -- By hypothesis, it satisfies: 
  z₀-spec : (x : X)  q x (z₀ x)    (y : Y x)  q x y  
  z₀-spec x = pr₂(ε x (q x)) 

  -- By expanding the definitions, this amounts to:
  z₀-spec₀ : (x : X)  p(h x (z₀ x))    (y : Y x)  p(h x y)  
  z₀-spec₀ = z₀-spec

  -- By the definition of f in prop-indexed-product (namely f x z = z x):
  z₀-spec₁ : (x : X)  p(h x (f x z₀))    (y : Y x)  p(h x y)  
  z₀-spec₁ = z₀-spec₀
  -- (So we can't abstract away the definition/proof of
  --  prop-indexed-product.)

  -- In particular, with y = f x z, we get:
  z₀-spec₁-particular-case : (x : X)  p(h x (f x z₀))    (z : Z)  p(h x (f x z))  
  z₀-spec₁-particular-case x r z = z₀-spec₁ x r (f x z)

  -- Using the fact that g x (f x z) = z for any x:X, we get:
  z₀-is-universal-witness-assuming-X : X  p z₀    (z : Z)  p z  
  z₀-is-universal-witness-assuming-X x r z = 
     trans (ap p (sym (hf x z))) (z₀-spec₁-particular-case x (trans (ap p (hf x z₀)) r) z)
  -- 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:
  z₀-is-universal-witness-assuming-X→∅ : (X  )  p z₀    (z : Z)  p z  
  z₀-is-universal-witness-assuming-X→∅ u r z = trans (ap p claim) r 
   where
    open import FunExt
    claim : z  z₀
    claim = funext x  unique-from-∅(u x))

  -- So we would get what we want if we had excluded middle, because
  -- the above shows that both X and X→∅ give the desired conclusion
  -- that z₀ is a universal witness. But excluded middle is not needed.

  -- We shuffle the arguments of z₀-is-universal-witness-assuming-X:
  claim₀ : p z₀    (z : Z)  X  p z  
  claim₀ r z x = z₀-is-universal-witness-assuming-X x r z

  -- We then take the contra-positive of the conclusion X → p z ≡ ₁,
  -- and use the fact that if a point of the two-point type 𝟚 is ₀,
  -- then it is not ₁:
  Claim₁ : p z₀    (z : Z)  p z    (X  )
  Claim₁ r z = contra-positive(claim₀ r z)  Lemma[b≡₀→b≢₁]
  -- This concludes the first part of the argument.

  -- We now shuffle the arguments of z₀-is-universal-witness-assuming-X→∅:
  Claim₂ : p z₀    (z : Z)  (X  )  p z  
  Claim₂ r z u = z₀-is-universal-witness-assuming-X→∅ u r z

  -- Combining the two last claims, we get:
  Claim₃ : p z₀    (z : Z)  p z    p z  
  Claim₃ r z = Claim₂ r z  Claim₁ r z

  -- Finally, we do case analysis on the value of p z:
  z₀-is-universal-witness : p z₀    (z : Z)  p z  
  z₀-is-universal-witness r z = two-equality-cases (Claim₃ r z) id

\end{code}

And we are done. (9 Sep 2015: We can generalize from X being a
subsingleton (a proposition) to X being subfinite (embedded into a
finite type).)


A particular case is the following:

\begin{code}

prop-tychonoff-corollary : {X Y : U}  isProp X 
                         searchable Y  searchable(X  Y)
prop-tychonoff-corollary hp ε = prop-tychonoff hp  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 1 or Y (or none,
if this is undecided)!

Better (9 Sep 2015):

\begin{code}

prop-tychonoff-corollary' : {X Y : U}  isProp X 
                           (X  searchable Y)  searchable(X  Y)
prop-tychonoff-corollary' hp ε = prop-tychonoff hp ε

\end{code}