Chuangjie Xu 2013

\begin{code}

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

module UsingFunext.Space.LocalCartesianClosedness where

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

\end{code}

Subspace

\begin{code}

Subspace : (X : Space) → (U X → Set) → Space
Subspace X Prp = A , R , rc₀ , rc₁ , rc₂
where
A : Set
A = Σ \(x : U X) → Prp x
R : Subset (₂ℕ → A)
R r = pr₁ ∘ r ∈ Probe X
rc₀ : ∀(a : A) → (λ α → a) ∈ R
rc₀ (x , _) = cond₀ X x
rc₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(r : ₂ℕ → A) → r ∈ R → r ∘ t ∈ R
rc₁ t uc r rR = cond₁ X t uc (pr₁ ∘ r) rR
rc₂ : ∀(r : ₂ℕ → A) → (Σ \(n : ℕ) → ∀(s : ₂Fin n) → (r ∘ (cons s)) ∈ R) → r ∈ R
rc₂ r pr = cond₂ X (pr₁ ∘ r) pr

cts-incl : (X : Space) → (Prp : U X → Set) → Map (Subspace X Prp) X
cts-incl X Prp = pr₁ , (λ r rR → rR)

\end{code}

C-spaces have all pullbacks.

\begin{code}

_×[_]_⟨_,_⟩ : (X Z Y : Space) → Map X Z → Map Y Z → Space
X ×[ Z ] Y ⟨ f , g ⟩ = Subspace (X ⊗ Y) Prp
where
Prp : U (X ⊗ Y) → Set
Prp (x , y) = pr₁ f x ≡ pr₁ g y

⟪_×[_]_⟨_,_⟩⟫-pr₁ : (X Z Y : Space) → (f : Map X Z) → (g : Map Y Z) →
Map (X ×[ Z ] Y ⟨ f , g ⟩) X
⟪ X ×[ Z ] Y ⟨ f , g ⟩⟫-pr₁ = (pr₁ ∘ pr₁) , λ r rR → pr₁ rR

⟪_×[_]_⟨_,_⟩⟫-pr₂ : (X Z Y : Space) → (f : Map X Z) → (g : Map Y Z) →
Map (X ×[ Z ] Y ⟨ f , g ⟩) Y
⟪ X ×[ Z ] Y ⟨ f , g ⟩⟫-pr₂ = (pr₂ ∘ pr₁) , λ r rR → pr₂ rR

\end{code}

Equalizers are calculated in the same way as above.

\begin{code}

⟪_,_⟫Eq₍_,_₎ : (X Y : Space) → Map X Y → Map X Y → Space
⟪ X , Y ⟫Eq₍ f , g ₎ = Subspace X Prp
where
Prp : U X → Set
Prp x = pr₁ f x ≡ pr₁ g x

\end{code}

Binary products in a slice category are constructed via pullbacks.

\begin{code}

⟪_,_,_⟫_×_ : (X Z Y : Space) → (f : Map X Z) → (g : Map Y Z) → Map (X ×[ Z ] Y ⟨ f , g ⟩) Z
⟪ X , Z , Y ⟫ f × g = h , cts
where
h : U (X ×[ Z ] Y ⟨ f , g ⟩) → U Z
h ((x , y) , e) = pr₁ f x
cts : continuous (X ×[ Z ] Y ⟨ f , g ⟩) Z h
cts r rR = pr₂ f (pr₁ ∘ pr₁ ∘ r) (pr₁ rR)

\end{code}

Given a continuous map f : X → Y and y : Y, the fiber f⁻¹(y) is a C-space.

\begin{code}

⟪_,_⟫_⁻¹₍_₎ : (X Y : Space) → Map X Y → U Y → Space
⟪ X , Y ⟫ f ⁻¹₍ y ₎ = Subspace X Prp
where
Prp : U X → Set
Prp x = pr₁ f x ≡ y

\end{code}

