Chuangjie Xu, 9 Sep 2014

\begin{code}

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

module CwF.Space.Base where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingFunext.Space.Coverage
open import CwF.Space.Preliminaries

\end{code}

Spaces and continuous maps

\begin{code}

Space : Set₁
Space = Σ \(X : Set) → Σ \(P : (₂ℕ → X) → Set) →
    (∀(x : X) → (λ α → x) ∈ P)
  × (∀(p : ₂ℕ → X) → p ∈ P → ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → p ∘ t ∈ P)
  × (∀(ρ : ₂ → ₂ℕ → X) → (∀(i : ₂) → ρ i ∈ P) → ▢ ρ ∈ P)

Map : Space → Space → Set
Map (X , P , _) (Y , Q , _) = Σ \(f : X → Y) → ∀ p → p ∈ P → (f ∘ p) ∈ Q

U = pr₁

Probe : (X : Space) → _
Probe (_ , P , _) = P

s⑴ : (X : Space) → _
s⑴ (_ , _ , c₁ , _) = c₁

s⑵ : (X : Space) → _
s⑵ (_ , _ , _ , c₂ , _) = c₂

s⑶ : (X : Space) → _
s⑶ (_ , _ , _ , _ , c₃) = c₃

\end{code}

Contexts are intepreted as spaces and substitutions as continuous maps.

\begin{code}

Cxt : Set₁
Cxt = Space

Sub : Cxt → Cxt → Set
Sub = Map

\end{code}

The empty context

\begin{code}

ε : Cxt
ε = ⒈ , (λ _ → ⒈) , (λ _ → ⋆) , (λ _ _ _ _ → ⋆) , (λ _ _ → ⋆)

\end{code}

The identity substitution

\begin{code}

Ι : (Γ : Cxt) → Sub Γ Γ
Ι Γ = id , (λ p pΓ → pΓ)

\end{code}

Substitution composition

\begin{code}

⟪_,_,_⟫_○_ : (Θ Δ Γ : Cxt) → Sub Δ Θ → Sub Γ Δ → Sub Γ Θ
⟪ Θ , Δ , Γ ⟫ (σ , nσ) ○ (τ , nτ) = (σ ∘ τ) , (λ p pΓ → nσ (τ ∘ p) (nτ p pΓ))

\end{code}

Equations

\begin{code}

-- 1 ∘ σ = σ
EQCat₀ : ∀(Γ Δ : Cxt) (σ : Sub Δ Γ)
       → (⟪ Γ , Γ , Δ ⟫ Ι Γ ○ σ) ≡ σ
EQCat₀ Γ Δ σ = refl

-- σ ∘ 1 = σ
EQCat₁ : ∀(Γ Δ : Cxt) (σ : Sub Δ Γ)
       → (⟪ Γ , Δ , Δ ⟫ σ ○ Ι Δ) ≡ σ
EQCat₁ Γ Δ σ = refl

-- (σ ∘ τ) ∘ ν = σ ∘ (τ ∘ ν)
EQCat₂ : ∀(Γ Δ Θ Ξ : Cxt) (σ : Sub Δ Γ) (τ : Sub Θ Δ) (ν : Sub Ξ Θ)
       →   (⟪ Γ , Θ , Ξ ⟫ (⟪ Γ , Δ , Θ ⟫ σ ○ τ) ○ ν)
         ≡ (⟪ Γ , Δ , Ξ ⟫ σ ○ (⟪ Δ , Θ , Ξ ⟫ τ ○ ν))
EQCat₂ Γ Δ Θ Ξ σ τ ν = refl

\end{code}