Chuangjie Xu 2012 (updated in February 2015)

\begin{code}

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

module UsingSetoid.Space.Space where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingSetoid.Setoid
open import UsingSetoid.Space.Coverage

\end{code}

We use E-maps ₂ℕ → X, called the probes, to topologize a setoid X.
Thus a topology on a setoid X, in our sense, is a setoid of E-maps
₂ℕ → X, called the probes, satisfying some conditions. We call it
the C-topology on X.

\begin{code}

probe-axioms : (X : Setoid) → Subset (E-map-₂ℕ X) → Set
probe-axioms X P =
    (∀(x : U X) → E-λα X x ∈ P)
  × (∀(t : E-map-₂ℕ-₂ℕ) → t ∈ C → ∀(p : E-map-₂ℕ X) → p ∈ P → ⟨ X ⟩ p ◎ t ∈ P)
  × (∀(p : E-map-₂ℕ X) → (Σ \(n : ℕ) → ∀(s : ₂Fin n) → ⟨ X ⟩ p ◎ Cons s ∈ P) → p ∈ P)
  × (∀(p q : E-map-₂ℕ X) → p ∈ P → (∀ α → E X (pr₁ p α) (pr₁ q α)) → q ∈ P)

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

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

G : Space → Set
G ((X , _) , _) = X

Probe : (X : Space) → Subset (E-map-₂ℕ (U X)) 
Probe (_ , P , _) = P

cond₀ : (X : Space) →
        ∀(x : G X) → E-λα (U X) x ∈ Probe X
cond₀ (_ , _ , c₀ , _) = c₀

cond₁ : (X : Space) →
        ∀(t : E-map-₂ℕ-₂ℕ) → t ∈ C → ∀(p : E-map-₂ℕ (U X)) → p ∈ Probe X →
        ⟨ U X ⟩ p ◎ t ∈ Probe X
cond₁ (_ , _ , _ , c₁ , _) = c₁

cond₂ : (X : Space) →
        ∀(p : E-map-₂ℕ (U X)) → (Σ \(n : ℕ) → ∀(s : ₂Fin n) → ⟨ U X ⟩ p ◎ Cons s ∈ Probe X) →
        p ∈ Probe X
cond₂ (_ , _ , _ , _ , c₂ , _) = c₂

cond₃ : (X : Space) →
        ∀(p q : E-map-₂ℕ (U X)) → p ∈ Probe X → (∀ α → E (U X) (pr₁ p α) (pr₁ q α)) →
        q ∈ 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) → E-map (U X) (U Y) → Set
continuous X Y f = ∀ p → p ∈ Probe X → ⟨ U X ∣ U Y ⟩ f ◎ p ∈ Probe Y

Map : Space → Space → Set
Map X Y = Σ \(f : E-map (U X) (U Y)) → continuous X Y f

id-is-continuous : ∀{X : Space} → continuous X X (E-id (U X))
id-is-continuous _ pinP = pinP

∘-preserves-continuity : (X Y Z : Space) →
    ∀(f : E-map (U X) (U Y)) → continuous X Y f →
    ∀(g : E-map (U Y) (U Z)) → continuous Y Z g →
    continuous X Z (⟨ U X ∣ U Y ∣ U Z ⟩ g ◎ f)
∘-preserves-continuity X Y Z f cf g cg p pP = cg (⟨ U X ∣ U Y ⟩ f ◎ p) (cf p pP)

continuous-constant : (X Y : Space) → G Y → Map X Y
continuous-constant X Y y = (f , ef) , cf
 where
  f : G X → G Y
  f _ = y
  ef : ∀ x x' → E (U X) x x' → E (U Y) (f x) (f x')
  ef _ _ _ = Refl (U Y) y
  cf : continuous X Y (f , ef)
  cf p pX = cond₃ Y _ _ (cond₀ Y y) (λ _ → Refl (U Y) y)

\end{code}