Chuangjie Xu, 2013

This corresponds to part of Section 2 of the paper
http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf

\begin{code}

module Space-LCC where

open import MiniLibrary
open import Sequence
open import UniformContinuity
open import Inequality
open import Sequence
open import Space
open import Space-product
open import Space-exponential
open import not-not

\end{code}

We observe that Agda (2.3.2.1) is not able to infer implict arguments
in this file, and hence we avoided implicit arguments.

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 w = π₀ f (π₀ w) ≡ π₀ g (π₁ w)

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

⟪_×[_]_⟨_,_⟩⟫-π₁ : (X Z Y : Space) → (f : Map X Z) → (g : Map Y Z) →
                   Map (X ×[ Z ] Y ⟨ f , g ⟩) Y
⟪ X ×[ Z ] Y ⟨ f , g ⟩⟫-π₁ = (π₁ ∘ π₀) , λ r rR → ∧-elim₁ 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 = π₀ f x ≡ π₀ 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) = π₀ f x
  cts : continuous {X ×[ Z ] Y ⟨ f , g ⟩} {Z} h
  cts r rR = π₁ f (π₀ ∘ π₀ ∘ r) (∧-elim₀ 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 = [ π₀ f x ≡ y ]
          --------------

\end{code}

To show that exponentials in a slice category satisfy the probe
axioms, we need the following lemma, which is proved using funext.

\begin{code}

open import not-not-funext

dep-functor : {X : Set}{Y : [ X ] → Set} → ((x : X) → Y(hide x)) → (xh : [ X ]) → [ Y xh ]
dep-functor {X} {Y} f xh = extension claim xh
 where
  claim : X → [ Y xh ]
  claim x = [transport] {[ X ]} {Y} (funext¹ (λ f → ∅-elim(xh f))) (hide(f x))
                                     ------

\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₂ , 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 =  (π₀ ∘ r ∈ Probe Z)
       ∧ (∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → U X) → p ∈ Probe X →
           (e : ∀(α : ₂ℕ) → [ π₀ f(p α) ≡ π₀(r(t α)) ]) →
           (λ α → π₀(π₀(π₁(r(t α)))(p α , e α))) ∈ Probe Y)

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

  lemma[] : ∀(w₀ w₁ : A) → (u : U ⟪ X , Z ⟫ f ⁻¹₍ π₀ w₁ ₎) → ([e] : [ w₁ ≡ w₀ ]) →
             [ π₀(π₀(π₁ w₀)(π₀ u , [transport] [e] (π₁ u))) ≡ π₀(π₀(π₁ w₁)u) ]
  lemma[] w₀ w₁ u = dep-functor (lemma w₀ w₁ u)

  rc₀ : ∀(r : ₂ℕ → A) → constant r → r ∈ R
  rc₀ r cr = ∧-intro c₀ c₁
   where
    c₀ : π₀ ∘ r ∈ Probe Z
    c₀ = cond₀ Z (π₀ ∘ r) (Lemma[∘-constant] r π₀ cr)
    c₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → U X) → p ∈ Probe X → (e : ∀(α : ₂ℕ) → [ π₀ f (p α) ≡ π₀(r(t α)) ]) →
          (λ α → π₀(π₀(π₁(r(t α)))(p α , e α))) ∈ Probe Y
    c₁ t uc p pP e = cond₃ Y (λ α → π₀(π₀(π₁(r 0̄))(p α , e0̄ α)))
                             (λ α → π₀(π₀(π₁(r(t α)))(p α , e α)))
                             claim₀ claim₁
     where
      e0̄ : ∀(α : ₂ℕ) → [ π₀ f (p α) ≡ π₀(r 0̄) ]
      e0̄ α = [transport] {A} {λ a → π₀ f (p α) ≡ π₀ a} (hide (cr (t α) 0̄)) (e α)
      claim₀ : (λ α → π₀(π₀(π₁(r 0̄))(p α , e0̄ α))) ∈ Probe Y
      claim₀ = π₁ (π₁(r 0̄)) (λ α → (p α , e0̄ α)) pP
      claim₁ : ∀(α : ₂ℕ) → [ π₀(π₀(π₁(r 0̄))(p α , e0̄ α)) ≡ π₀(π₀(π₁(r(t α)))(p α , e α)) ]
      claim₁ α = hide (lemma (r 0̄) (r(t α)) (p α , e α) (cr (t α) 0̄))

  rc₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(r : ₂ℕ → A) → r ∈ R → r ∘ t ∈ R
  rc₁ t uct r rR = ∧-intro c₀ c₁
   where
    c₀ : π₀ ∘ r ∘ t ∈ Probe Z
    c₀ = cond₁ Z t uct (π₀ ∘ r) (∧-elim₀ rR)
    c₁ : ∀(u : ₂ℕ → ₂ℕ) → u ∈ C → ∀(p : ₂ℕ → U X) → p ∈ Probe X → (e : ∀(α : ₂ℕ) → [ π₀ f(p α) ≡ π₀(r(t(u α))) ]) →
          (λ α → π₀(π₀(π₁(r(t(u α))))(p α , e α))) ∈ Probe Y
    c₁ u ucu p pP e = ∧-elim₁ 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) = ∧-intro c₀ c₁
   where
    c₀ : π₀ ∘ r ∈ Probe Z
    c₀ = cond₂ Z (π₀ ∘ r) (n , λ s → ∧-elim₀ (pr s))
    c₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → U X) → p ∈ Probe X → (e : ∀(α : ₂ℕ) → [ π₀ f(p α) ≡ π₀(r(t α)) ]) →
          (λ α → π₀(π₀(π₁(r(t α)))(p α , e α))) ∈ Probe Y
    c₁ t uc p pP e = cond₂ Y (λ α → π₀(π₀(π₁(r(t α)))(p α , e α))) (∃-intro n' prf)
     where
      n' : ℕ
      n' = ∃-witness (Axiom[coverage] n t uc)
      prf : ∀(s' : ₂Fin n') → (λ α → π₀(π₀(π₁(r(t(cons s' α))))(p(cons s' α) , e(cons s' α)))) ∈ Probe Y
      prf s' = cond₃ Y (λ α → π₀(π₀(π₁(r(cons s''(t'' α))))(p(cons s' α) , e' α)))
                       (λ α → π₀(π₀(π₁(r(t(cons s' α))))(p(cons s' α) , e(cons s' α))))
                       claim₀ claim₁
       where
        s'' : ₂Fin n
        s'' = ∃-witness (∃-elim (Axiom[coverage] n t uc) s')
        t'' : ₂ℕ → ₂ℕ
        t'' = ∃-witness (∃-elim (∃-elim (Axiom[coverage] n t uc) s'))
        uct'' : t'' ∈ C
        uct'' = ∧-elim₀ (∃-elim (∃-elim (∃-elim (Axiom[coverage] n t uc) s')))
        eq : [ t ∘ (cons s') ≡ (cons s'') ∘ t'' ]
        eq = ∧-elim₁ (∃-elim (∃-elim (∃-elim (Axiom[coverage] n t uc) s')))
        ps'inP : (p ∘ (cons s')) ∈ Probe X
        ps'inP = 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' : ∀(α : ₂ℕ) → [ π₀ f(p(cons s' α)) ≡ π₀(r(cons s'' (t'' α))) ]
        e' α = [transport] {A} {λ a → π₀ f(p(cons s' α)) ≡ π₀ a} (er α) (e(cons s' α))
        claim₀ : (λ α → π₀(π₀(π₁(r(cons s''(t'' α))))(p(cons s' α) , e' α))) ∈ Probe Y
        claim₀ = ∧-elim₁ (pr s'') t'' uct'' (p ∘ (cons s')) ps'inP e'
        claim₁ : ∀(α : ₂ℕ) → [ π₀(π₀(π₁(r(cons s''(t'' α))))(p(cons s' α) , e' α)) ≡
                               π₀(π₀(π₁(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 α)

  rc₃ : ∀(r r' : ₂ℕ → A) → r ∈ R → (∀(α : ₂ℕ) → [ r α ≡ r' α ]) → r' ∈ R
  rc₃ r r' rR ex = ∧-intro c₀ c₁
   where
    c₀ : π₀ ∘ r' ∈ Probe Z
    c₀ = cond₃ Z (π₀ ∘ r) (π₀ ∘ r') (∧-elim₀ rR) (λ α → [ap] π₀ (ex α))
    c₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → U X) → p ∈ Probe X → (e' : ∀(α : ₂ℕ) → [ π₀ f(p α) ≡ π₀(r'(t α)) ]) →
          (λ α → π₀(π₀(π₁(r'(t α)))(p α , e' α))) ∈ Probe Y
    c₁ t uc p pP e' = cond₃ Y (λ α → π₀(π₀(π₁(r(t α)))(p α , e α)))
                              (λ α → π₀(π₀(π₁(r'(t α)))(p α , e' α)))
                              claim₀ claim₁
     where
      e : ∀(α : ₂ℕ) → [ π₀ f(p α) ≡ π₀(r(t α)) ]
      e α = [transport] {A} {λ a → π₀ f(p α) ≡ π₀ a} ([sym](ex (t α))) (e' α)
      claim₀ : (λ α → π₀(π₀(π₁(r(t α)))(p α , e α))) ∈ Probe Y
      claim₀ = ∧-elim₁ rR t uc p pP e
      claim₁ : ∀(α : ₂ℕ) → [ π₀(π₀(π₁(r(t α)))(p α , e α)) ≡ π₀(π₀(π₁(r'(t α)))(p α , e' α)) ]
      claim₁ α = lemma[] (r(t α)) (r'(t α)) (p α , e' α) ([sym](ex (t α)))


⟪_,_,_⟫_^_ : (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 = π₀ , λ r rR → π₀ 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 ⟩⟫-π₀

\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)) → π₀ g (π₀ (π₀ φ x)) ≡ π₀ 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 = π₀ ∘ π₀ , (λ r rR → ∧-elim₀ 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 = π₀ g (π₀ (φ x)) , π₁ (φ x)
      cψ : continuous {f⁻¹ y} {f⁻¹ y} ψ
      cψ p pP = π₁ g (π₀ ∘ φ ∘ 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 : ∀(α : ₂ℕ) → [ π₀ f (p α) ≡ π₀ (h(q(t α))) ]) →
              (λ α → π₀ g (π₀(π₀(π₁(q(t α)))(p α , e α)))) ∈ Probe X
         -- = (λ α → π₀(π₀(π₁(h(q(t α))))(p α , e α))) ∈ Probe X
      claim t uc p pP e = π₁ g r rZ
       where
        r : ₂ℕ → U Z
        r α = π₀(π₀(π₁(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₁ ⟩⟫-π₀

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