Chuangjie Xu 2012

This corresponds to part of Section 2 of the paper
http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf

\begin{code}

module Space-cantor where

open import MiniLibrary
open import Sequence
open import Inequality
open import UniformContinuity
open import Space
open import Space-discrete
open import Space-exponential
open import not-not

\end{code}

The Cantor space ₂ℕ with the monoid C form a C-space, which
is isomorphic to the exponential ℕSpace ⇒ ₂Space.

\begin{code}

Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] : (r : ₂ℕ → ₂ℕ) → r ∈ C →
     ∃ \(φ : ₂ℕ → U (ℕSpace ⇒ ₂Space)) → φ ∈ Probe (ℕSpace ⇒ ₂Space)
Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] r ucr = ∃-intro φ prf
 where
  φ : ₂ℕ → U (ℕSpace ⇒ ₂Space)
  φ α = r α , Lemma[discrete-ℕSpace] {₂Space} (r α)
  prf : ∀(p : ₂ℕ → ℕ) → p ∈ LC → ∀(t : ₂ℕ → ₂ℕ) → t ∈ C →
         (λ α → (π₀ ∘ φ)(t α)(p α)) ∈ LC
  prf p ucp t uct = Lemma[LM-₂-least-modulus] q l pr
   where
    q : ₂ℕ → ₂
    q α = (π₀ ∘ φ)(t α)(p α)
    m : ℕ
    m = ∃-witness ucp
    f : ₂Fin m → ℕ
    f s = p (cons s 0̄)
    eq : ∀(α : ₂ℕ) → p α ≡ f (take m α)
    eq α = ∧-elim₀ (∃-elim ucp) α (cons (take m α) 0̄) (Lemma[cons-take-≣[]] m α 0̄)
    k' : ℕ
    k' = ∃-witness (max-fin f)
    k'-max : ∀(α : ₂ℕ) → p α ≤ k'
    k'-max α = transport {ℕ} {λ i → i ≤ k'} (sym (eq α)) (∃-elim (max-fin f) (take m α))
    k : ℕ
    k = succ k'
    k-max : ∀(α : ₂ℕ) → p α < k
    k-max α = ≤-succ (k'-max α)
    ucrt : uniformly-continuous-₂ℕ (r ∘ t)
    ucrt = Lemma[∘-UC] r ucr t uct
    n : ℕ
    n = ∃-witness (ucrt k)
    l : ℕ
    l = maximum m n
    m≤l : m ≤ l
    m≤l = ∧-elim₀ (Lemma[≤-max] m n)
    n≤l : n ≤ l
    n≤l = ∧-elim₁ (Lemma[≤-max] m n)
    pr : ∀(α β : ₂ℕ) → α ≣[ l ] β → r(t α)(p α) ≡ r(t β)(p β)
    pr α β awl = transport {ℕ} {λ i → r(t α)(p α) ≡ r(t β) i} eqp subgoal
     where
      awm : α ≣[ m ] β
      awm = Lemma[≣[]-≤] awl m≤l
      eqp : p α ≡ p β
      eqp = ∧-elim₀ (∃-elim ucp) α β awm
      awn : α ≣[ n ] β
      awn = Lemma[≣[]-≤] awl n≤l
      awk : r (t α) ≣[ k ] r (t β)
      awk = ∧-elim₀ (∃-elim (ucrt k)) α β awn
      subgoal : r(t α)(p α) ≡ r(t β)(p α)
      subgoal = Lemma[≣[]-<] awk (p α) (k-max α)

\end{code}

In particular, the identity map is also a probe.

\begin{code}

ID : ₂ℕ → U(ℕSpace ⇒ ₂Space)
ID = ∃-witness (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] id Lemma[id-UC])

Lemma[ID-[≡]] : ∀(α : U (ℕSpace ⇒ ₂Space)) → [ α ≡ ID (π₀ α) ]
Lemma[ID-[≡]] α = Lemma[Map-₂] ℕSpace α (ID (π₀ α)) (λ n → refl)

ID-is-a-probe : ID ∈ Probe(ℕSpace ⇒ ₂Space)
ID-is-a-probe = ∃-elim (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] id Lemma[id-UC])

\end{code}

As the underlining category C contains only one object, the
Yoneda lemma equivalently says that the set of continuous maps
from the Yoneda embedding to any C-space is isomorphic to the
C-topology of that space.

\begin{code}

Lemma[Yoneda] : ∀{X : Space} → Map (ℕSpace ⇒ ₂Space) X →
                 ∃ \(p : ₂ℕ → U X) → p ∈ Probe X
Lemma[Yoneda] (f , cts) = (f ∘ ID) , (cts ID ID-is-a-probe)

\end{code}