Martin Escardo 2011.

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

\begin{code}

{-# OPTIONS --without-K #-}

module CantorSearchable where

open import Cantor
open import Two
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 Exhaustible
open import CurryHoward
open import Equality

A : (₂ℕ  )  
A = ∃-witness(exhaustible-implies-exhaustible' cantor-exhaustible)

\end{code}

Discreteness of (₂ℕ → ℕ):

\begin{code}

open import DiscreteAndSeparated
open import Naturals

discrete-₂ℕ→ℕ : discrete(₂ℕ  )

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

\end{code}

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

\begin{code}

open import DecidableAndDetachable
open import Equality

equal : (₂ℕ  )  (₂ℕ  )  

equal f  = ∃-witness(characteristic-function(discrete-₂ℕ→ℕ 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}