\begin{code}
module Space-product where
open import MiniLibrary
open import Sequence
open import UniformContinuity
open import Space
open import not-not
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 = ((π₀ ∘ r) ∈ P) ∧ ((π₁ ∘ r) ∈ Q)
rc₀ : ∀(r : ₂ℕ → X × Y) → constant r → r ∈ R
rc₀ r cr = ∧-intro c₀ c₁
where
c₀ : π₀ ∘ r ∈ P
c₀ = pc₀ (π₀ ∘ r) (λ α β → ap π₀ (cr α β))
c₁ : π₁ ∘ r ∈ Q
c₁ = qc₀ (π₁ ∘ r) (λ α β → ap π₁ (cr α β))
rc₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(r : ₂ℕ → X × Y) → r ∈ R → r ∘ t ∈ R
rc₁ t uc r rR = ∧-intro c₀ c₁
where
c₀ : π₀ ∘ (r ∘ t) ∈ P
c₀ = pc₁ t uc (π₀ ∘ r) (∧-elim₀ rR)
c₁ : π₁ ∘ (r ∘ t) ∈ Q
c₁ = qc₁ t uc (π₁ ∘ r) (∧-elim₁ rR)
rc₂ : ∀(r : ₂ℕ → X × Y) → (∃ \(n : ℕ) → ∀(s : ₂Fin n) → (r ∘ (cons s)) ∈ R) → r ∈ R
rc₂ r ex = ∧-intro c₀ c₁
where
n : ℕ
n = ∃-witness ex
prf : ∀(s : ₂Fin n) → (r ∘ (cons s)) ∈ R
prf = ∃-elim ex
c₀ : π₀ ∘ r ∈ P
c₀ = pc₂ (π₀ ∘ r) (∃-intro n (λ s → ∧-elim₀(prf s)))
c₁ : π₁ ∘ r ∈ Q
c₁ = qc₂ (π₁ ∘ r) (∃-intro n (λ s → ∧-elim₁(prf s)))
rc₃ : ∀(r r' : ₂ℕ → X × Y) → r ∈ R → (∀(α : ₂ℕ) → [ r α ≡ r' α ]) → r' ∈ R
rc₃ r r' rR ex = ∧-intro c₀ c₁
where
c₀ : π₀ ∘ r' ∈ P
c₀ = pc₃ (π₀ ∘ r) (π₀ ∘ r') (∧-elim₀ rR) (λ α → [ap] π₀ (ex α))
c₁ : π₁ ∘ r' ∈ Q
c₁ = qc₃ (π₁ ∘ r) (π₁ ∘ r') (∧-elim₁ rR) (λ α → [ap] π₁ (ex α))
continuous-π₀ : {A B : Space} →
Σ \(p : U (A ⊗ B) → U A) → continuous {A ⊗ B} {A} p
continuous-π₀ {A} {B} = π₀ , λ p pr → ∧-elim₀ pr
continuous-π₁ : {A B : Space} →
Σ \(p : U (A ⊗ B) → U B) → continuous {A ⊗ B} {B} p
continuous-π₁ {A} {B} = π₁ , λ p pr → ∧-elim₁ pr
\end{code}