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 3 _⊗_

_⊗_ : 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 3 _⇒_

_⇒_ : 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₀ (φ , ) p pP t uc =  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}