Martin Escardo 29 April 2014.

An hprop-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 hpropositions, 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 an hproposition X amounts to X=0 or X=1, so
that

Y^X is searchable if Y is searchable and X is an hproposition.

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 an hproposition 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 #-}

module HProp-Tychonoff where

open import Searchable
open import HSets
open import HProp-indexed-product
open import Equality
open import Two
open import SetsAndFunctions
open import CurryHoward
open import Isomorphism

\end{code}

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

A crucial lemma is

hprop-indexed-product : hprop X → (a : X) → Z ≅ Y a

This is proved in the module HProp-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}

hprop-tychonoff : {X : Set} {Y : X → Set} → hprop X
→ ((x : X) → searchable(Y x)) → searchable((x : X) → Y x)
hprop-tychonoff {X} {Y} hp ε p = z₀ , z₀-is-universal-witness
where
-- hp : hprop X
--  ε : (x : X) → searchable(Y x)
--  p : Z → ₂

Z = (x : X) → Y x

hip : (x : X) → Z ≅ Y x
hip = hprop-indexed-product hp

-- The essence of the first part of the proof is this:
not-useful : X → searchable Z
not-useful x = iso-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 hprop-indexed-product, abstractly:
f : (x : X) → Z → Y x
f x = π₀(hip x)

g : (x : X) → Y x → Z
g x = π₀(π₁(hip x))

fg : (x : X) (y : Y x) → f x (g x y) ≡ y -- Not used.
fg x = π₀(π₁(π₁(hip x)))

gf : (x : X) (z : Z) → g x (f x z) ≡ z   -- Crucially used.
gf x = π₁(π₁(π₁(hip 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(g 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 = π₀(ε x (q x))

-- By hypothesis, it satisfies:
z₀-spec : (x : X) → q x (z₀ x) ≡ ₁ → (y : Y x) → q x y ≡ ₁
z₀-spec x = π₁(ε x (q x))

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

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

-- In particular, with y = f x z, we get:
z₀-spec₁-particular-case : (x : X) → p(g x (f x z₀)) ≡ ₁ → (z : Z) → p(g 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 (cong p (sym (gf x z))) (z₀-spec₁-particular-case x (trans (cong p (gf 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 (cong p claim) r
where
open import Extensionality
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 (an hprop) to X being subfinite (embedded into a finite
type).)

A particular case is the following:

\begin{code}

hprop-tychonoff-corollary : {X Y : Set} → hprop X
→ searchable Y → searchable(X → Y)
hprop-tychonoff-corollary hp ε = hprop-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}

hprop-tychonoff-corollary' : {X Y : Set} → hprop X
→ (X → searchable Y) → searchable(X → Y)
hprop-tychonoff-corollary' hp ε = hprop-tychonoff hp ε

\end{code}