An exponential in a slice category C-space/X is constructed in the
same way as in Set/X, with a suitable C-topology on its domain.

\begin{code}

dom⟪_,_,_⟫_^_ : (X Z Y : Space) → Map Y Z → Map X Z → Space
dom⟪ X , Z , Y ⟫ g ^ f = A , R , rc₀ , rc₁ , rc₂
where
f⁻¹ : U Z → Space
f⁻¹ z = ⟪ X , Z ⟫ f ⁻¹₍ z ₎
g⁻¹ : U Z → Space
g⁻¹ z = ⟪ Y , Z ⟫ g ⁻¹₍ z ₎
A : Set
A = Σ \(z : U Z) → Map (f⁻¹ z) (g⁻¹  z)
R : Subset (₂ℕ → A)
R r =  (pr₁ ∘ r ∈ Probe Z)
× (∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → U X) → p ∈ Probe X →
(e : ∀(α : ₂ℕ) → pr₁ f(p α) ≡ pr₁(r(t α))) →
(λ α → pr₁(pr₁(pr₂(r(t α)))(p α , e α))) ∈ Probe Y)

lemma : ∀(w₀ w₁ : A) → (u : U ⟪ X , Z ⟫ f ⁻¹₍ pr₁ w₁ ₎) → (e : w₁ ≡ w₀) →
pr₁(pr₁(pr₂ w₀)(pr₁ u , transport _ e (pr₂ u))) ≡ pr₁(pr₁(pr₂ w₁)u)
lemma w .w u refl = refl

rc₀ : ∀(a : A) → (λ α → a) ∈ R
rc₀ (z , φ , cφ) = c₀ , c₁
where
c₀ : (λ α → z) ∈ Probe Z
c₀ = cond₀ Z z
c₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → U X) → p ∈ Probe X →
(e : ∀(α : ₂ℕ) → pr₁ f (p α) ≡ z)
→ (λ α → pr₁ (φ (p α , e α))) ∈ Probe Y
c₁ t uc p pP e = cφ (λ α → p α , e α) pP

rc₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(r : ₂ℕ → A) → r ∈ R → r ∘ t ∈ R
rc₁ t uct r rR = c₀ , c₁
where
c₀ : pr₁ ∘ r ∘ t ∈ Probe Z
c₀ = cond₁ Z t uct (pr₁ ∘ r) (pr₁ rR)
c₁ : ∀(u : ₂ℕ → ₂ℕ) → u ∈ C → ∀(p : ₂ℕ → U X) → p ∈ Probe X →
(e : ∀(α : ₂ℕ) → pr₁ f(p α) ≡ pr₁(r(t(u α))))
→ (λ α → pr₁(pr₁(pr₂(r(t(u α))))(p α , e α))) ∈ Probe Y
c₁ u ucu p pP e = pr₂ rR (t ∘ u) (Lemma[∘-UC] t uct u ucu) p pP e

