Chuangjie Xu 2012 (updated in February 2015, ported to TypeTopology in 2025)

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt using (naive-funext)

module C-Spaces.UsingFunExt.CartesianClosedness (fe : naive-funext 𝓀₀ 𝓀₀) where

open import C-Spaces.Preliminaries.Sequence
open import C-Spaces.UniformContinuity
open import C-Spaces.Coverage
open import C-Spaces.UsingFunExt.Space

\end{code}

The terminal C-space:

\begin{code}

πŸ™Space : Space
πŸ™Space = πŸ™ , P , cβ‚€ , c₁ , cβ‚‚
 where
  P : (β‚‚β„• β†’ πŸ™) β†’ Set
  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 = unique-to-πŸ™ , (Ξ» p _ β†’ ⋆)

\end{code}

Binary product of C-spaces:

\begin{code}

infixl 3 _βŠ—_

_βŠ—_ : Space β†’ Space β†’ Space
(X , P , pcβ‚€ , pc₁ , pcβ‚‚) βŠ— (Y , Q , qcβ‚€ , qc₁ , qcβ‚‚) = (X Γ— Y) , R , rcβ‚€ , rc₁ , rcβ‚‚
 where
  R : (β‚‚β„• β†’ X Γ— Y) β†’ Set
  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 3 _β‡’_

_β‡’_ : Space β†’ Space β†’ Space
X β‡’ Y = Map X Y , R , rcβ‚€ , rc₁ , rcβ‚‚
 where
  R : (β‚‚β„• β†’ Map X Y) β†’ Set
  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)))
      ex : βˆ€ Ξ± β†’ t (cons s Ξ±) ∼ cons s' (t' Ξ±)
      ex = prβ‚‚ (prβ‚‚ (prβ‚‚ (prβ‚‚ (Theorem[Coverage-axiom] n t uc) s)))
      eq : cons s' ∘ t' ＝ t ∘ cons s 
      eq = (fe (Ξ» Ξ± β†’ fe (ex Ξ±)))⁻¹
           ----      ----
      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 : (β‚‚β„• β†’ A) β†’ Set
  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}