Martin Escardo, 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 where

open import MiniLibrary
open import Sequence
open import Inequality
open import UniformContinuity
open import not-not
open import not-not-funext

\end{code}

The site we are working with is the monoid of uniformly continuous
endo-functions of the Cantor space with a coverage in which, for each
natural number n, there is a family of concatenation maps "cons s"
indexed by finite binary sequence s of length n.

The monoid of uniformly continuous ₂ℕ → ₂ℕ:

\begin{code}

C : Subset(₂ℕ → ₂ℕ)
C = uniformly-continuous-₂ℕ

\end{code}

The coverage axiom amounts to uniform continuity of endo-functions of
the Cantor space in the following sense.

\begin{code}

Axiom[coverage] : ∀(m : ℕ) → ∀(t : ₂ℕ → ₂ℕ) → t ∈ C →
                   ∃ \(n : ℕ) → ∀(s : ₂Fin n) →
                    ∃ \(s' : ₂Fin m) → ∃ \(t' : ₂ℕ → ₂ℕ) →
                     (t' ∈ C) ∧ [ t ∘ (cons s) ≡ (cons s') ∘ t' ]
Axiom[coverage] m t uct = ∃-intro n prf
 where
  n : ℕ
  n = ∃-witness (uct m)
  prf : ∀(s : ₂Fin n) → ∃ \(s' : ₂Fin m) → ∃ \(t' : ₂ℕ → ₂ℕ) →
         (t' ∈ C) ∧ [ t ∘ (cons s) ≡ (cons s') ∘ t' ]
  prf s = ∃-intro s' (∃-intro t' (∧-intro c₀ c₁))
   where
    s' : ₂Fin m
    s' = take m (t (cons s (λ i → ₀)))
    t' : ₂ℕ → ₂ℕ
    t' α = drop m (t (cons s α))
    c₀ : t' ∈ C
    c₀ k = Lemma[LM-₂ℕ-least-modulus] t' l prt'
     where
      ucts : uniformly-continuous-₂ℕ (t ∘ (cons s))
      ucts = Lemma[∘-UC] t uct (cons s) (Lemma[cons-UC] s)
      l : ℕ
      l = ∃-witness (ucts (k + m))
      prts : ∀(α β : ₂ℕ) → α ≣[ l ] β → t (cons s α) ≣[ k + m ] t (cons s β)
      prts = ∧-elim₀ (∃-elim (ucts (k + m)))
      eq : ∀(α : ₂ℕ) → ∀(i : ℕ) → t' α i ≡ t (cons s α) (i + m)
      eq α i = Lemma[drop+] m (t (cons s α)) i
      claim₀ : ∀(α β : ₂ℕ) → α ≣[ l ] β → t (cons s α) ≣[ k + m ] t (cons s β) →
                ∀(i : ℕ) → i < k → t' α i ≡ t' β i
      claim₀ α β el ekm i i<k = transport {₂} {λ b → t' α i ≡ b} (sym(eq β i)) sclaim₂
       where
        sclaim₀ : ∀(i : ℕ) → i < (k + m) → t (cons s α) i ≡ t (cons s β) i
        sclaim₀ = Lemma[≣[]-<] ekm
        sclaim₁ : t (cons s α) (i + m) ≡ t (cons s β) (i + m)
        sclaim₁ = sclaim₀ (i + m) (Lemma[a<b→a+c<b+c] i k m i<k)
        sclaim₂ : t' α i ≡ t (cons s β) (i + m)
        sclaim₂ = transport {₂} {λ b → b ≡ t (cons s β) (i + m)} (sym(eq α i)) sclaim₁
      claim₁ : ∀(α β : ₂ℕ) → α ≣[ l ] β → t (cons s α) ≣[ k + m ] t (cons s β) → t' α ≣[ k ] t' β
      claim₁ α β el ekm = Lemma[<-≣[]] (claim₀ α β el ekm)
      prt' : ∀(α β : ₂ℕ) → α ≣[ l ] β → t' α ≣[ k ] t' β
      prt' α β el = claim₁ α β el (prts α β el)
    c₁ : [ t ∘ (cons s) ≡ (cons s') ∘ t' ]
    c₁ = funext² claim
         -------
     where
      claim : ∀(α : ₂ℕ) → ∀(i : ℕ) → t (cons s α) i ≡ cons s' (t' α) i
      claim α i = transport {₂Fin m} {λ x → t (cons s α) i ≡ cons x (t' α) i} sclaim₂ sclaim₀
       where
        sclaim₀ : t (cons s α) i ≡ cons (take m (t (cons s α))) (t' α) i
        sclaim₀ = sym (Lemma[cons-take-drop] m (t (cons s α)) i)
        sclaim₁ : t (cons s α) ≣[ m ] t (cons s 0̄)
        sclaim₁ = ∧-elim₀ (∃-elim (uct m)) (cons s α) (cons s 0̄) (Lemma[cons-≣[]] s α 0̄)
        sclaim₂ : take m (t (cons s α)) ≡ s'
        sclaim₂ = Lemma[≣[]-take] sclaim₁

\end{code}

Instead of working with whole category of sheaves over the above site,
we consider only those concrete sheaves which amount to the following
C-spaces. To topologize a set X, we use functions ₂ℕ → X, called
probes, rather than subsets of X, called open. Thus a topology on a
set X, in our sense, is a set of maps ₂ℕ → X, called the probes,
satisfying some conditions. We call it the C-topology.

\begin{code}

probe-axioms : (X : Set) → Subset(₂ℕ → X) → Set
probe-axioms X P =
    (∀(p : ₂ℕ → X) → constant p → p ∈ P)
  ∧ (∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → X) → p ∈ P → p ∘ t ∈ P)
  ∧ (∀(p : ₂ℕ → X) → (∃ \(n : ℕ) → ∀(s : ₂Fin n) → (p ∘ (cons s)) ∈ P) → p ∈ P)
  ∧ (∀(p p' : ₂ℕ → X) → p ∈ P → (∀(α : ₂ℕ) → [ p α ≡ p' α ]) → p' ∈ P)

TopologyOn : Set → Set₁
TopologyOn X = Σ \(P : Subset(₂ℕ → X)) → probe-axioms X P

Space : Set₁
Space = Σ \(X : Set) → TopologyOn X

U : Space → Set
U = π₀

Probe : (X : Space) → Subset(₂ℕ → U X)
Probe X = π₀ (π₁ X)

cond₀ : (X : Space) →
        ∀(p : ₂ℕ → U X) → constant p → p ∈ Probe X
cond₀ (_ , _ , c₀ , _) = c₀

cond₁ : (X : Space) →
        ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → U X) → p ∈ Probe X →
        p ∘ t ∈ Probe X
cond₁ (_ , _ , _ , c₁ , _) = c₁

cond₂ : (X : Space) →
        ∀(p : ₂ℕ → U X) → (∃ \(n : ℕ) → ∀(s : ₂Fin n) → p ∘ (cons s) ∈ Probe X) →
        p ∈ Probe X
cond₂ (_ , _ , _ , _ , c₂ , _) = c₂

cond₃ : (X : Space) →
        ∀(p p' : ₂ℕ → U X) → p ∈ Probe X → (∀(α : ₂ℕ) → [ p α ≡ p' α ]) → p' ∈ Probe X
cond₃ (_ , _ , _ , _ , _ , c₃) = c₃


\end{code}

Then we define continuous functions between spaces and show that they
do form a category.

\begin{code}

continuous : {X Y : Space} → (U X → U Y) → Set
continuous {X} {Y} f = ∀ p → p ∈ Probe X → f ∘ p ∈ Probe Y

Map : Space → Space → Set
Map X Y = Σ \(f : U X → U Y) → continuous {X} {Y} f

Mapto : (Y : Space) → Set₁
Mapto Y = Σ \(X : Space) → Map X Y

id-is-continuous : ∀{X : Space} → continuous {X} {X} id
id-is-continuous p pinP = pinP

∘-preserves-continuity : {X Y Z : Space} →
    ∀(f : U X → U Y) → continuous {X} {Y} f →
    ∀(g : U Y → U Z) → continuous {Y} {Z} g →
    continuous {X} {Z} (g ∘ f)
∘-preserves-continuity f fcts g gcts p pinP = gcts(f ∘ p)(fcts p pinP)

⟪_,_,_⟫_○_ : (X Y Z : Space) → Map Y Z → Map X Y → Map X Z
⟪ X , Y , Z ⟫ g ○ f = (π₀ g ∘ π₀ f) , ∘-preserves-continuity {X} {Y} {Z} (π₀ f) (π₁ f) (π₀ g) (π₁ g)


Subspace : (X : Space) → (U X → Set) → Space
Subspace X Prp = A , R , rc₀ , rc₁ , rc₂ , rc₃
 where
  A : Set
  A = Σ \(x : U X) → Prp x
  R : Subset (₂ℕ → A)
  R r = π₀ ∘ r ∈ Probe X
  rc₀ : ∀(r : ₂ℕ → A) → constant r → r ∈ R
  rc₀ r cr = cond₀ X (π₀ ∘ r) (Lemma[∘-constant] r π₀ cr)
  rc₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(r : ₂ℕ → A) → r ∈ R → r ∘ t ∈ R
  rc₁ t uc r rR = cond₁ X t uc (π₀ ∘ r) rR
  rc₂ : ∀(r : ₂ℕ → A) → (∃ \(n : ℕ) → ∀(s : ₂Fin n) → (r ∘ (cons s)) ∈ R) → r ∈ R
  rc₂ r pr = cond₂ X (π₀ ∘ r) pr
  rc₃ : ∀(r r' : ₂ℕ → A) → r ∈ R → (∀(α : ₂ℕ) → [ r α ≡ r' α ]) → r' ∈ R
  rc₃ r r' rR ex = cond₃ X (π₀ ∘ r) (π₀ ∘ r') rR (λ α → [ap] π₀ (ex α))

