Chuangjie Xu 2012 (updated in February 2015)

\begin{code}

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

module UsingFunext.Space.CartesianClosedness where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingFunext.Space.Coverage
open import UsingFunext.Space.Space

\end{code}

The category of C-spaces is cartesian closed.

The terminal C-space:

\begin{code}

⒈Space : Space
⒈Space = ⒈ , P , c₀ , c₁ , c₂
 where
  P : Subset (₂ℕ → ⒈)
  P p = ⒈
  c₀ : ∀(x : ⒈) → (λ α → x) ∈ P
  c₀ _ = ⋆
  c₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → ⒈) → p ∈ P → p ∘ t ∈ P
  c₁ _ _ _ _ = ⋆
  c₂ : ∀(p : ₂ℕ → ⒈) → (Σ \(n : ℕ) → ∀(s : ₂Fin n) → (p ∘ (cons s)) ∈ P) → p ∈ P
  c₂ _ _ = ⋆

continuous-unit : (A : Space) → Map A ⒈Space
continuous-unit A = unit , (λ p _ → ⋆)

\end{code}

Binary product of C-spaces:

\begin{code}

infixl  _⊗_

_⊗_ : Space → Space → Space
(X , P , pc₀ , pc₁ , pc₂) ⊗ (Y , Q , qc₀ , qc₁ , qc₂) = (X × Y , R , rc₀ , rc₁ , rc₂)
 where
  R : Subset(₂ℕ → X × Y)
  R r = ((pr₁ ∘ r) ∈ P) × ((pr₂ ∘ r) ∈ Q)

  rc₀ : ∀(w : X × Y) → (λ α → w) ∈ R
  rc₀ (x , y) = c₀ , c₁
   where
    c₀ : (λ α → x) ∈ P
    c₀ = pc₀ x
    c₁ : (λ α → y) ∈ Q
    c₁ = qc₀ y

  rc₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(r : ₂ℕ → X × Y) →  r ∈ R → r ∘ t ∈ R
  rc₁ t uc r rR = c₀ , c₁
   where
    c₀ : pr₁ ∘ (r ∘ t) ∈ P
    c₀ = pc₁ t uc (pr₁ ∘ r) (pr₁ rR)
    c₁ : pr₂ ∘ (r ∘ t) ∈ Q
    c₁ = qc₁ t uc (pr₂ ∘ r) (pr₂ rR)

  rc₂ : ∀(r : ₂ℕ → X × Y) → (Σ \(n : ℕ) → ∀(s : ₂Fin n) → (r ∘ (cons s)) ∈ R) → r ∈ R
  rc₂ r (n , prf) = c₀ , c₁
   where
    c₀ : pr₁ ∘ r ∈ P
    c₀ = pc₂ (pr₁ ∘ r) (n , (λ s → pr₁(prf s)))
    c₁ : pr₂ ∘ r ∈ Q
    c₁ = qc₂ (pr₂ ∘ r) (n , (λ s → pr₂(prf s)))

\end{code}

Exponential of C-spaces

\begin{code}

infixr  _⇒_

_⇒_ : Space → Space → Space
X ⇒ Y = Map X Y , R , rc₀ , rc₁ , rc₂
 where
  R : Subset(₂ℕ → Map X Y)
  R r = ∀(p : ₂ℕ → U X) → p ∈ Probe X → ∀(t : ₂ℕ → ₂ℕ) → t ∈ C →
         (λ α → (pr₁ ∘ r)(t α)(p α)) ∈ Probe Y

  rc₀ : ∀(φ : Map X Y) → (λ α → φ) ∈ R
  rc₀ (φ , cφ) p pP t uc = cφ p pP

  rc₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(r : ₂ℕ → Map X Y) → r ∈ R → r ∘ t ∈ R
  rc₁ t uc r rR p pP t' uc' = rR p pP (t ∘ t') (Lemma[∘-UC] t uc t' uc')

  rc₂ : ∀(r : ₂ℕ → Map X Y) →
         (Σ \(n : ℕ) → ∀(s : ₂Fin n) → (r ∘ (cons s)) ∈ R) → r ∈ R
  rc₂ r (n , ps) p pP t uc = cond₂ Y (λ α → (pr₁ ∘ r)(t α)(p α)) (m , prf)
   where
    m : ℕ
    m = pr₁ (Theorem[Coverage-axiom] n t uc)
    prf : ∀(s : ₂Fin m) → (λ α → (pr₁ ∘ r)(t(cons s α))(p(cons s α))) ∈ Probe Y
    prf s = transport (λ x → (λ α → (pr₁ ∘ r)(x α)(p(cons s α))) ∈ Probe Y) eq 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 : cons s' ∘ t' ≡ t ∘ cons s 
      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
      claim : (λ α → (pr₁ ∘ r)(cons s' (t' α))(p(cons s α))) ∈ Probe Y
      claim = ps s' (p ∘ (cons s)) psinP t' uc'

