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}