Chuangjie Xu 2013 (updated in February 2015)

\begin{code}

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

module UsingNotNotFunext.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 UsingNotNotFunext.NotNot
open import UsingNotNotFunext.NotNotFunext
open import UsingNotNotFunext.Space.Coverage
open import UsingNotNotFunext.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₂ , 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 _ _ 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 _ _ (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

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₂ , 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)

  c₃ : ∀(p p' : ₂ℕ → A) → p ∈ P → (∀ α → ¬¬ p α ≡ p' α) → p' ∈ P
  c₃ p p' pP e i = cond₃ (X i) _ _ (pP i) (λ α → ¬¬ap (π i) (e α))


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}