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

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


{-# 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


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


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


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

A particular case is the following:


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


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


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