Chuangjie Xu 2012 (updated in February 2015)

\begin{code}

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

module UsingSetoid.Space.CartesianClosedness where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingSetoid.Setoid
open import UsingSetoid.Space.Coverage
open import UsingSetoid.Space.Space

\end{code}

The category of C-spaces is cartesian closed.

The terminal C-space:

\begin{code}

⒈Space : Space
⒈Space = E⒈ , P , c₀ , c₁ , c₂ , c₃
 where
  P : Subset (E-map-₂ℕ E⒈)
  P p = ⒈
  c₀ : ∀(x : ⒈) → E-λα E⒈ x ∈ P
  c₀ _ = ⋆
  c₁ : ∀ t → t ∈ C → ∀ p → p ∈ P → ⟨ E⒈ ⟩ p ◎ t ∈ P
  c₁ _ _ _ _ = ⋆
  c₂ : ∀ p → (Σ \(n : ℕ) → ∀(s : ₂Fin n) → ⟨ E⒈ ⟩ p ◎ Cons s ∈ P) → p ∈ P
  c₂ _ _ = ⋆
  c₃ : ∀ p q → p ∈ P → (∀ α → pr₁ p α ≡ pr₁ q α) → q ∈ P
  c₃ _ _ _ _ = ⋆

continuous-unit : (A : Space) → Map A ⒈Space
continuous-unit A = E-unit {U A} , (λ 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
  epr₁ : E-map (X ✻ Y) X
  epr₁ = E-pr₁ X Y
  epr₂ : E-map (X ✻ Y) Y
  epr₂ = E-pr₂ X Y

  R : Subset (E-map-₂ℕ (X ✻ Y))
  R r = (⟨ X ✻ Y ∣ X ⟩ epr₁ ◎ r ∈ P) × (⟨ X ✻ Y ∣ Y ⟩ epr₂ ◎ r ∈ Q)

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

  rc₁ : ∀ t → t ∈ C → ∀ r → r ∈ R → ⟨ X ✻ Y ⟩ r ◎ t ∈ R
  rc₁ t uc r (rP , rQ) = c₀ , c₁
   where
    c₀ : ⟨ X ✻ Y ∣ X ⟩ epr₁ ◎ ⟨ X ✻ Y ⟩ r ◎ t ∈ P
    c₀ = pc₁ t uc _ rP
    c₁ : ⟨ X ✻ Y ∣ Y ⟩ epr₂ ◎ ⟨ X ✻ Y ⟩ r ◎ t ∈ Q
    c₁ = qc₁ t uc _ rQ

  rc₂ : ∀ r → (Σ \(n : ℕ) → ∀(s : ₂Fin n) → ⟨ X ✻ Y ⟩ r ◎ Cons s ∈ R) → r ∈ R
  rc₂ r (n , prf) = c₀ , c₁
   where
    c₀ : ⟨ X ✻ Y ∣ X ⟩ epr₁ ◎ r ∈ P
    c₀ = pc₂ _ (n , pr₁ ∘ prf)
    c₁ : ⟨ X ✻ Y ∣ Y ⟩ epr₂ ◎ r ∈ Q
    c₁ = qc₂ _ (n , pr₂ ∘ prf)

  rc₃ : ∀ r r' → r ∈ R → (∀ α → E (X ✻ Y) (pr₁ r α) (pr₁ r' α)) → r' ∈ R
  rc₃ r r' (rP , rQ) ex = c₀ , c₁
   where
    c₀ : ⟨ X ✻ Y ∣ X ⟩ epr₁ ◎ r' ∈ P
    c₀ = pc₃ _ _ rP (pr₁ ∘ ex)
    c₁ : ⟨ X ✻ Y ∣ Y ⟩ epr₂ ◎ r' ∈ Q
    c₁ = qc₃ _ _ rQ (pr₂ ∘ ex)

\end{code}

Exponential of C-spaces

\begin{code}

