\begin{code}
module Space-exponential where
open import MiniLibrary
open import Sequence
open import UniformContinuity
open import Space
open import not-not
infixr 3 _⇒_
_⇒_ : Space → Space → Space
P ⇒ Q = Map P Q , R , rc₀ , rc₁ , rc₂ , rc₃
where
R : Subset(₂ℕ → Map P Q)
R r = ∀(p : ₂ℕ → U P) → p ∈ Probe P → ∀(t : ₂ℕ → ₂ℕ) → t ∈ C →
(λ α → (π₀ ∘ r)(t α)(p α)) ∈ Probe Q
rc₀ : ∀(r : ₂ℕ → Map P Q) → constant r → r ∈ R
rc₀ r cr p pP t uct = cond₃ Q ((π₀(r 0̄)) ∘ p) (λ α → (π₀ ∘ r)(t α)(p α)) claim₀ claim₁
where
claim₀ : (π₀(r 0̄)) ∘ p ∈ Probe Q
claim₀ = π₁(r 0̄) p pP
claim₁ : ∀(α : ₂ℕ) → [ π₀(r 0̄)(p α) ≡ (π₀ ∘ r) (t α) (p α) ]
claim₁ α = hide (fun-ap (ap π₀ (cr 0̄ (t α))) (p α))
rc₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(r : ₂ℕ → Map P Q) → 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 P Q) →
(∃ \(n : ℕ) → ∀(s : ₂Fin n) → (r ∘ (cons s)) ∈ R) → r ∈ R
rc₂ r ex p pP t uc = cond₂ Q (λ α → (π₀ ∘ r)(t α)(p α)) (∃-intro n' prf)
where
n : ℕ
n = ∃-witness ex
ps : ∀(s : ₂Fin n) → (r ∘ (cons s)) ∈ R
ps = ∃-elim ex
n' : ℕ
n' = ∃-witness (Axiom[coverage] n t uc)
prf : ∀(s' : ₂Fin n') → (λ α → (π₀ ∘ r)(t(cons s' α))(p(cons s' α))) ∈ Probe Q
prf s' = cond₃ Q (λ α → (π₀ ∘ r)(cons s'' (t'' α))(p(cons s' α)))
(λ α → (π₀ ∘ r)(t (cons s' α))(p(cons s' α)))
claim₀ claim₁
where
s'' : ₂Fin n
s'' = ∃-witness (∃-elim (Axiom[coverage] n t uc) s')
t'' : ₂ℕ → ₂ℕ
t'' = ∃-witness (∃-elim (∃-elim (Axiom[coverage] n t uc) s'))
uct'' : t'' ∈ C
uct'' = ∧-elim₀ (∃-elim (∃-elim (∃-elim (Axiom[coverage] n t uc) s')))
eq : [ t ∘ (cons s') ≡ (cons s'') ∘ t'' ]
eq = ∧-elim₁ (∃-elim (∃-elim (∃-elim (Axiom[coverage] n t uc) s')))
ps'inP : (p ∘ (cons s')) ∈ Probe P
ps'inP = cond₁ P (cons s') (Lemma[cons-UC] s') p pP
claim₀ : (λ α → (π₀ ∘ r)(cons s'' (t'' α))(p(cons s' α))) ∈ Probe Q
claim₀ = ps s'' (p ∘ (cons s')) ps'inP t'' uct''
claim₁ : ∀(α : ₂ℕ) → [ (π₀ ∘ r)(cons s'' (t'' α))(p(cons s' α)) ≡
(π₀ ∘ r)(t(cons s' α))(p(cons s' α)) ]
claim₁ α = [ap] (λ x → (π₀ ∘ r)(x α)(p(cons s' α))) ([sym] eq)
rc₃ : ∀(r r' : ₂ℕ → Map P Q) → r ∈ R → ((α : ₂ℕ) → [ r α ≡ r' α ]) → r' ∈ R
rc₃ r r' rR ex p pP t uct = cond₃ Q (λ α → (π₀ ∘ r)(t α)(p α))
(λ α → (π₀ ∘ r')(t α)(p α))
(rR p pP t uct)
(λ α → [fun-ap] ([ap] π₀ (ex (t α))) (p α))
\end{code}