\end{code}

Universal properties of products and of exponentials

\begin{code}

continuous-pair : (X Y Z : Space)
                → Map X Y → Map X Z → Map X (Y ⊗ Z)
continuous-pair X Y Z (f , cf) (g , cg) = (fg , cfg)
 where
  fg : U X → U (Y ⊗ Z)
  fg x = (f x , g x)
  cfg : continuous X (Y ⊗ Z) fg
  cfg p pX = cf p pX , cg p pX

cpr₁ : (X Y : Space) → Map (X ⊗ Y) X
cpr₁ X Y = pr₁ , (λ _ → pr₁)

cpr₂ : (X Y : Space) → Map (X ⊗ Y) Y
cpr₂ X Y = pr₂ , (λ _ → pr₂)

continuous-pr₁ : (X Y Z : Space) → Map X (Y ⊗ Z) → Map X Y
continuous-pr₁ X Y Z (w , cw) = pr₁ ∘ w , (λ p pX → pr₁ (cw p pX))

continuous-pr₂ : (X Y Z : Space) → Map X (Y ⊗ Z) → Map X Z
continuous-pr₂ X Y Z (w , cw) = pr₂ ∘ w , (λ p pX → pr₂ (cw p pX))

continuous-λ : (X Y Z : Space) → Map (X ⊗ Y) Z → Map X (Y ⇒ Z)
continuous-λ X Y Z (f , cf) = g , cg
 where
  g : U X → U(Y ⇒ Z)
  g x = h , ch
   where
    h : U Y → U Z
    h y = f(x , y)
    ch : continuous Y Z h
    ch q qY = cf r rXY
     where
      r : ₂ℕ → U X × U Y
      r α = (x , q α)
      rXY : r ∈ Probe (X ⊗ Y)
      rXY = cond₀ X x , qY
  cg : continuous X (Y ⇒ Z) g
  cg p pX q qY t uct = cf r rXY
   where
    r : ₂ℕ → U X × U Y
    r α = (p(t α) , q α)
    rXY : r ∈ Probe (X ⊗ Y)
    rXY = cond₁ X t uct p pX , qY

continuous-app : (X Y Z : Space) → Map X (Y ⇒ Z) → Map X Y → Map X Z
continuous-app X Y Z (f , cf) (a , ca) = (fa , cfa)
 where
  fa : U X → U Z
  fa x = pr₁ (f x) (a x)
  cfa : continuous X Z fa
  cfa p pX = cf p pX (a ∘ p) (ca p pX) id Lemma[id-UC]

\end{code}

Arbitrary product of C-spaces

\begin{code}

∏ : {I : Set} → (I → Space) → Space
∏ {I} X = A , P , c₀ , c₁ , c₂
 where
  A : Set
  A = (i : I) → U(X i)
  π : (i : I) → A → U(X i)
  π i a = a i

  P : Subset (₂ℕ → A)
  P p = ∀(i : I) → (π i) ∘ p ∈ Probe (X i)

  c₀ : ∀(a : A) → (λ α → a) ∈ P
  c₀ a i = cond₀ (X i) (a i)

  c₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → A) → p ∈ P → p ∘ t ∈ P
  c₁ t uc p pP i = cond₁ (X i) t uc ((π i) ∘ p) (pP i)

  c₂ : ∀(p : ₂ℕ → A) → (Σ \(n : ℕ) → ∀(s : ₂Fin n) → (p ∘ (cons s)) ∈ P) → p ∈ P
  c₂ p (n , pr) i = cond₂ (X i) ((π i) ∘ p) (n , λ s → pr s i)


continuous-π : {I : Set} → (X : I → Space) → (i : I) → Map (∏ X) (X i)
continuous-π {I} X i = π , cts
 where
  π : U(∏ X) → U(X i)
  π w = w i
  cts : continuous (∏ X) (X i) π
  cts p pX = pX i


universal-property-∏ :
    {I : Set} → ∀(X : I → Space) →
    ∀(Y : Space) → ∀(f : (i : I) → Map Y (X i)) →
    Σ \(g : Map Y (∏ X)) →
      ∀(i : I) → ∀(y : U Y) → pr₁(continuous-π X i)(pr₁ g y) ≡ pr₁ (f i) y
universal-property-∏ {I} X Y f = (g , cg) , (λ _ _ → refl)
 where
  g : U Y → U(∏ X)
  g y i = pr₁ (f i) y
  cg : continuous Y (∏ X) g
  cg q qY i = pr₂ (f i) q qY

\end{code}