Chuangjie Xu 2013 (updated in February 2015)

\begin{code}

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

module UsingIrrelevantFunext.Space.CartesianClosedness where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingIrrelevantFunext.Irrelevance
open import UsingIrrelevantFunext.Space.Coverage
open import UsingIrrelevantFunext.Space.Space
open import UsingIrrelevantFunext.IrrelevantFunext

\end{code}

The category of C-spaces is cartesian closed.

The terminal C-space:

\begin{code}

⒈Space : Space
⒈Space = ⒈ , P , c₀ , 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₂ _ _ = ⋆
  c₃ : ∀(p p' : ₂ℕ → ⒈) → p ∈ P → ((α : ₂ℕ) → [ p α ≡ 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₂ , pc₃) ⊗ (Y , Q , qc₀ , qc₁ , qc₂ , qc₃) =
                  X × Y , R , rc₀ , 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)))

  rc₃ : ∀(r r' : ₂ℕ → X × Y) → r ∈ R → (∀(α : ₂ℕ) → [ r α ≡ r' α ]) → r' ∈ R
  rc₃ r r' rR ex = c₀ , c₁
   where
    c₀ : pr₁ ∘ r' ∈ P
    c₀ = pc₃ (pr₁ ∘ r) (pr₁ ∘ r') (pr₁ rR) (λ α → [ap] pr₁ (ex α))
    c₁ : pr₂ ∘ r' ∈ Q
    c₁ = qc₃ (pr₂ ∘ r) (pr₂ ∘ r') (pr₂ rR) (λ α → [ap] pr₂ (ex α))

\end{code}

Exponential of C-spaces

\begin{code}

infixr  _⇒_

_⇒_ : Space → Space → Space
X ⇒ Y = Map X Y , R , rc₀ , 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 = cond₃ Y (λ α → (pr₁ ∘ r)(cons s' (t' α))(p(cons s α)))
                     (λ α → (pr₁ ∘ r)(t (cons s α))(p(cons s α)))
                     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)))
      [eq] : ∀(α : ₂ℕ) → [ cons s' (t' α) ≡ t(cons s α) ]
      [eq] α = [sym] (funext¹ (eq α))
                     ---------
      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'
      claim₁ : ∀(α : ₂ℕ) → [ (pr₁ ∘ r)(cons s' (t' α))(p(cons s α)) ≡
                             (pr₁ ∘ r)(t(cons s α))(p(cons s α)) ]
      claim₁ α = [ap] (λ x → (pr₁ ∘ r) x (p(cons s α))) ([eq] α)

  rc₃ : ∀(r r' : ₂ℕ → Map X Y) → r ∈ R → ((α : ₂ℕ) → [ r α ≡ r' α ]) → r' ∈ R
  rc₃ r r' rR ex p pP t uct = cond₃ Y (λ α → (pr₁ ∘ r)(t α)(p α))
                                      (λ α → (pr₁ ∘ r')(t α)(p α))
                                      (rR p pP t uct)
                                      (λ α → [fun-ap] ([ap] pr₁ (ex (t α))) (p α))

\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

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}