Chuangjie Xu 2013 (updated in February 2015, ported to TypeTopology in 2025)

\begin{code}

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

module C-Spaces.UsingNotNotFunExt.Space where

open import MLTT.Spartan

open import C-Spaces.Preliminaries.Sequence
open import C-Spaces.Coverage

\end{code}

C-topologies and C-spaces

\begin{code}

probe-axioms : (X : 𝓀₀ Μ‡ ) β†’ ((β‚‚β„• β†’ X) β†’ 𝓀₀ Μ‡ ) β†’ 𝓀₀ Μ‡
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)
  Γ— (βˆ€(p q : β‚‚β„• β†’ X) β†’ p ∈ P β†’ (βˆ€ Ξ± β†’ ¬¬ (p Ξ± ＝ q Ξ±)) β†’ q ∈ P)

TopologyOn : 𝓀₀ Μ‡  β†’ 𝓀₁ Μ‡
TopologyOn X = Ξ£ P κž‰ ((β‚‚β„• β†’ X) β†’ 𝓀₀ Μ‡ ) , probe-axioms X P

Space : 𝓀₁ Μ‡
Space = Ξ£ X κž‰ 𝓀₀ Μ‡  , TopologyOn X

U : Space β†’ 𝓀₀ Μ‡
U = pr₁

Probe : (X : Space) β†’ (β‚‚β„• β†’ U X) β†’ 𝓀₀ Μ‡
Probe X = pr₁ (prβ‚‚ X)

condβ‚€ : (X : Space) β†’
        βˆ€ x β†’ (Ξ» Ξ± β†’ x) ∈ Probe X
condβ‚€ (_ , _ , cβ‚€ , _) = cβ‚€

cond₁ : (X : Space) β†’
        βˆ€ t β†’ t ∈ C β†’ βˆ€ p β†’ p ∈ Probe X β†’
        p ∘ t ∈ Probe X
cond₁ (_ , _ , _ , c₁ , _) = c₁

condβ‚‚ : (X : Space) β†’
        βˆ€ p β†’ (Ξ£ n κž‰ β„• , βˆ€(s : β‚‚Fin n) β†’ p ∘ cons s ∈ Probe X) β†’
        p ∈ Probe X
condβ‚‚ (_ , _ , _ , _ , cβ‚‚ , _) = cβ‚‚

cond₃ : (X : Space) β†’
        βˆ€ p q β†’ p ∈ Probe X β†’ (βˆ€ Ξ± β†’ ¬¬ (p Ξ± ＝ q Ξ±)) β†’
        q ∈ Probe X
cond₃ (_ , _ , _ , _ , _ , c₃) = c₃

cond₃' : (X : Space) β†’
         βˆ€ p q β†’ p ∈ Probe X β†’ p ∼ q β†’
         q ∈ Probe X
cond₃' X p q pX e = cond₃ X p q pX (Ξ» Ξ± β†’ ¬¬-intro (e Ξ±))

\end{code}

Continuous maps

\begin{code}

continuous : (X Y : Space) β†’ (U X β†’ U Y) β†’ 𝓀₀ Μ‡
continuous X Y f = βˆ€ p β†’ p ∈ Probe X β†’ f ∘ p ∈ Probe Y

Map : Space β†’ Space β†’ 𝓀₀ Μ‡
Map X Y = Ξ£ f κž‰ (U X β†’ U Y) , continuous X Y f

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)

\end{code}