rc₂ : ∀(r : ₂ℕ → A) → (Σ \(n : ℕ) → ∀(s : ₂Fin n) → (r ∘ (cons s)) ∈ R) → r ∈ R
rc₂ r (n , pr) = c₀ , c₁
where
c₀ : pr₁ ∘ r ∈ Probe Z
c₀ = cond₂ Z (pr₁ ∘ r) (n , λ s → pr₁ (pr s))
c₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → U X) → p ∈ Probe X →
(e : ∀(α : ₂ℕ) → pr₁ f(p α) ≡ pr₁(r(t α)))
→ (λ α → pr₁(pr₁(pr₂(r(t α)))(p α , e α))) ∈ Probe Y
c₁ t uc p pP e = cond₂ Y (λ α → pr₁(pr₁(pr₂(r(t α)))(p α , e α))) (m , prf)
where
m : ℕ
m = pr₁ (Theorem[Coverage-axiom] n t uc)
prf : ∀(s : ₂Fin m)
→ (λ α → pr₁(pr₁(pr₂(r(t(cons s α))))(p(cons s α) , e(cons s α)))) ∈ Probe Y
prf s = transport (Probe Y) claim₂ claim₀
where
s' : ₂Fin n
s' = pr₁ (pr₂ (Theorem[Coverage-axiom] n t uc) s)
t' : ₂ℕ → ₂ℕ
t' = pr₁ (pr₂ (pr₂ (Theorem[Coverage-axiom] n t uc) s))
uc' : t' ∈ C
uc' = pr₁ (pr₂ (pr₂ (pr₂ (Theorem[Coverage-axiom] n t uc) s)))
eq : t ∘ cons s ≡ cons s' ∘ t'
eq = pr₂ (pr₂ (pr₂ (pr₂ (Theorem[Coverage-axiom] n t uc) s)))
psinP : (p ∘ (cons s)) ∈ Probe X
psinP = cond₁ X (cons s) (Lemma[cons-UC] s) p pP
er : ∀(α : ₂ℕ) → r(t(cons s α)) ≡ r(cons s' (t' α))
er α = ap r (fun-ap eq α)
e' : ∀(α : ₂ℕ) → pr₁ f(p(cons s α)) ≡ pr₁(r(cons s' (t' α)))
e' α = transport (λ a → pr₁ f(p(cons s α)) ≡ pr₁ a) (er α) (e(cons s α))
claim₀ : (λ α → pr₁(pr₁(pr₂(r(cons s'(t' α))))(p(cons s α) , e' α))) ∈ Probe Y
claim₀ = pr₂ (pr s') t' uc' (p ∘ (cons s)) psinP e'
claim₁ : ∀(α : ₂ℕ) → pr₁(pr₁(pr₂(r(cons s'(t' α))))(p(cons s α) , e' α))
≡ pr₁(pr₁(pr₂(r(t(cons s α))))(p(cons s α) , e(cons s α)))
claim₁ α = lemma (r(cons s' (t' α))) (r(t(cons s α)))
(p(cons s α) , e(cons s α)) (er α)
claim₂ : (λ α → pr₁(pr₁(pr₂(r(cons s'(t' α))))(p(cons s α) , e' α)))
≡ (λ α → pr₁(pr₁(pr₂(r(t(cons s α))))(p(cons s α) , e(cons s α))))
claim₂ = funext claim₁
--------

⟪_,_,_⟫_^_ : (X Z Y : Space) → (g : Map Y Z) → (f : Map X Z) → Map (dom⟪ X , Z , Y ⟫ g ^ f) Z
⟪ X , Z , Y ⟫ g ^ f = pr₁ , λ r rR → pr₁ rR

\end{code}

Pullback functors:

\begin{code}

⟪_,_⟫_* : (X Y : Space) → (Map X Y) → Mapto Y → Mapto X
⟪ X , Y ⟫ f * (Z , g) = X ×[ Y ] Z ⟨ f , g ⟩ , ⟪ X ×[ Y ] Z ⟨ f , g ⟩⟫-pr₁

\end{code}

Dependent sums (left adjoint) are calculated via composition.

\begin{code}

⟪_,_⟫Σ[_] : (X Y : Space) → Map X Y → Mapto X → Mapto Y
⟪ X , Y ⟫Σ[ f ] (Z , g) = Z , ⟪ Z , X , Y ⟫ f ○ g

dom⟪_,_⟫Σ[_] : (X Y : Space) → Map X Y → Mapto X → Space
dom⟪ X , Y ⟫Σ[ f ] (Z , g) = Z

\end{code}

Dependent products (right adjoint) are via the following diagram

Π[f](g) -----> (g∘f)^f
| ⌟             |
|               | g^f
|               |
V               V
id -----------> f^f.

\begin{code}

dom⟪_,_⟫Π[_] : (X Y : Space) → (Map X Y) → Mapto X → Space
dom⟪ X , Y ⟫Π[ f ] (Z , g) = Subspace A Prp
where
f⁻¹ : U Y → Space
f⁻¹ y = ⟪ X , Y ⟫ f ⁻¹₍ y ₎
f∘g : Map Z Y
f∘g = ⟪ Z , X , Y ⟫ f ○ g
A : Space
A = dom⟪ X , Y , Z ⟫ f∘g ^ f
Prp : U A → Set
Prp (y , φ) = ∀(x : U(f⁻¹ y)) → pr₁ g (pr₁ (pr₁ φ x)) ≡ pr₁ x

⟪_,_⟫Π[_] : (X Y : Space) → (Map X Y) → Mapto X → Mapto Y
⟪ X , Y ⟫Π[ f ] (Z , g) = A , h
where
A : Space
A = dom⟪ X , Y ⟫Π[ f ] (Z , g)
h : Map A Y
h = pr₁ ∘ pr₁ , (λ r rR → pr₁ rR)

\end{code}

According to the diagram, we get the following definition of Π, which
is equivalent to the above one. We use the above one since it is
simpler and easier to work with.

⟪_,_⟫Π[_] : (X Y : Space) → (Map X Y) → Mapto X → Mapto Y
⟪ X , Y ⟫Π[ f ] (Z , g) = A , h
where
dom[f∘g^f] : Space
dom[f∘g^f] = dom⟪ X , Y , Z ⟫ (⟪ Z , X , Y ⟫ f ○ g) ^ f
dom[f^f] : Space
dom[f^f] = dom⟪ X , Y , X ⟫ f ^ f
f⁻¹ : U Y → Space
f⁻¹ y = ⟪ X , Y ⟫ f ⁻¹₍ y ₎

h₀ : Map Y dom[f^f]
h₀ = h , cts
where
h : U Y → U dom[f^f]
h y = y , id , (λ p pP → pP)
cts : continuous {Y} {dom[f^f]} h
cts q qQ = ∧-intro qQ (λ t uc p pP e → pP)

h₁ : Map dom[f∘g^f] dom[f^f]
h₁ = h , cts
where
h : U dom[f∘g^f] → U dom[f^f]
h (y , φ , cφ) = y , ψ , cψ
where
ψ : U (f⁻¹ y) → U (f⁻¹ y)
ψ x = pr₁ g (pr₁ (φ x)) , pr₂ (φ x)
cψ : continuous {f⁻¹ y} {f⁻¹ y} ψ
cψ p pP = pr₂ g (pr₁ ∘ φ ∘ p) (cφ p pP)
cts : continuous {dom[f∘g^f]} {dom[f^f]} h
cts q (qQ₀ , qQ₁) = ∧-intro qQ₀ claim
where
claim : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → U X) → p ∈ Probe X →
(e : ∀(α : ₂ℕ) → [ pr₁ f (p α) ≡ pr₁ (h(q(t α))) ]) →
(λ α → pr₁ g (pr₁(pr₁(pr₂(q(t α)))(p α , e α)))) ∈ Probe X
-- = (λ α → pr₁(pr₁(pr₂(h(q(t α))))(p α , e α))) ∈ Probe X
claim t uc p pP e = pr₂ g r rZ
where
r : ₂ℕ → U Z
r α = pr₁(pr₁(pr₂(q(t α)))(p α , e α))
rZ : r ∈ Probe Z
rZ = qQ₁ t uc p pP e

A : Space
A = Y ×[ dom[f^f] ] dom[f∘g^f] ⟨ h₀ , h₁ ⟩

h : Map A Y
h = ⟪ Y ×[ dom[f^f] ] dom[f∘g^f] ⟨ h₀ , h₁ ⟩⟫-pr₁

dom⟪_,_⟫Π[_] : (X Y : Space) → (Map X Y) → Mapto X → Space
dom⟪ X , Y ⟫Π[ f ] (Z , g)= pr₁(⟪ X , Y ⟫Π[ f ] (Z , g))