Chuangjie Xu 2012 (updated in February 2015)

\begin{code}

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

module UsingSetoid.Space.DiscreteSpace where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingSetoid.Setoid
open import UsingSetoid.Space.Coverage
open import UsingSetoid.Space.Space
open import UsingSetoid.Space.CartesianClosedness

\end{code}

The locally constant functions ₂ℕ → X on any set X form a C-topology
on X. Any space with such a C-topology is discrete, i.e. all maps from
it to any other space is continuous.

\begin{code}

Setoid≡ : Set  Setoid
Setoid≡ X = X , _≡_ , ≡-isEqRel

LC : {X : Set}  E-map-₂ℕ (Setoid≡ X)  Set
LC (f , _) = locally-constant f

LC-topology : (X : Set)  discrete X  probe-axioms (Setoid≡ X) LC
LC-topology X dis = c₀ , c₁ , c₂ , c₃
 where
  SX : Setoid
  SX = Setoid≡ X

  c₀ : ∀(x : X)  E-λα SX x  LC
  c₀ x = 0 ,  _ _ _  refl) ,  _ _  ≤-zero)

  c₁ :  t  t  C   p  p  LC   SX  p  t  LC
  c₁ (t , et) uc (p , ep) (m , pr , _) =
      Lemma[LM-least-modulus] _≡_ dis _⁻¹ _·_ (p  t) n claim₁
   where
    n : 
    n = pr₁ (uc m)
    claim₀ : ∀(α β : ₂ℕ)  α ≡[ n ] β  t α ≡[ m ] t β
    claim₀ = pr₁ (pr₂ (uc m))
    claim₁ : ∀(α β : ₂ℕ)  α ≡[ n ] β  p(t α)  p(t β)
    claim₁ α β en = pr (t α) (t β) (claim₀ α β en)

  c₂ :  p  (Σ \(n : )  ∀(s : ₂Fin n)   SX  p  Cons s  LC)  p  LC
  c₂ (p , ep) (n , ps) = Lemma[LM-least-modulus] _≡_ dis _⁻¹ _·_ p (n + k) prf
   where
    f : ₂Fin n  
    f s = pr₁ (ps s)
    k : 
    k = pr₁ (max-fin f)
    k-max : ∀(s : ₂Fin n)  f s  k
    k-max = pr₂ (max-fin f)
    fact : ∀(s : ₂Fin n)  ∀(α β : ₂ℕ)  α ≡[ k ] β  p(cons s α)  p(cons s β)
    fact s α β ek = pr₁ (pr₂ (ps s)) α β (Lemma[≡[]-≤] ek (k-max s))
    prf : ∀(α β : ₂ℕ)  α ≡[ n + k ] β  p α  p β
    prf α β enk = goal
     where
      s : ₂Fin n
      s = take n α
      en : α ≡[ n ] β
      en = Lemma[≡[]-≤] enk (Lemma[a≤a+b] n k)
      eqs : take n α  take n β
      eqs = Lemma[≡[]-take] en
      α' : ₂ℕ
      α' = drop n α
       : cons s α'  α
       = Lemma[cons-take-drop] n α
      β' : ₂ℕ
      β' = drop n β
       : cons s β'  β
       i = transport  x  cons x β' i  β i)
                       (eqs ⁻¹) (Lemma[cons-take-drop] n β i)
      awk : ∀(i : )  i < k  α' i  β' i
      awk i i<k = eqα · subgoal · eqβ ⁻¹
       where
        i+n<k+n : i + n < k + n
        i+n<k+n = Lemma[a<b→a+c<b+c] i k n i<k
        i+n<n+k : i + n < n + k
        i+n<n+k = transport  m  (i + n) < m) (Lemma[n+m=m+n] k n) i+n<k+n
        subgoal : α (i + n)  β (i + n)
        subgoal = Lemma[≡[]-<] enk (i + n) i+n<n+k
        le : (n i : )  (α : ₂ℕ)  drop n α i  α (i + n)
        le 0 i α = refl
        le (succ n) i α = le n i (α  succ)
        eqα : α' i  α (i + n)
        eqα = le n i α
        eqβ : β' i  β (i + n)
        eqβ = le n i β
      ek : α' ≡[ k ] β'
      ek = Lemma[<-≡[]] awk
      claim₀ : p α  p(cons s α')
      claim₀ = ep _ _  i  ( i)⁻¹)
      claim₁ : p(cons s α')  p(cons s β')
      claim₁ = fact s α' β' ek
      claim₂ : p(cons s β')  p β
      claim₂ = ep _ _ 
      goal : p α  p β
      goal = claim₀ · claim₁ · claim₂

  c₃ :  p q  p  LC  (∀ α  pr₁ p α  pr₁ q α)  q  LC
  c₃ (p , _) (q , _) (n , prf , min) ex = (n , prf' , min')
   where
    prf' : ∀(α β : ₂ℕ)  α ≡[ n ] β  q α  q β
    prf' α β en = (ex α)⁻¹ · prf α β en · ex β
    min' :  n'  ((α β : ₂ℕ)  α ≡[ n' ] β  q α  q β)  n  n'
    min' n' prn' = min n'  α β en'  (ex α) · (prn' α β en') · (ex β)⁻¹ )


DiscreteSpace : (X : Set)  discrete X  Space
DiscreteSpace X dis = Setoid≡ X , LC , LC-topology X dis


Lemma[discreteness] : (X : Set) (dis : discrete X) (Y : Space)
                     ∀(f : E-map (Setoid≡ X) (U Y))
                     continuous (DiscreteSpace X dis) Y f
Lemma[discreteness] X _ Y f p (m , prf , _) = cond₂ Y _ (m , claim)
 where
  claim : ∀(s : ₂Fin m)
         ( U Y  ( Setoid≡ X  U Y  f  p)  Cons s)  Probe Y
  claim s = cond₃ Y _ _ (cond₀ Y y) claim₁
   where
    y : G Y
    y = pr₁ f (pr₁ p (cons s ))
    claim₀ : ∀(α : ₂ℕ)  pr₁ p (cons s )  pr₁ p (cons s α)
    claim₀ α = prf (cons s ) (cons s α) (Lemma[cons-≡[]] s  α)
    claim₁ : ∀(α : ₂ℕ)  E (U Y) y (pr₁ f (pr₁ p (cons s α)))
    claim₁ α = pr₂ f _ _ (claim₀ α)

\end{code}

All the uniformly continuous maps ₂ℕ → ₂ (and ₂ℕ → ℕ) are
locally constant. And hence they form a C-topology on ₂ (and ℕ).

The coproduct 1 + 1:

\begin{code}

₂Space : Space
₂Space = DiscreteSpace  ₂-discrete

Lemma[discrete-₂Space] : (X : Space)   f  continuous ₂Space X f
Lemma[discrete-₂Space] X f = Lemma[discreteness]  ₂-discrete X f

continuous-if : (A : Space)  Map ₂Space (A  A  A)
continuous-if A = (IF , e-IF) , c-IF
 where
  _~_ : G A  G A  Set
  _~_ = E (U A)
  IF :   G (A  A  A)
  IF b = (if-b , e-if-b) , c-if-b
   where
    if-b : G A  G (A  A)
    if-b a₀ = (if-b-a₀ , e-if-b-a₀) , c-if-b-a₀
     where
      if-b-a₀ : G A  G A
      if-b-a₀ a₁ = if b a₀ a₁
      e-if-b-a₀ :  a₁ a₁'  a₁ ~ a₁'  if b a₀ a₁ ~ if b a₀ a₁'
      e-if-b-a₀ a₁ a₁' ea₁ = lemma b
       where
        lemma :  i   if i a₀ a₁ ~ if i a₀ a₁'
        lemma  = Refl (U A) a₀
        lemma  = ea₁
      c-if-b-a₀ : continuous A A (if-b-a₀ , e-if-b-a₀)
      c-if-b-a₀ p pA = cond₃ A _ _ (lemma₀ b) (lemma₁ b)
       where
        f :   E-map-₂ℕ (U A)
        f  = E-λα (U A) a₀
        f  = p
        lemma₀ : ∀(i : )  f i  Probe A -- (λ a₁ → if i a₀ a₁) ∘ p ∈ Probe A
        lemma₀  = cond₀ A a₀
        lemma₀  = pA
        lemma₁ :  i   α  pr₁ (f i) α ~ if i a₀ (pr₁ p α)
        lemma₁  α = Refl (U A) a₀
        lemma₁  α = Refl (U A) (pr₁ p α)
    e-if-b :  a₀ a₀'  a₀ ~ a₀'   a₁  if b a₀ a₁ ~ if b a₀' a₁
    e-if-b a₀ a₀' ea₀ a₁ = lemma b
     where
      lemma :  i   if i a₀ a₁ ~ if i a₀' a₁
      lemma  = ea₀
      lemma  = Refl (U A) a₁
    c-if-b : continuous A (A  A) (if-b , e-if-b)
    c-if-b p pA q qA t tC = cond₃ A _ _ (lemma₀ b) (lemma₁ b)
     where
      f :   E-map-₂ℕ (U A)
      f  =  U A  p  t
      f  = q
      lemma₀ :  i   f i  Probe A
      lemma₀  = cond₁ A t tC p pA
      lemma₀  = qA
      lemma₁ :  i   α  pr₁ (f i) α ~ if i (pr₁ p (pr₁ t α)) (pr₁ q α)
      lemma₁  α = Refl (U A) (pr₁ p (pr₁ t α))
      lemma₁  α = Refl (U A) (pr₁ q α)
  e-IF :  b b'  b  b'   a₀ a₁  if b a₀ a₁ ~ if b' a₀ a₁
  e-IF b .b refl = Refl (U (A  A  A)) (IF b)
  c-IF : continuous ₂Space (A  A  A) (IF , e-IF)
  c-IF = Lemma[discrete-₂Space] (A  A  A) (IF , e-IF)

\end{code}

The natural numbers object:

\begin{code}

ℕSpace : Space
ℕSpace = DiscreteSpace  ℕ-discrete

Lemma[discrete-ℕSpace] : (X : Space)   f  continuous ℕSpace X f
Lemma[discrete-ℕSpace] X f = Lemma[discreteness]  ℕ-discrete X f

continuous-succ : Map ℕSpace ℕSpace
continuous-succ = E-succ , c-succ
 where
  E-succ : E-map Eℕ Eℕ
  E-succ = (succ , λ _ _  ap succ)
  c-succ :  p  p  LC   Eℕ  Eℕ  E-succ  p  LC
  c-succ (p , ep) (n , prf , min) = n , prf' , min'
   where
    prf' : ∀(α β : ₂ℕ)  α ≡[ n ] β  succ (p α)  succ (p β)
    prf' α β en = ap succ (prf α β en)
    min' : ∀(n' : )  (∀ α β  α ≡[ n' ] β  succ(p α)  succ(p β))  n  n'
    min' n' pr' = min n'  α β en'  succ-injective(pr' α β en'))

continuous-rec : (A : Space)  Map A ((ℕSpace  A  A)  ℕSpace  A)
continuous-rec A = (REC , e-REC) , continuity-of-REC
 where
  _~_ : G A  G A  Set
  _~_ = E (U A)
  ū : G (ℕSpace  A  A)    G A  G A
  ū f n = pr₁ (pr₁ (pr₁ (pr₁ f) n))
  ē : (f : G (ℕSpace  A  A))  (n : )
      a a'  a ~ a'  ū f n a ~ ū f n a'
  ē f n = pr₂ (pr₁ (pr₁ (pr₁ f) n))

  REC : G A  G ((ℕSpace  A  A)  ℕSpace  A)
  REC a = ((rec-a , e-rec-a) , c-rec-a)
   where
    rec-a : G (ℕSpace  A  A)  G (ℕSpace  A)
    rec-a f = (rec-a-f , e-rec-a-f) , c-rec-a-f
     where
      rec-a-f :   G A
      rec-a-f = rec a (ū f)
      e-rec-a-f :  n m  n  m  rec a (ū f) n ~ rec a (ū f) m
      e-rec-a-f n .n refl = Refl (U A) (rec a (ū f) n)
      c-rec-a-f : continuous ℕSpace A (rec-a-f , e-rec-a-f)
      c-rec-a-f = Lemma[discrete-ℕSpace] A (rec-a-f , e-rec-a-f)
    e-rec-a :  f f'  (∀ n b  ū f n b ~ ū f' n b)
              n  rec a (ū f) n ~ rec a (ū f') n 
    e-rec-a f f' ef  0       = Refl (U A) a
    e-rec-a f f' ef (succ n) = Trans (U A) _ _ _ claim₀ claim₁
     where
      claim₀ : rec a (ū f) (succ n) ~ ū f' n (rec a (ū f) n)
      claim₀ = ef n (rec a (ū f) n)
      claim₁ : ū f' n (rec a (ū f) n) ~ rec a (ū f') (succ n)
      claim₁ = ē f' n _ _ (e-rec-a f f' ef n)
    c-rec-a : continuous (ℕSpace  A  A) (ℕSpace  A) (rec-a , e-rec-a)
    c-rec-a p pNAA q (n , qr , _) t uc = cond₂ A _ (n , prf)
     where
      rec-a-p : E-map-₂ℕ (U(ℕSpace  A))
      rec-a-p =  U (ℕSpace  A  A)  U (ℕSpace  A)  (rec-a , e-rec-a)  p
      rec-a-pt-q : E-map-₂ℕ (U A)
      rec-a-pt-q = Exp ℕSpace A rec-a-p t q
      prf : ∀(s : ₂Fin n)   U A  rec-a-pt-q  Cons s  Probe A
      prf s = cond₃ A _ _ (lemma qs0) claim
       where
        tsC : t  Cons s  C
        tsC = Lemma[◎-UC] t uc (Cons s) (Lemma[cons-UC] s)
        pts : E-map-₂ℕ (U (ℕSpace  A  A))
        pts =  U (ℕSpace  A  A)  p  (t  Cons s)
        f :   E-map-₂ℕ (U A)
        f k = g k , eg k
         where
          g :   ₂ℕ  G A
          g i α = rec a (ū (pr₁ pts α)) i
          eg :  i   α α'  α  α'  g i α ~ g i α'
          eg  0       _ _  _  = Refl (U A) a
          eg (succ i) α α'  = Trans (U A) _ _ _  claim₁ claim₂
           where
            claim₀ : g i α ~ g i α'
            claim₀ = eg i α α' 
            claim₁ : g (succ i) α ~ ū (pr₁ pts α) i (g i α')
            claim₁ = ē (pr₁ pts α) i _ _ claim₀
            claim₂ : ū (pr₁ pts α) i (g i α') ~ g (succ i) α'
            claim₂ = pr₂ pts _ _  _ _
        lemma :  k  f k  Probe A
        lemma  0       = cond₀ A a
        lemma (succ k) = cond₃ A _ _ claim₁ claim₂
         where
          ptsk : E-map-₂ℕ (U (A  A))
          ptsk = Exp ℕSpace (A  A) p (t  Cons s) (E-λα Eℕ k)
          claim₀ : ptsk  Probe (A  A)
          claim₀ = pNAA (E-λα Eℕ k) (cond₀ ℕSpace k) (t  Cons s) tsC
          ptskfk : E-map-₂ℕ (U A)
          ptskfk = Exp A A ptsk (E-id E₂ℕ) (f k)
          claim₁ : ptskfk  Probe A
          claim₁ = claim₀ (f k) (lemma k) (E-id E₂ℕ) Lemma[id-UC]
          claim₂ :  α  pr₁ ptskfk α ~ pr₁ (f (succ k)) α
          claim₂ α = Refl (U A) (pr₁ ptskfk α)
        qs0 : 
        qs0 = pr₁ q (cons s )
        claim :  α  pr₁ (f qs0) α ~ pr₁ rec-a-pt-q (cons s α)
        claim α = pr₂ (pr₁ (rec-a (pr₁ pts α))) _ _
                      (qr _ _ (Lemma[cons-≡[]] s  α))

  e-REC :  a a'  a ~ a'   f n  rec a (ū f) n ~ rec a' (ū f) n
  e-REC a a' ea f  0       = ea
  e-REC a a' ea f (succ n) = ē f n _ _ (e-REC a a' ea f n)

  continuity-of-REC : continuous A ((ℕSpace  A  A)  ℕSpace  A) (REC , e-REC)
  continuity-of-REC p pA q qNAA t tC u (n , ur , _) v vC = cond₂ A _ (n , prf)
   where
    rec-p : E-map-₂ℕ (U ((ℕSpace  A  A)  ℕSpace  A))
    rec-p =  U A  U ((ℕSpace  A  A)  ℕSpace  A)  (REC , e-REC)  p
    rec-pt-q : E-map-₂ℕ (U (ℕSpace  A))
    rec-pt-q = Exp (ℕSpace  A  A) (ℕSpace  A) rec-p t q
    rec-ptv-qv-u : E-map-₂ℕ (U A)
    rec-ptv-qv-u = Exp ℕSpace A rec-pt-q v u
    prf : ∀(s : ₂Fin n)   U A  rec-ptv-qv-u  Cons s  Probe A
    prf s = cond₃ A _ _ (lemma us0) claim
     where
      vsC : v  Cons s  C
      vsC = Lemma[◎-UC] v vC (Cons s) (Lemma[cons-UC] s)
      ptvs : E-map-₂ℕ (U A)
      ptvs =  U A  p  (t  v  Cons s)
      qvs : E-map-₂ℕ (U (ℕSpace  A  A))
      qvs =  U (ℕSpace  A  A)  q  (v  Cons s)
      tvsC : t  v  Cons s  C
      tvsC = Lemma[◎-UC] t tC (v  Cons s) vsC
      f :   E-map-₂ℕ (U A)
      f k = g k , eg k
       where
        g :   ₂ℕ  G A
        g i α = rec (pr₁ ptvs α) (ū(pr₁ qvs α)) i
        eg :  i   α α'  α  α'  g i α ~ g i α'
        eg  0       α α'  = pr₂ p _ _ (pr₂ t _ _ (pr₂ v _ _ (cons-E-map s _ _ )))
        eg (succ i) α α'  = Trans (U A) _ _ _ claim₁ claim₂
         where
          claim₀ : g i α ~ g i α'
          claim₀ = eg i α α' 
          claim₁ : g (succ i) α ~ ū (pr₁ qvs α) i (g i α')
          claim₁ = ē (pr₁ qvs α) i _ _ claim₀
          claim₂ : ū (pr₁ qvs α) i (g i α') ~ g (succ i) α'
          claim₂ = pr₂ qvs _ _  _ _
      lemma :  k  f k  Probe A
      lemma  0       = cond₁ A (t  v  Cons s) tvsC p pA
      lemma (succ k) = cond₃ A _ _ claim₁ claim₂
       where
        qvsk : E-map-₂ℕ (U (A  A))
        qvsk = Exp ℕSpace (A  A) q (v  Cons s) (E-λα Eℕ k) 
        claim₀ : qvsk  Probe (A  A)
        claim₀ = qNAA (E-λα Eℕ k) (cond₀ ℕSpace k) (v  Cons s) vsC
        qvskfk : E-map-₂ℕ (U A)
        qvskfk = Exp A A qvsk (E-id E₂ℕ) (f k)
        claim₁ : qvskfk  Probe A
        claim₁ = claim₀ (f k) (lemma k) (E-id E₂ℕ) Lemma[id-UC]
        claim₂ :  α  pr₁ qvskfk α ~ pr₁ (f (succ k)) α
        claim₂ α = Refl (U A) (pr₁ qvskfk α)
      us0 : 
      us0 = pr₁ u (cons s )
      claim :  α  pr₁ (f us0) α ~ pr₁ rec-ptv-qv-u (cons s α) 
      claim α = pr₂ (pr₁ (pr₁ rec-pt-q (pr₁ v (cons s α)))) _ _
                    (ur _ _ (Lemma[cons-≡[]] s  α))

\end{code}