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

open import SpartanMLTT
open import Two
open import UF-FunExt

module CantorSearchable (fe : βˆ€ U V β†’ funext U V) where

open import SearchableTypes
open import CountableTychonoff (fe)
open import OmniscientTypes
open import ExhaustibleTypes

cantor-searchable : searchable (β„• β†’ 𝟚)
cantor-searchable = countable-Tychonoff (Ξ» i β†’ 𝟚-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 ExhaustibleTypes

A : ((β„• β†’ 𝟚) β†’ 𝟚) β†’ 𝟚
A = pr₁(exhaustible-implies-exhaustible' cantor-exhaustible)

\end{code}

Discreteness of ((β„• β†’ 𝟚) β†’ β„•):

\begin{code}

open import DiscreteAndSeparated

discrete-Cantorβ†’β„• : discrete((β„• β†’ 𝟚) β†’ β„•)
discrete-Cantor→ℕ = omniscient-discrete-discrete' (fe U₀ U₀) 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}

number : 𝟚 β†’ β„•
number β‚€ = 0
number ₁ = 1

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}