Martin Escardo 2011.

The Cantor space is the type (ℕ → 𝟚). We show it is searchable, under
the assumptions discussed in CountableTychonoff.

This module is a set of corollaries of the module CountableTychonoff
and other modules.

\begin{code}

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

module CantorSearchable where

open import Two
open import Naturals
open import Searchable
open import CountableTychonoff
open import Omniscience
open import Exhaustible

cantor-searchable : searchable (  𝟚)
cantor-searchable = countable-Tychonoff  i  two-searchable)

cantor-omniscient : omniscient (  𝟚)
cantor-omniscient = searchable-implies-omniscient cantor-searchable

cantor-exhaustible : exhaustible (  𝟚)
cantor-exhaustible = searchable-implies-exhaustible cantor-searchable

\end{code}

The characteristic function of the universal quantifier
of the Cantor space:

\begin{code}

open import SpartanMLTT
open import Exhaustible

A : ((  𝟚)  𝟚)  𝟚
A = pr₁(exhaustible-implies-exhaustible' cantor-exhaustible)

\end{code}

Discreteness of ((ℕ → 𝟚) → ℕ):

\begin{code}

open import DiscreteAndSeparated
open import Naturals

discrete-Cantor→ℕ : discrete((  𝟚)  )

discrete-Cantor→ℕ = omniscient-discrete-discrete' cantor-omniscient ℕ-discrete

\end{code}

The characteristic function of equality on ((ℕ → 𝟚) → ℕ):

\begin{code}

open import DecidableAndDetachable

equal : ((  𝟚)  )  ((  𝟚)  )  𝟚

equal f  = pr₁(characteristic-function(discrete-Cantor→ℕ f))

\end{code}

Experiments: Evaluate the following to normal form (give ₀, ₁, ₁, ₀ quickly):

\begin{code}

test0 : 𝟚
test0 = A α  min𝟚(α 17)(α 180))

test1 : 𝟚
test1 = A α  )

test2 : 𝟚
test2 = equal  α  number(α 17))  α  number(α 100))

test3 : 𝟚
test3 = equal  α  number(α 100))  α  number(α 100))

test4 : 𝟚
test4 = equal  α  number(α 1000))  α  number(α 1000))

test5 : 𝟚
test5 = equal  α  number(α 1001))  α  number(α 1000))

\end{code}