MapSetoid : Space → Space → Setoid
MapSetoid X Y = Map X Y , _≋_ , rc , sc , tc
 where
  _≈_ : G Y → G Y → Set
  _≈_ = E (U Y)
  _≋_ : Map X Y → Map X Y → Set
  ((f , _) , _) ≋ ((g , _) , _) = ∀ x → f x ≈ g x
  rc : ∀ f → f ≋ f
  rc ((f , _) , _) = λ x → Refl (U Y) (f x)
  sc : ∀ f g → f ≋ g → g ≋ f
  sc ((f , _) , _) ((g , _) , _) e = λ x → Sym (U Y) _ _ (e x)
  tc : ∀ f₀ f₁ f₂ → f₀ ≋ f₁ → f₁ ≋ f₂ → f₀ ≋ f₂
  tc ((f₀ , _) , _) ((f₁ , _) , _) ((f₂ , _) , _) e e' =
      λ x → Trans (U Y) _ _ _ (e x) (e' x)

Exp : (X Y : Space) →
      E-map-₂ℕ (MapSetoid X Y) → E-map-₂ℕ-₂ℕ → E-map-₂ℕ (U X)
    → E-map-₂ℕ (U Y)
Exp (X , _) (Y , _) (r , er) (t , et) (p , ep) = (q , eq)
 where
  _≈_ : U Y → U Y → Set
  _≈_ = E Y
  q : ₂ℕ → U Y
  q α = pr₁ (pr₁ (r (t α))) (p α)
  eq : ∀ α β → α ≣ β → q α ≈ q β
  eq α β e = Trans Y _ _ _ claim₀ claim₁
   where
    claim₀ : pr₁ (pr₁ (r (t α))) (p α) ≈ pr₁ (pr₁ (r (t β))) (p α)
    claim₀ = er (t α) (t β) (et α β e) (p α)
    claim₁ : pr₁ (pr₁ (r (t β))) (p α) ≈ pr₁ (pr₁ (r (t β))) (p β)
    claim₁ = pr₂ (pr₁ (r (t β))) (p α) (p β) (ep α β e)


infixr  _⇒_

_⇒_ : Space → Space → Space
X ⇒ Y = MapSetoid X Y , R , rc₀ , rc₁ , rc₂ , rc₃
 where
  _≈_ : G Y → G Y → Set
  _≈_ = E (U Y)
  _≋_ : Map X Y → Map X Y → Set
  _≋_ = E (MapSetoid X Y)
  exp : E-map-₂ℕ (MapSetoid X Y) → E-map-₂ℕ-₂ℕ → E-map-₂ℕ (U X)
      → E-map-₂ℕ (U Y)
  exp = Exp X Y

  R : Subset (E-map-₂ℕ (MapSetoid X Y))
  R r = ∀ p → p ∈ Probe X → ∀ t → t ∈ C → exp r t p ∈ Probe Y

  rc₀ : ∀ φ → E-λα (MapSetoid X Y) φ ∈ R
  rc₀ (φ , cφ) p pX t uc = cond₃ Y _ _ (cφ p pX) (λ α → Refl (U Y) _)

  rc₁ : ∀ t → t ∈ C → ∀ r → r ∈ R → ⟨ MapSetoid X Y ⟩ r ◎ t ∈ R
  rc₁ t uc r rR p pX t' uc' = rR p pX (t ◎ t') (Lemma[◎-UC] t uc t' uc')


  rc₂ : ∀ r → (Σ \(n : ℕ) → ∀(s : ₂Fin n) → ⟨ MapSetoid X Y ⟩ r ◎ Cons s ∈ R) → r ∈ R
  rc₂ r (n , ps) p pX t uc = cond₂ Y _ (m , prf)
   where
    m : ℕ
    m = pr₁ (Theorem[Coverage-axiom] n t uc)
    prf : ∀(s : ₂Fin m) → ⟨ U Y ⟩ exp r t 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' : E-map-₂ℕ-₂ℕ
      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)))
      claim₀ : ∀ α → cons s' (pr₁ t' α) ≣ pr₁ t (cons s α)
      claim₀ α i = (pr₂ (pr₂ (pr₂ (pr₂ (Theorem[Coverage-axiom] n t uc) s))) α i)⁻¹
      claim₁ : ∀ α → pr₁ r (cons s' (pr₁ t' α)) ≋ pr₁ r (pr₁ t (cons s α))
      claim₁ α = pr₂ r _ _ (claim₀ α)
      claim₂ : ∀ α →   pr₁ (pr₁ (pr₁ r (cons s' (pr₁ t' α)))) (pr₁ p (cons s α))
                     ≈ pr₁ (pr₁ (pr₁ r (pr₁ t (cons s α)))) (pr₁ p (cons s α))
      claim₂ α = claim₁ α (pr₁ p (cons s α))
      claim₃ : ⟨ U X ⟩ p ◎ Cons s ∈ Probe X
      claim₃ = cond₁ X (Cons s) (Lemma[cons-UC] s) p pX
      claim₄ : exp (⟨ MapSetoid X Y ⟩ r ◎ Cons s') t' (⟨ U X ⟩ p ◎ Cons s) ∈ Probe Y
      claim₄ = ps s' _ claim₃ t' uc'

  rc₃ : ∀ r r' → r ∈ R → (∀ α → E (MapSetoid X Y) (pr₁ r α) (pr₁ r' α)) → r' ∈ R
  rc₃ r r' rR ex p pX t tC = cond₃ Y _ _ (rR p pX t tC) (λ α → ex (pr₁ t α) (pr₁ p α))


