\begin{code}
module Space-discrete where
open import MiniLibrary
open import Sequence
open import UniformContinuity
open import Inequality
open import Space
open import Space-exponential
open import not-not
open import not-not-funext
\end{code}
\begin{code}
LC : {X : Set} → (₂ℕ → X) → Set
LC = locally-constant
LC-topology : (X : Set) → discrete X → probe-axioms X LC
LC-topology X dis = c₀ , c₁ , c₂ , c₃
where
c₀ : ∀(p : ₂ℕ → X) → constant p → p ∈ LC
c₀ p cp = ∃-intro 0 ((λ α β e → cp α β) , (λ n e → ≤-zero))
c₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → X) → p ∈ LC → (p ∘ t) ∈ LC
c₁ t uct p ucp = Lemma[LM-least-modulus] _≡_ dis sym trans (p ∘ t) n prf
where
m : ℕ
m = ∃-witness ucp
n : ℕ
n = ∃-witness(uct m)
prp : ∀(α β : ₂ℕ) → α ≣[ m ] β → p α ≡ p β
prp = ∧-elim₀ (∃-elim ucp)
prt : ∀(α β : ₂ℕ) → α ≣[ n ] β → t α ≣[ m ] t β
prt = ∧-elim₀ (∃-elim (uct m))
prf : ∀(α β : ₂ℕ) → α ≣[ n ] β → p(t α) ≡ p(t β)
prf α β en = prp (t α) (t β) (prt α β en)
c₂ : ∀(p : ₂ℕ → X) → (∃ \(n : ℕ) → ∀(s : ₂Fin n) → (p ∘ (cons s)) ∈ LC) → p ∈ LC
c₂ p (n , pr) = Lemma[LM-least-modulus] _≡_ dis sym trans p (n + k) prf
where
f : ₂Fin n → ℕ
f s = ∃-witness (pr s)
k : ℕ
k = ∃-witness (max-fin f)
k-max : ∀(s : ₂Fin n) → f s ≤ k
k-max = ∃-elim (max-fin f)
fact : ∀(s : ₂Fin n) → ∀(α β : ₂ℕ) → α ≣[ k ] β → p(cons s α) ≡ p(cons s β)
fact s α β ek = ∧-elim₀ (∃-elim (pr s)) α β (Lemma[≣[]-≤] ek (k-max s))
prf : ∀(α β : ₂ℕ) → α ≣[ n + k ] β → p α ≡ p β
prf α β enk = decidable-structure (dis (p α) (p β)) goal
where
s : ₂Fin n
s = take n α
en : α ≣[ n ] β
en = Lemma[≣[]-≤] enk (Lemma[a≤a+b] n k)
eqs : take n α ≡ take n β
eqs = Lemma[≣[]-take] en
α' : ₂ℕ
α' = drop n α
pα : [ cons s α' ≡ α ]
pα = funext¹ (Lemma[cons-take-drop] n α)
β' : ₂ℕ
β' = drop n β
pβ : [ cons s β' ≡ β ]
pβ = [transport] {₂Fin n} {λ x → cons x β' ≡ β}
(hide (sym eqs)) (funext¹ (Lemma[cons-take-drop] n β))
awk : ∀(i : ℕ) → i < k → α' i ≡ β' i
awk i i<k = trans (trans eqα subgoal) (sym eqβ)
where
i+n<k+n : i + n < k + n
i+n<k+n = Lemma[a<b→a+c<b+c] i k n i<k
i+n<n+k : i + n < n + k
i+n<n+k = transport {ℕ} {λ m → (i + n) < m} (Lemma[n+m=m+n] k n) i+n<k+n
subgoal : α (i + n) ≡ β (i + n)
subgoal = Lemma[≣[]-<] enk (i + n) i+n<n+k
le : (n i : ℕ) → (α : ₂ℕ) → drop n α i ≡ α (i + n)
le 0 i α = refl
le (succ n) i α = le n i (α ∘ succ)
eqα : α' i ≡ α (i + n)
eqα = le n i α
eqβ : β' i ≡ β (i + n)
eqβ = le n i β
ek : α' ≣[ k ] β'
ek = Lemma[<-≣[]] awk
goal : [ p α ≡ p β ]
goal = [transport] {₂ℕ} {λ x → p α ≡ p x} pβ ([transport] {₂ℕ} {λ x → p x ≡ p(cons s β')} pα (hide (fact s α' β' ek)))
c₃ : ∀(p p' : ₂ℕ → X) → p ∈ LC → (∀(α : ₂ℕ) → [ p α ≡ p' α ]) → p' ∈ LC
c₃ p p' (n , (pr , min)) [ex] = ∃-intro n (∧-intro pr' min')
where
ex : ∀(α : ₂ℕ) → p α ≡ p' α
ex α = decidable-structure (dis (p α) (p' α)) ([ex] α)
pr' : ∀(α β : ₂ℕ) → α ≣[ n ] β → p' α ≡ p' β
pr' α β en = trans (trans (sym (ex α)) (pr α β en)) (ex β)
min' : ∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≣[ n' ] β → p' α ≡ p' β) → n ≤ n'
min' n' pr'' = min n' claim
where
claim : ∀(α β : ₂ℕ) → α ≣[ n' ] β → p α ≡ p β
claim α β en' = trans (trans (ex α) (pr'' α β en')) (sym (ex β))
Discrete-Space : (X : Set) → discrete X → Space
Discrete-Space X dec = X , LC , LC-topology X dec
Lemma[discreteness] : {X : Set}{dec : discrete X} → ∀{Y : Space} → ∀(f : X → U Y) →
continuous {Discrete-Space X dec} {Y} f
Lemma[discreteness] {X} {dec} {Y} f p plc = cond₂ Y (f ∘ p) (∃-intro m claim)
where
m : ℕ
m = ∃-witness plc
claim : ∀(s : ₂Fin m) → (f ∘ p ∘ (cons s)) ∈ Probe Y
claim s = cond₀ Y (f ∘ p ∘ (cons s)) claim₁
where
claim₀ : constant (p ∘ (cons s))
claim₀ α β = ∧-elim₀ (∃-elim plc) (cons s α) (cons s β) (Lemma[cons-≣[]] s α β)
claim₁ : constant (f ∘ p ∘ (cons s))
claim₁ = Lemma[∘-constant] (p ∘ (cons s)) f claim₀
\end{code}
\begin{code}
₂Space : Space
₂Space = Discrete-Space ₂ ₂-discrete
Lemma[discrete-₂Space] : {X : Space} → ∀(f : ₂ → U X) → continuous {₂Space} {X} f
Lemma[discrete-₂Space] {X} f = Lemma[discreteness] {₂} {₂-discrete} {X} f
continuous-if : {A : Space} →
Σ \(If : U A → U(A ⇒ ₂Space ⇒ A)) →
continuous {A} {A ⇒ ₂Space ⇒ A} If
continuous-if {A} = (If , continuity-of-if)
where
If : U A → U(A ⇒ ₂Space ⇒ A)
If a = (f , cf)
where
f : U A → U(₂Space ⇒ A)
f a' = if a a' , Lemma[discrete-₂Space] {A} (if a a')
cf : continuous {A} {₂Space ⇒ A} f
cf p pa q q2 t uct = cond₂ A (λ α → if a (p(t α)) (q α)) (∃-intro n prf)
where
n : ℕ
n = ∃-witness q2
prf : ∀(s : ₂Fin n) → (λ α → if a (p (t (cons s α))) (q (cons s α))) ∈ Probe A
prf s = cond₃ A (λ α → if a (p (t (cons s α))) (q (cons s 0̄)))
(λ α → if a (p (t (cons s α))) (q (cons s α))) claim₀ claim₁
where
ucts : uniformly-continuous-₂ℕ (t ∘ (cons s))
ucts = Lemma[∘-UC] t uct (cons s) (Lemma[cons-UC] s)
lemma : ∀(b : ₂) → (λ α → if a (p (t (cons s α))) b) ∈ Probe A
lemma ₀ = cond₀ A (λ α → a) (λ α β → refl)
lemma ₁ = cond₁ A (t ∘ (cons s)) ucts p pa
claim₀ : (λ α → if a (p (t (cons s α))) (q (cons s 0̄))) ∈ Probe A
claim₀ = lemma (q (cons s 0̄))
eq : ∀(α : ₂ℕ) → q (cons s 0̄) ≡ q (cons s α)
eq α = ∧-elim₀ (∃-elim q2) (cons s 0̄) (cons s α) (Lemma[cons-≣[]] s 0̄ α)
claim₁ : ∀(α : ₂ℕ) → [ if a (p (t (cons s α))) (q (cons s 0̄)) ≡
if a (p (t (cons s α))) (q (cons s α)) ]
claim₁ α = hide (ap (if a (p (t (cons s α)))) (eq α))
continuity-of-if : continuous {A} {A ⇒ ₂Space ⇒ A} If
continuity-of-if p pa q qa t uct r r2 u ucu = cond₂ A (λ α → if (p(t(u α))) (q(u α)) (r α)) (∃-intro n prf)
where
n : ℕ
n = ∃-witness r2
prf : ∀(s : ₂Fin n) → (λ α → if (p(t(u(cons s α)))) (q(u(cons s α))) (r(cons s α))) ∈ Probe A
prf s = cond₃ A (λ α → if (p(t(u(cons s α)))) (q(u(cons s α))) (r (cons s 0̄)))
(λ α → if (p(t(u(cons s α)))) (q(u(cons s α))) (r(cons s α)))
claim₀ claim₁
where
ucus : uniformly-continuous-₂ℕ (u ∘ (cons s))
ucus = Lemma[∘-UC] u ucu (cons s) (Lemma[cons-UC] s)
uctus : uniformly-continuous-₂ℕ (t ∘ u ∘ (cons s))
uctus = Lemma[∘-UC] t uct (u ∘ (cons s)) ucus
lemma : ∀(b : ₂) → (λ α → if (p(t(u(cons s α)))) (q(u(cons s α))) b) ∈ Probe A
lemma ₀ = cond₁ A (t ∘ u ∘ (cons s)) uctus p pa
lemma ₁ = cond₁ A (u ∘ (cons s)) ucus q qa
claim₀ : (λ α → if (p(t(u(cons s α)))) (q(u(cons s α))) (r (cons s 0̄))) ∈ Probe A
claim₀ = lemma (r (cons s 0̄))
eq : ∀(α : ₂ℕ) → r (cons s 0̄) ≡ r (cons s α)
eq α = ∧-elim₀ (∃-elim r2) (cons s 0̄) (cons s α) (Lemma[cons-≣[]] s 0̄ α)
claim₁ : ∀(α : ₂ℕ) → [ if (p(t(u(cons s α)))) (q(u(cons s α))) (r(cons s 0̄)) ≡
if (p(t(u(cons s α)))) (q(u(cons s α))) (r(cons s α)) ]
claim₁ α = hide (ap (if (p(t(u(cons s α)))) (q(u(cons s α)))) (eq α))
\end{code}
\begin{code}
ℕSpace : Space
ℕSpace = Discrete-Space ℕ ℕ-discrete
Lemma[discrete-ℕSpace] : {X : Space} → ∀(f : ℕ → U X) → continuous {ℕSpace} {X} f
Lemma[discrete-ℕSpace] {X} f = Lemma[discreteness] {ℕ} {ℕ-discrete} {X} f
continuous-succ : Σ \(s : ℕ → ℕ) → continuous {ℕSpace} {ℕSpace} s
continuous-succ = succ , Lemma[discrete-ℕSpace] {ℕSpace} succ
continuous-rec : {A : Space} → Map A ((ℕSpace ⇒ A ⇒ A) ⇒ ℕSpace ⇒ A)
continuous-rec {A} = r , continuity-of-rec
where
ū : U(ℕSpace ⇒ A ⇒ A) → ℕ → U A → U A
ū (f , _) n x = π₀ (f n) x
r : U A → U((ℕSpace ⇒ A ⇒ A) ⇒ ℕSpace ⇒ A)
r a = (g , cg)
where
g : U(ℕSpace ⇒ A ⇒ A) → U(ℕSpace ⇒ A)
g f = rec a (ū f) , Lemma[discrete-ℕSpace] {A} (rec a (ū f))
cg : continuous {ℕSpace ⇒ A ⇒ A} {ℕSpace ⇒ A} g
cg p pNAA q qN t uct = cond₂ A (λ α → rec a (ū(p(t α))) (q α)) (∃-intro n prf)
where
n : ℕ
n = ∃-witness qN
prf : ∀(s : ₂Fin n) → (λ α → rec a (ū(p(t(cons s α)))) (q(cons s α))) ∈ Probe A
prf s = cond₃ A (λ α → rec a (ū(p(t(cons s α)))) (q(cons s 0̄)))
(λ α → rec a (ū(p(t(cons s α)))) (q(cons s α)))
claim₀ claim₁
where
ucts : uniformly-continuous-₂ℕ (t ∘ (cons s))
ucts = Lemma[∘-UC] t uct (cons s) (Lemma[cons-UC] s)
lemma : ∀(k : ℕ) → (λ α → rec a (ū(p(t(cons s α)))) k) ∈ Probe A
lemma 0 = cond₁ A (t ∘ (cons s)) ucts (λ _ → a) ((cond₀ A (λ _ → a) (λ _ _ → refl)))
lemma (succ k) = claim (λ α → rec a (ū(p(t(cons s α)))) k) (lemma k) id Lemma[id-UC]
where
claim : (λ α → π₀ (p (t(cons s α))) k) ∈ Probe (A ⇒ A)
claim = pNAA (λ _ → k) (0 , (λ _ _ _ → refl) , (λ _ _ → ≤-zero)) (t ∘ (cons s)) ucts
claim₀ : (λ α → rec a (ū(p(t(cons s α)))) (q(cons s 0̄))) ∈ Probe A
claim₀ = lemma (q(cons s 0̄))
eq : ∀(α : ₂ℕ) → q (cons s 0̄) ≡ q (cons s α)
eq α = ∧-elim₀ (∃-elim qN) (cons s 0̄) (cons s α) (Lemma[cons-≣[]] s 0̄ α)
claim₁ : ∀(α : ₂ℕ) → [ rec a (ū(p(t(cons s α)))) (q(cons s 0̄))
≡ rec a (ū(p(t(cons s α)))) (q(cons s α)) ]
claim₁ α = hide (ap (rec a (ū(p(t(cons s α))))) (eq α))
continuity-of-rec : continuous {A} {(ℕSpace ⇒ A ⇒ A) ⇒ ℕSpace ⇒ A} r
continuity-of-rec p pA q qNAA t uct u uN v ucv = cond₂ A (λ α → rec (p(t(v α))) (ū(q(v α))) (u α)) (∃-intro n prf)
where
n : ℕ
n = ∃-witness uN
prf : ∀(s : ₂Fin n) → (λ α → rec (p(t(v(cons s α)))) (ū(q(v(cons s α)))) (u(cons s α))) ∈ Probe A
prf s = cond₃ A (λ α → rec (p(t(v(cons s α)))) (ū(q(v(cons s α)))) (u(cons s 0̄)))
(λ α → rec (p(t(v(cons s α)))) (ū(q(v(cons s α)))) (u(cons s α)))
claim₀ claim₁
where
ucvs : uniformly-continuous-₂ℕ (v ∘ (cons s))
ucvs = Lemma[∘-UC] v ucv (cons s) (Lemma[cons-UC] s)
uctvs : uniformly-continuous-₂ℕ (t ∘ v ∘ (cons s))
uctvs = Lemma[∘-UC] t uct (v ∘ (cons s)) ucvs
lemma : ∀(k : ℕ) → (λ α → rec (p(t(v(cons s α)))) (ū(q(v(cons s α)))) k) ∈ Probe A
lemma 0 = cond₁ A (t ∘ v ∘ (cons s)) uctvs p pA
lemma (succ k) = claim (λ α → rec (p(t(v(cons s α)))) (ū(q(v(cons s α)))) k) (lemma k) id Lemma[id-UC]
where
claim : (λ α → π₀ (q(v(cons s α))) k) ∈ Probe (A ⇒ A)
claim = qNAA (λ _ → k) (0 , (λ _ _ _ → refl) , (λ _ _ → ≤-zero)) (v ∘ (cons s)) ucvs
claim₀ : (λ α → rec (p(t(v(cons s α)))) (ū(q(v(cons s α)))) (u(cons s 0̄))) ∈ Probe A
claim₀ = lemma (u(cons s 0̄))
eq : ∀(α : ₂ℕ) → u(cons s 0̄) ≡ u(cons s α)
eq α = ∧-elim₀ (∃-elim uN) (cons s 0̄) (cons s α) (Lemma[cons-≣[]] s 0̄ α)
claim₁ : ∀(α : ₂ℕ) → [ rec (p(t(v(cons s α)))) (ū(q(v(cons s α)))) (u(cons s 0̄))
≡ rec (p(t(v(cons s α)))) (ū(q(v(cons s α)))) (u(cons s α)) ]
claim₁ α = hide (ap (rec (p(t(v(cons s α)))) (ū(q(v(cons s α))))) (eq α))
\end{code}
\begin{code}
Lemma[LC-hprop] : {X : Set} → hset X → ∀(p : ₂ℕ → X) → (lc₀ lc₁ : LC p) → [ lc₀ ≡ lc₁ ]
Lemma[LC-hprop] hsX p (n₀ , (pr₀ , min₀)) (n₁ , (pr₁ , min₁)) = Lemma[[≡]-Σ] e ee
where
e : n₀ ≡ n₁
e = Lemma[m≤n∧n≤m→m=n] (min₀ n₁ pr₁) (min₁ n₀ pr₀)
pr₀'min₀' : (∀(α β : ₂ℕ) → α ≣[ n₁ ] β → p α ≡ p β)
∧ (∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≣[ n' ] β → p α ≡ p β) → n₁ ≤ n')
pr₀'min₀' = transport e (∧-intro pr₀ min₀)
pr₀' : ∀(α β : ₂ℕ) → α ≣[ n₁ ] β → p α ≡ p β
pr₀' α β en = ∧-elim₀ pr₀'min₀' α β en
eepr : ∀(α β : ₂ℕ) → (en : α ≣[ n₁ ] β) → pr₀' α β en ≡ pr₁ α β en
eepr α β en = hsX (p α) (p β) (pr₀' α β en) (pr₁ α β en)
epr : [ pr₀' ≡ pr₁ ]
epr = funext³ eepr
min₀' : ∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≣[ n' ] β → p α ≡ p β) → n₁ ≤ n'
min₀' = ∧-elim₁ pr₀'min₀'
eemin : ∀(n' : ℕ) → (pr' : ∀(α β : ₂ℕ) → α ≣[ n' ] β → p α ≡ p β) → min₀' n' pr' ≡ min₁ n' pr'
eemin n' pr' = Lemma[≤-hprop] (min₀' n' pr') (min₁ n' pr')
emin : [ min₀' ≡ min₁ ]
emin = funext² eemin
ee : [ (pr₀' , min₀') ≡ (pr₁ , min₁) ]
ee = Lemma[[≡]-∧] epr emin
Lemma[Map-discrete] : (X : Space)(Y : Set)(d : discrete Y)(h : hset Y) →
(f g : Map X (Discrete-Space Y d)) →
(∀(x : U X) → π₀ f x ≡ π₀ g x) → [ f ≡ g ]
Lemma[Map-discrete] X Y d h (f , cf) (g , cg) ex = extension claim [e₀]
where
[e₀] : [ f ≡ g ]
[e₀] = funext¹ ex
claim : f ≡ g → [ (f , cf) ≡ (g , cg) ]
claim e₀ = Lemma[[≡]-Σ] e₀ [e₁]
where
cf' : ∀(p : ₂ℕ → U X) → p ∈ Probe X →
∃ \(n : ℕ) →
(∀(α β : ₂ℕ) → α ≣[ n ] β → g(p α) ≡ g(p β))
∧ (∀(m : ℕ) → (∀(α β : ₂ℕ) → α ≣[ m ] β → g(p α) ≡ g(p β)) → n ≤ m)
cf' = transport e₀ cf
φf : (p : ₂ℕ → U X) → p ∈ Probe X → ℕ
φf p pX = ∃-witness (cf' p pX)
Φf₀ : ∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(α β : ₂ℕ) → α ≣[ φf p pX ] β → g(p α) ≡ g(p β)
Φf₀ p pX = ∧-elim₀ (∃-elim (cf' p pX))
Φf₁ : ∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(m : ℕ) → (∀(α β : ₂ℕ) → α ≣[ m ] β → g(p α) ≡ g(p β)) → φf p pX ≤ m
Φf₁ p pX = ∧-elim₁ (∃-elim (cf' p pX))
CF : ∃ \(φ : (p : ₂ℕ → U X) → p ∈ Probe X → ℕ) →
(∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(α β : ₂ℕ) → α ≣[ φ p pX ] β → g(p α) ≡ g(p β))
∧ (∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(m : ℕ) → (∀(α β : ₂ℕ) → α ≣[ m ] β → g(p α) ≡ g(p β)) → φ p pX ≤ m)
CF = (φf , Φf₀ , Φf₁)
φg : (p : ₂ℕ → U X) → p ∈ Probe X → ℕ
φg p pX = ∃-witness (cg p pX)
Φg₀ : ∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(α β : ₂ℕ) → α ≣[ φg p pX ] β → g(p α) ≡ g(p β)
Φg₀ p pX = ∧-elim₀ (∃-elim (cg p pX))
Φg₁ : ∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(m : ℕ) → (∀(α β : ₂ℕ) → α ≣[ m ] β → g(p α) ≡ g(p β)) → φg p pX ≤ m
Φg₁ p pX = ∧-elim₁ (∃-elim (cg p pX))
CG : ∃ \(φ : (p : ₂ℕ → U X) → p ∈ Probe X → ℕ) →
(∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(α β : ₂ℕ) → α ≣[ φ p pX ] β → g(p α) ≡ g(p β))
∧ (∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(m : ℕ) → (∀(α β : ₂ℕ) → α ≣[ m ] β → g(p α) ≡ g(p β)) → φ p pX ≤ m)
CG = (φg , Φg₀ , Φg₁)
[eφ] : [ φf ≡ φg ]
[eφ] = funext² epx
where
epx : (p : ₂ℕ → U X) → (pX : p ∈ Probe X) → φf p pX ≡ φg p pX
epx p pX = Lemma[m≤n∧n≤m→m=n] claim₀ claim₁
where
claim₀ : φf p pX ≤ φg p pX
claim₀ = Φf₁ p pX (φg p pX) (Φg₀ p pX)
claim₁ : φg p pX ≤ φf p pX
claim₁ = Φg₁ p pX (φf p pX) (Φf₀ p pX)
sclaim : φf ≡ φg → [ CF ≡ CG ]
sclaim eφ = Lemma[[≡]-Σ] eφ [eΦ]
where
Φf' : (∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(α β : ₂ℕ) → α ≣[ φg p pX ] β → g(p α) ≡ g(p β))
∧ (∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(m : ℕ) → (∀(α β : ₂ℕ) → α ≣[ m ] β → g(p α) ≡ g(p β)) → φg p pX ≤ m)
Φf' = transport {(p : ₂ℕ → U X) → p ∈ Probe X → ℕ}
{λ φ → (∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(α β : ₂ℕ) → α ≣[ φ p pX ] β → g(p α) ≡ g(p β))
∧ (∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(m : ℕ) → (∀(α β : ₂ℕ) → α ≣[ m ] β → g(p α) ≡ g(p β)) → φ p pX ≤ m)}
eφ (Φf₀ , Φf₁)
Φf₀' : ∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(α β : ₂ℕ) → α ≣[ φg p pX ] β → g(p α) ≡ g(p β)
Φf₀' = ∧-elim₀ Φf'
Φf₁' : ∀(p : ₂ℕ → U X) → ∀(pX : p ∈ Probe X) → ∀(m : ℕ) → (∀(α β : ₂ℕ) → α ≣[ m ] β → g(p α) ≡ g(p β)) → φg p pX ≤ m
Φf₁' = ∧-elim₁ Φf'
[eΦ]₀ : [ Φf₀' ≡ Φg₀ ]
[eΦ]₀ = funext⁵ fact
where
fact : (p : ₂ℕ → U X) → (pX : p ∈ Probe X) → ∀(α β : ₂ℕ) → (en : α ≣[ φg p pX ] β) →
Φf₀' p pX α β en ≡ Φg₀ p pX α β en
fact p pX α β en = h (g(p α)) (g(p β)) (Φf₀' p pX α β en) (Φg₀ p pX α β en)
[eΦ]₁ : [ Φf₁' ≡ Φg₁ ]
[eΦ]₁ = funext⁴ fact
where
fact : (p : ₂ℕ → U X) → (pX : p ∈ Probe X) → (m : ℕ) → (pr : ∀(α β : ₂ℕ) → α ≣[ m ] β → g(p α) ≡ g(p β)) →
Φf₁' p pX m pr ≡ Φg₁ p pX m pr
fact p pX m pr = Lemma[≤-hprop] (Φf₁' p pX m pr) (Φg₁ p pX m pr)
[eΦ] : [ (Φf₀' , Φf₁') ≡ (Φg₀ , Φg₁) ]
[eΦ] = Lemma[[≡]-∧] [eΦ]₀ [eΦ]₁
[E] : [ CF ≡ CG ]
[E] = extension sclaim [eφ]
[e₁] : [ cf' ≡ cg ]
[e₁] = functor (ap (λ w p pX → (π₀ w p pX , π₀(π₁ w) p pX , π₁(π₁ w) p pX))) [E]
Lemma[Map-₂] : (X : Space) → (f g : Map X ₂Space) →
(∀(x : U X) → π₀ f x ≡ π₀ g x) → [ f ≡ g ]
Lemma[Map-₂] X = Lemma[Map-discrete] X ₂ ₂-discrete ₂-hset
Lemma[Map-ℕ] : (X : Space) → (f g : Map X ℕSpace) →
(∀(x : U X) → π₀ f x ≡ π₀ g x) → [ f ≡ g ]
Lemma[Map-ℕ] X = Lemma[Map-discrete] X ℕ ℕ-discrete ℕ-hset
\end{code}