Chuangjie Xu 2012 (updated in February 2015)


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

module UsingFunext.Space.Space where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingFunext.Space.Coverage


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.


probe-axioms : (X : Set)  Subset(₂ℕ  X)  Set
probe-axioms X P =
    (∀(x : X)   α  x)  P)
  × (∀(t : ₂ℕ  ₂ℕ)  t  C  ∀(p : ₂ℕ  X)  p  P  p  t  P)
  × (∀(p : ₂ℕ  X)  (Σ \(n : )  ∀(s : ₂Fin n)  (p  (cons s))  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 = pr₁

Probe : (X : Space)  Subset(₂ℕ  U X) 
Probe X = pr₁ (pr₂ X)

cond₀ : (X : Space) 
        ∀(x : U X)   α  x)  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₂


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


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 X Y Z f cf g cg p pP = cg (f  p) (cf p pP)

continuous-constant : (X Y : Space)  U Y  Map X Y
continuous-constant X Y y =  _  y) ,  _ _  cond₀ Y y)

⟪_,_,_⟫_○_ : (X Y Z : Space)  Map Y Z  Map X Y  Map X Z
 X , Y , Z  (g , cg)  (f , cf) = (g  f) , λ p pP  cg (f  p) (cf p pP)