Martin Escardo 2011.

We now iterate the proof of the fact that binary products preserve
compactness, to get that countable (dependent) products preserve
compactness. The first lemma passes with termination check enabled:

\begin{code}

{-# OPTIONS --without-K #-}
{-# OPTIONS --no-termination-check #-}

module CountableTychonoff where

open import Two
open import Naturals
open import CurryHoward
open import Searchable
open import Equality
open import Sequence

binary-Tychonoff' : {X :   Set}  

 searchable(X 0)   searchable((n : )  X(succ n))
  searchable((n : )  X n)

binary-Tychonoff' ε δ =
 retractions-preserve-searchability 
  cons-retraction 
 (binary-Tychonoff ε δ) 

\end{code}

It is the following that needs disabling of termination
checking. It terminates on the assumption that functions are
continuous, but doesn't use their moduli of continuity. Put another
way, we get an infinite proof, so to speak, but whenever it is
applied to compute a ground value, a finite portion of the proof is
used, because of continuity.

We emphasize that although continuity is used at the meta-level to
justify termination, the result is not anti-classical. In fact,
classically, all sets are searchable! This module just enlarges the
constructive universe a bit, using Brouwerian ideas, but being
compatible with Bishop in the sense of not contradicting classical
mathematics.

Because the proof of termination is not constructive, if you are a
strict constructivist you won't be convinced that this proof-program
always terminates (when used to define a value of ground
type). However, you will have a hard time exhibiting a
counter-example: the assumption existence of a non-continuous function
allows you to constructively prove LPO! (With the termination checker
enabled.) (I plan to actually write down this proof in Agda.)


\begin{code}

countable-Tychonoff : {X :   Set} 

 (∀ n  searchable(X n))  searchable((n : )  X n)

countable-Tychonoff {X} ε = 
 binary-Tychonoff' (hd ε) (countable-Tychonoff(tl ε))

\end{code}

A corollary is that the Cantor space is searchable, and hence omniscient
and exhaustible. See the module CantorSearchable.