\begin{code}
module Space-coproduct where
open import MiniLibrary
open import Sequence
open import UniformContinuity
open import Space
open import Space-exponential
open import not-not
open import not-not-funext
open import Inequality
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 = ∃ \(n : ℕ) → ∀(s : ₂Fin n) →
(∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₀(p α) ]))
∨ (∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₁(q α) ]))
rc₀ : ∀(r : ₂ℕ → X ⊎ Y) → constant r → r ∈ R
rc₀ r cr = ∃-intro 0 prf
where
c₀ : (∃ \(x : X) → r 0̄ ≡ in₀ x) →
∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r(cons ⟨⟩ α) ≡ in₀(p α) ])
c₀ (x , e) = ∃-intro (λ α → x) (∧-intro (pc₀ (λ α → x) (λ _ _ → refl)) (λ α → hide (trans (cr α 0̄) e)))
c₁ : (∃ \(y : Y) → r 0̄ ≡ in₁ y) →
∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r(cons ⟨⟩ α) ≡ in₁(q α) ])
c₁ (y , e) = ∃-intro (λ α → y) (∧-intro (qc₀ (λ α → y) (λ _ _ → refl)) (λ α → hide (trans (cr α 0̄) e)))
prf : ∀(s : ₂Fin 0) → (∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₀(p α) ]))
∨ (∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₁(q α) ]))
prf ⟨⟩ = cases c₀ c₁ (Lemma[⊎] (r 0̄))
rc₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(r : ₂ℕ → X ⊎ Y) → r ∈ R → r ∘ t ∈ R
rc₁ t uc r (m , pr) = ∃-intro n prf
where
n : ℕ
n = ∃-witness (uc m)
prf : ∀(s : ₂Fin n) → (∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r(t(cons s α)) ≡ in₀(p α) ]))
∨ (∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r(t(cons s α)) ≡ in₁(q α) ]))
prf s = cases c₀ c₁ (pr s')
where
s' : ₂Fin m
s' = ∃-witness (∃-elim (Axiom[coverage] m t uc) s)
t' : ₂ℕ → ₂ℕ
t' = ∃-witness (∃-elim (∃-elim (Axiom[coverage] m t uc) s))
uc' : t' ∈ C
uc' = ∧-elim₀ (∃-elim (∃-elim (∃-elim (Axiom[coverage] m t uc) s)))
[eq] : [ t ∘ (cons s) ≡ (cons s') ∘ t' ]
[eq] = ∧-elim₁ (∃-elim (∃-elim (∃-elim (Axiom[coverage] m t uc) s)))
[eqtα] : ∀(α : ₂ℕ) → [ r(t(cons s α)) ≡ r(cons s' (t' α)) ]
[eqtα] α = [ap] r ([fun-ap] [eq] α)
c₀ : (∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r(cons s' α) ≡ in₀(p α) ])) →
∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r(t(cons s α)) ≡ in₀(p α) ])
c₀ (p , pP , [eα]) = ∃-intro (p ∘ t') (∧-intro (pc₁ t' uc' p pP) [eα]')
where
[eα]' : ∀(α : ₂ℕ) → [ r(t(cons s α)) ≡ in₀(p(t' α)) ]
[eα]' α = [trans] ([eqtα] α) ([eα] (t' α))
c₁ : (∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r(cons s' α) ≡ in₁(q α) ])) →
∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r(t(cons s α)) ≡ in₁(q α) ])
c₁ (q , qQ , [eα]) = ∃-intro (q ∘ t') (∧-intro (qc₁ t' uc' q qQ) [eα]')
where
[eα]' : ∀(α : ₂ℕ) → [ r(t(cons s α)) ≡ in₁(q(t' α)) ]
[eα]' α = [trans] ([eqtα] α) ([eα] (t' α))
rc₂ : ∀(r : ₂ℕ → X ⊎ Y) → (∃ \(n : ℕ) → ∀(s : ₂Fin n) → (r ∘ (cons s)) ∈ R) → r ∈ R
rc₂ r (n , pr) = ∃-intro (k + n) prf
where
k : ℕ
k = ∃-witness (max-fin (λ s → ∃-witness (pr s)))
k-max : ∀(s : ₂Fin n) → ∃-witness (pr s) ≤ k
k-max = ∃-elim (max-fin (λ s → ∃-witness (pr s)))
prf : ∀(s : ₂Fin (k + n)) → (∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₀(p α) ]))
∨ (∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₁(q α) ]))
prf s = cases c₀ c₁ (∃-elim (pr s₀) s₁)
where
s₀ : ₂Fin n
s₀ = Vtake k n s
l : ℕ
l = ∃-witness (pr s₀)
l≤k : l ≤ k
l≤k = k-max s₀
m : ℕ
m = ∃-witness (Lemma[≤-∃] l k l≤k)
k=m+l : k ≡ m + l
k=m+l = trans (sym (∃-elim (Lemma[≤-∃] l k l≤k))) (Lemma[n+m=m+n] l m)
s₁ : ₂Fin l
s₁ = Vtake m l (transport {ℕ} {₂Fin} k=m+l (Vdrop k n s))
s₂ : ₂Fin m
s₂ = Vdrop m l (transport {ℕ} {₂Fin} k=m+l (Vdrop k n s))
lemma : ∀(α : ₂ℕ) → [ cons s α ≡ cons s₀ (cons s₁ (cons s₂ α)) ]
lemma α = funext¹ (λ i → sym (Lemma[cons-Vtake-Vdrop]² n m l k k=m+l s α i))
c₀ : (∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r(cons s₀ (cons s₁ α)) ≡ in₀(p α) ])) →
∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₀(p α) ])
c₀ (p , pP , [e]) = ∃-intro ps₂ (∧-intro ps₂P [e]')
where
ps₂ : ₂ℕ → X
ps₂ = p ∘ (cons s₂)
ps₂P : ps₂ ∈ P
ps₂P = pc₁ (cons s₂) (Lemma[cons-UC] s₂) p pP
[e]' : ∀(α : ₂ℕ) → [ r(cons s α) ≡ in₀(p(cons s₂ α)) ]
[e]' α = [trans] ([ap] r (lemma α)) ([e] (cons s₂ α))
c₁ : (∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r(cons s₀ (cons s₁ α)) ≡ in₁(q α) ])) →
∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₁(q α) ])
c₁ (q , qQ , [e]) = ∃-intro qs₂ (∧-intro qs₂Q [e]')
where
qs₂ : ₂ℕ → Y
qs₂ = q ∘ (cons s₂)
qs₂Q : qs₂ ∈ Q
qs₂Q = qc₁ (cons s₂) (Lemma[cons-UC] s₂) q qQ
[e]' : ∀(α : ₂ℕ) → [ r(cons s α) ≡ in₁(q(cons s₂ α)) ]
[e]' α = [trans] ([ap] r (lemma α)) ([e] (cons s₂ α))
rc₃ : ∀(r r' : ₂ℕ → X ⊎ Y) → r ∈ R → (∀(α : ₂ℕ) → [ r α ≡ r' α ]) → r' ∈ R
rc₃ r r' (n , pr) [eα] = ∃-intro n prf
where
prf : ∀(s : ₂Fin n) → (∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r'(cons s α) ≡ in₀(p α) ]))
∨ (∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r'(cons s α) ≡ in₁(q α) ]))
prf s = cases c₀ c₁ (pr s)
where
c₀ : (∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₀(p α) ])) →
∃ \(p : ₂ℕ → X) → (p ∈ P) ∧ (∀(α : ₂ℕ) → [ r'(cons s α) ≡ in₀(p α) ])
c₀ (p , pP , [e]) = ∃-intro p (∧-intro pP (λ α → [trans] ([sym]([eα](cons s α))) ([e] α)))
c₁ : (∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₁(q α) ])) →
∃ \(q : ₂ℕ → Y) → (q ∈ Q) ∧ (∀(α : ₂ℕ) → [ r'(cons s α) ≡ in₁(q α) ])
c₁ (q , qQ , [e]) = ∃-intro q (∧-intro qQ (λ α → [trans] ([sym]([eα](cons s α))) ([e] α)))
continuous-in₀ : {X Y : Space} →
Σ \(i : U X → U (X ⊕ Y)) → continuous {X} {X ⊕ Y} i
continuous-in₀ {X} {Y} = in₀ , cts
where
cts : ∀(r : ₂ℕ → U X) → r ∈ Probe X → in₀ ∘ r ∈ Probe (X ⊕ Y)
cts r rP = ∃-intro 0 prf
where
prf : ∀(s : ₂Fin 0) →
(∃ \(p : ₂ℕ → U X) → (p ∈ Probe X) ∧ (∀(α : ₂ℕ) → [ in₀(r(cons s α)) ≡ in₀(p α) ]))
∨ (∃ \(q : ₂ℕ → U Y) → (q ∈ Probe Y) ∧ (∀(α : ₂ℕ) → [ in₀(r(cons s α)) ≡ in₁(q α) ]))
prf ⟨⟩ = in₀ (∃-intro r (∧-intro rP (λ α → [refl])))
continuous-in₁ : {X Y : Space} →
Σ \(i : U Y → U (X ⊕ Y)) → continuous {Y} {X ⊕ Y} i
continuous-in₁ {X} {Y} = in₁ , cts
where
cts : ∀(r : ₂ℕ → U Y) → r ∈ Probe Y → in₁ ∘ r ∈ Probe (X ⊕ Y)
cts r rQ = ∃-intro 0 prf
where
prf : ∀(s : ₂Fin 0) →
(∃ \(p : ₂ℕ → U X) → (p ∈ Probe X) ∧ (∀(α : ₂ℕ) → [ in₁(r(cons s α)) ≡ in₀(p α) ]))
∨ (∃ \(q : ₂ℕ → U Y) → (q ∈ Probe Y) ∧ (∀(α : ₂ℕ) → [ in₁(r(cons s α)) ≡ in₁(q α) ]))
prf ⟨⟩ = in₁ (∃-intro r (∧-intro rQ (λ α → [refl])))
continuous-case : {X Y Z : Space} →
Σ \(c : U(X ⇒ Z) → U((Y ⇒ Z) ⇒ (X ⊕ Y) ⇒ Z)) →
continuous {X ⇒ Z} {(Y ⇒ Z) ⇒ (X ⊕ Y) ⇒ Z} c
continuous-case {X} {Y} {Z} = c , cts
where
c : U(X ⇒ Z) → U((Y ⇒ Z) ⇒ (X ⊕ Y) ⇒ Z)
c (f₀ , cf₀) = case-f₀ , ccf₀
where
case-f₀ : U(Y ⇒ Z) → U((X ⊕ Y) ⇒ Z)
case-f₀ (f₁ , cf₁) = case-f₀-f₁ , ccf₀f₁
where
case-f₀-f₁ : U(X ⊕ Y) → U Z
case-f₀-f₁ (in₀ x) = f₀ x
case-f₀-f₁ (in₁ y) = f₁ y
ccf₀f₁ : continuous {X ⊕ Y} {Z} case-f₀-f₁
ccf₀f₁ r (n , pr) = cond₂ Z (case-f₀-f₁ ∘ r) (n , prf)
where
prf : ∀(s : ₂Fin n) → case-f₀-f₁ ∘ r ∘ (cons s) ∈ Probe Z
prf s = case claim₀ claim₁ (pr s)
where
claim₀ : (∃ \(p : ₂ℕ → U X) → (p ∈ Probe X) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₀(p α) ])) →
case-f₀-f₁ ∘ r ∘ (cons s) ∈ Probe Z
claim₀ (p , pX , e) = cond₃ Z (f₀ ∘ p) (case-f₀-f₁ ∘ r ∘ (cons s)) (cf₀ p pX) ex
where
ex₀ : ∀(α : ₂ℕ) → [ f₀(p α) ≡ case-f₀-f₁(in₀(p α)) ]
ex₀ α = [refl]
ex₁ : ∀(α : ₂ℕ) → [ case-f₀-f₁(in₀(p α)) ≡ case-f₀-f₁(r(cons s α)) ]
ex₁ α = [ap] case-f₀-f₁ ([sym](e α))
ex : ∀(α : ₂ℕ) → [ f₀(p α) ≡ case-f₀-f₁(r(cons s α)) ]
ex α = [trans] (ex₀ α) (ex₁ α)
claim₁ : (∃ \(q : ₂ℕ → U Y) → (q ∈ Probe Y) ∧ (∀(α : ₂ℕ) → [ r(cons s α) ≡ in₁(q α) ])) →
case-f₀-f₁ ∘ r ∘ (cons s) ∈ Probe Z
claim₁ (q , qY , e) = cond₃ Z (f₁ ∘ q) (case-f₀-f₁ ∘ r ∘ (cons s)) (cf₁ q qY) ex
where
ex₀ : ∀(α : ₂ℕ) → [ f₁(q α) ≡ case-f₀-f₁(in₁(q α)) ]
ex₀ α = [refl]
ex₁ : ∀(α : ₂ℕ) → [ case-f₀-f₁(in₁(q α)) ≡ case-f₀-f₁(r(cons s α)) ]
ex₁ α = [ap] case-f₀-f₁ ([sym](e α))
ex : ∀(α : ₂ℕ) → [ f₁(q α) ≡ case-f₀-f₁(r(cons s α)) ]
ex α = [trans] (ex₀ α) (ex₁ α)
ccf₀ : continuous {Y ⇒ Z} {(X ⊕ Y) ⇒ Z} case-f₀
ccf₀ r rYZ u (n , pr) t uc = cond₂ Z (λ α → π₀(case-f₀(r(t α)))(u α)) (n , prf)
where
prf : ∀(s : ₂Fin n) → (λ α → π₀(case-f₀(r(t(cons s α))))(u(cons s α))) ∈ Probe Z
prf s = case claim₀ claim₁ (pr s)
where
claim₀ : (∃ \(p : ₂ℕ → U X) → (p ∈ Probe X) ∧ (∀(α : ₂ℕ) → [ u(cons s α) ≡ in₀(p α) ])) →
(λ α → π₀(case-f₀(r(t(cons s α))))(u(cons s α))) ∈ Probe Z
claim₀ (p , pX , e) = cond₃ Z (f₀ ∘ p) (λ α → π₀(case-f₀(r(t(cons s α))))(u(cons s α))) (cf₀ p pX) ex
where
ex₀ : ∀(α : ₂ℕ) → [ f₀(p α) ≡ π₀(case-f₀(r(t(cons s α))))(in₀(p α)) ]
ex₀ α = [refl]
ex₁ : ∀(α : ₂ℕ) → [ π₀(case-f₀(r(t(cons s α))))(in₀(p α)) ≡ π₀(case-f₀(r(t(cons s α))))(u(cons s α)) ]
ex₁ α = [ap] (π₀(case-f₀(r(t(cons s α))))) ([sym](e α))
ex : ∀(α : ₂ℕ) → [ f₀(p α) ≡ π₀(case-f₀(r(t(cons s α))))(u(cons s α)) ]
ex α = [trans] (ex₀ α) (ex₁ α)
claim₁ : (∃ \(q : ₂ℕ → U Y) → (q ∈ Probe Y) ∧ (∀(α : ₂ℕ) → [ u(cons s α) ≡ in₁(q α) ])) →
(λ α → π₀(case-f₀(r(t(cons s α))))(u(cons s α))) ∈ Probe Z
claim₁ (q , qY , e) = cond₃ Z (λ α → π₀(r(t(cons s α)))(q α))
(λ α → π₀(case-f₀(r(t(cons s α))))(u(cons s α)))
rtsqZ ex
where
rtsqZ : (λ α → π₀(r(t(cons s α)))(q α)) ∈ Probe Z
rtsqZ = rYZ q qY (t ∘ (cons s)) (Lemma[∘-UC] t uc (cons s) (Lemma[cons-UC] s))
ex₀ : ∀(α : ₂ℕ) → [ π₀(r(t(cons s α)))(q α) ≡ π₀(case-f₀(r(t(cons s α))))(in₁(q α)) ]
ex₀ α = [refl]
ex₁ : ∀(α : ₂ℕ) → [ π₀(case-f₀(r(t(cons s α))))(in₁(q α)) ≡ π₀(case-f₀(r(t(cons s α))))(u(cons s α)) ]
ex₁ α = [ap] (π₀(case-f₀(r(t(cons s α))))) ([sym](e α))
ex : ∀(α : ₂ℕ) → [ π₀(r(t(cons s α)))(q α) ≡ π₀(case-f₀(r(t(cons s α))))(u(cons s α)) ]
ex α = [trans] (ex₀ α) (ex₁ α)
cts : continuous {X ⇒ Z} {(Y ⇒ Z) ⇒ (X ⊕ Y) ⇒ Z} c
cts u uXZ v vYZ t uct w (n , pr) r ucr = cond₂ Z (λ α → π₀(π₀(c(u(t(r α))))(v(r α)))(w α)) (n , prf)
where
prf : ∀(s : ₂Fin n) → (λ α → π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(w(cons s α))) ∈ Probe Z
prf s = case claim₀ claim₁ (pr s)
where
claim₀ : (∃ \(p : ₂ℕ → U X) → (p ∈ Probe X) ∧ (∀(α : ₂ℕ) → [ w(cons s α) ≡ in₀(p α) ])) →
(λ α → π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(w(cons s α))) ∈ Probe Z
claim₀ (p , pX , e) = cond₃ Z (λ α → π₀(u(t(r(cons s α))))(p α))
(λ α → π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(w(cons s α)))
utrspZ ex
where
uctrs : (t ∘ r ∘ (cons s)) ∈ C
uctrs = Lemma[∘-UC] (t ∘ r) (Lemma[∘-UC] t uct r ucr) (cons s) (Lemma[cons-UC] s)
utrspZ : (λ α → π₀(u(t(r(cons s α))))(p α)) ∈ Probe Z
utrspZ = uXZ p pX (t ∘ r ∘ (cons s)) uctrs
ex₀ : ∀(α : ₂ℕ) → [ π₀(u(t(r(cons s α))))(p α)
≡ π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(in₀(p α)) ]
ex₀ α = [refl]
ex₁ : ∀(α : ₂ℕ) → [ π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(in₀(p α))
≡ π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(w(cons s α)) ]
ex₁ α = [ap] (π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))) ([sym](e α))
ex : ∀(α : ₂ℕ) → [ π₀(u(t(r(cons s α))))(p α)
≡ π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(w(cons s α)) ]
ex α = [trans] (ex₀ α) (ex₁ α)
claim₁ : (∃ \(q : ₂ℕ → U Y) → (q ∈ Probe Y) ∧ (∀(α : ₂ℕ) → [ w(cons s α) ≡ in₁(q α) ])) →
(λ α → π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(w(cons s α))) ∈ Probe Z
claim₁ (q , qY , e) = cond₃ Z (λ α → π₀(v(r(cons s α)))(q α))
(λ α → π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(w(cons s α)))
vrsqZ ex
where
vrsqZ : (λ α → π₀(v(r(cons s α)))(q α)) ∈ Probe Z
vrsqZ = vYZ q qY (r ∘ (cons s)) (Lemma[∘-UC] r ucr (cons s) (Lemma[cons-UC] s))
ex₀ : ∀(α : ₂ℕ) → [ π₀(v(r(cons s α)))(q α)
≡ π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(in₁(q α)) ]
ex₀ α = [refl]
ex₁ : ∀(α : ₂ℕ) → [ π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(in₁(q α))
≡ π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(w(cons s α)) ]
ex₁ α = [ap] (π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))) ([sym](e α))
ex : ∀(α : ₂ℕ) → [ π₀(v(r(cons s α)))(q α)
≡ π₀(π₀(c(u(t(r(cons s α)))))(v(r(cons s α))))(w(cons s α)) ]
ex α = [trans] (ex₀ α) (ex₁ α)
\end{code}