cts-incl : (X : Space) → (Prp : U X → Set) → Map (Subspace X Prp) X
cts-incl X Prp = π₀ , (λ r rR → rR)

\end{code}

Initial C-space.
The C-topology is empty.

\begin{code}

∅Space : Space
∅Space = ∅ , P , c₀ , c₁ , c₂ , c₃
 where
  P : Subset (₂ℕ → ∅)
  P p = ∅
  c₀ : ∀(p : ₂ℕ → ∅) → constant p → p ∈ P
  c₀ p _ = p 0̄
  c₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → ∅) → p ∈ P → p ∘ t ∈ P
  c₁ _ _ p _ = p 0̄
  c₂ : ∀(p : ₂ℕ → ∅) → (∃ \(n : ℕ) → ∀(s : ₂Fin n) → (p ∘ (cons s)) ∈ P) → p ∈ P
  c₂ p _ = p 0̄
  c₃ : ∀(p p' : ₂ℕ → ∅) → p ∈ P → ((α : ₂ℕ) → [ p α ≡ p' α ]) → p' ∈ P
  c₃ _ _ z _ = z

continuous-empty : {A : Space} →
                  Σ \(u : ∅ → U A) → continuous {∅Space} {A} u
continuous-empty = (λ ()) , (λ p → λ ())

\end{code}

Terminal C-space.
The unit map to ⒈ is the only probe.

\begin{code}

⒈Space : Space
⒈Space = ⒈ , P , c₀ , c₁ , c₂ , c₃
 where
  P : Subset (₂ℕ → ⒈)
  P p = ⒈
  c₀ : ∀(p : ₂ℕ → ⒈) → constant p → p ∈ P
  c₀ _ _ = ⋆
  c₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → ⒈) → p ∈ P → p ∘ t ∈ P
  c₁ _ _ _ _ = ⋆
  c₂ : ∀(p : ₂ℕ → ⒈) → (∃ \(n : ℕ) → ∀(s : ₂Fin n) → (p ∘ (cons s)) ∈ P) → p ∈ P
  c₂ _ _ = ⋆
  c₃ : ∀(p p' : ₂ℕ → ⒈) → p ∈ P → ((α : ₂ℕ) → [ p α ≡ p' α ]) → p' ∈ P
  c₃ _ _ _ _ = ⋆

continuous-unit : {A : Space} →
                  Σ \(u : U A → ⒈) → continuous {A} {⒈Space} u
continuous-unit = unit , (λ p _ → ⋆)


\end{code}