continuous-λ : (X Y Z : Space) → Map (X ⊗ Y) Z → Map X (Y ⇒ Z)
continuous-λ X Y Z ((f , ef) , cf) = (g , eg) , cg
 where
  _~_ = E (U X)
  _≈_ = E (U Y)
  _≋_ = E (U Z)
  g : G X → G(Y ⇒ Z)
  g x = (h , eh) , ch
   where
    h : G Y → G Z
    h y = f(x , y)
    eh : ∀ y y' → y ≈ y' → h y ≋ h y'
    eh y y' ey = ef _ _ (Refl (U X) x , ey)
    ch : continuous Y Z (h , eh)
    ch (q , eq) qY = cf (r , er) rXY
     where
      r : ₂ℕ → G X × G Y
      r α = (x , q α)
      er : ∀ α α' → α ≣ α' → (x ~ x) × (q α ≈ q α')
      er α α' eα = Refl (U X) x , eq α α' eα
      rXY : (r , er) ∈ Probe (X ⊗ Y)
      rXY = cond₀ X x , qY
  eg : ∀ x x' → x ~ x' → ∀ y → f (x , y) ≋ f (x' , y)
  eg x x' ex y = ef _ _ (ex , Refl (U Y) y)
  cg : continuous X (Y ⇒ Z) (g , eg)
  cg (p , ep) pX (q , eq) qY (t , et) uc = cond₃ Z _ _ claim (λ α → Refl (U Z) _)
   where
    r : ₂ℕ → G X × G Y
    r α = (p(t α) , q α)
    er : ∀ α α' → α ≣ α' → (p(t α) ~ p(t α')) × (q α ≈ q α')
    er α α' eα = ep _ _ (et _ _ eα) , eq _ _ eα
    rXY : (r , er) ∈ Probe (X ⊗ Y)
    rXY = cond₁ X (t , et) uc (p , ep) pX , qY
    claim : ⟨ U X ✻ U Y ∣ U Z ⟩ (f , ef) ◎ (r , er) ∈ Probe Z
    claim = cf (r , er) rXY

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
  _~_ = E (U X)
  _≈_ = E (U Z)
  fa : G X → G Z
  fa x = pr₁ (pr₁ (pr₁ f x)) (pr₁ a x)
  efa : ∀ x x' → x ~ x' → fa x ≈ fa x'
  efa x x' ex = Trans (U Z) _ _ _ claim₀ claim₁
   where
    claim₀ : fa x ≈ pr₁ (pr₁ (pr₁ f x')) (pr₁ a x)
    claim₀ = pr₂ f x x' ex (pr₁ a x)
    claim₁ : pr₁ (pr₁ (pr₁ f x')) (pr₁ a x) ≈ fa x'
    claim₁ = pr₂ (pr₁ (pr₁ f x')) (pr₁ a x) (pr₁ a x') (pr₂ a x x' ex)
  FA : E-map (U X) (U Z)
  FA = (fa , efa)
  cfa : continuous X Z FA
  cfa p pX = cf p pX (⟨ U X ∣ U Y ⟩ a ◎ p) (ca p pX) (E-id E₂ℕ) Lemma[id-UC]

\end{code}