Chuangjie Xu 2013 (updated in February 2015)

\begin{code}

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

module UsingIrrelevantFunext.Space.DiscreteSpace where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingIrrelevantFunext.Irrelevance
open import UsingIrrelevantFunext.Space.Coverage
open import UsingIrrelevantFunext.Space.Space
open import UsingIrrelevantFunext.Space.CartesianClosedness
open import UsingIrrelevantFunext.IrrelevantFunext

\end{code}

The locally constant functions ₂ℕ → X on any set X form a C-topology on X. Any
space with such a C-topology is discrete, i.e. all maps from it to any other
space is continuous.

\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₀ : ∀(x : X) → (λ α → x) ∈ LC
  c₀ x =  , (λ _ _ _ → refl) , (λ _ _ → ≤-zero)

  c₁ : ∀(t : ₂ℕ → ₂ℕ) → t ∈ C → ∀(p : ₂ℕ → X) → p ∈ LC → (p ∘ t) ∈ LC
  c₁ t uct p ucp = Lemma[LM-least-modulus] _≡_ dis _⁻¹ _·_ (p ∘ t) n prf
   where
    m : ℕ
    m = pr₁ ucp
    n : ℕ
    n = pr₁(uct m)
    prp : ∀(α β : ₂ℕ) → α ≡[ m ] β → p α ≡ p β
    prp = pr₁ (pr₂ ucp)
    prt : ∀(α β : ₂ℕ) → α ≡[ n ] β → t α ≡[ m ] t β
    prt = pr₁ (pr₂ (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 , ps) = Lemma[LM-least-modulus] _≡_ dis _⁻¹ _·_ p (n + k) prf
   where
    f : ₂Fin n → ℕ
    f s = pr₁ (ps s)
    k : ℕ
    k = pr₁ (max-fin f)
    k-max : ∀(s : ₂Fin n) → f s ≤ k
    k-max = pr₂ (max-fin f)
    fact : ∀(s : ₂Fin n) → ∀(α β : ₂ℕ) → α ≡[ k ] β → p(cons s α) ≡ p(cons s β)
    fact s α β ek = pr₁ (pr₂ (ps 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] (λ x → cons x β' ≡ β) (hide (eqs ⁻¹))
                       (funext¹ (Lemma[cons-take-drop] n β))
                        -------
      awk : ∀(i : ℕ) → i < k → α' i ≡ β' i
      awk i i<k = eqα · subgoal · 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  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 , (prf , min)) [ex] = n , prf' , min'
   where
    ex : ∀(α : ₂ℕ) → p α ≡ p' α
    ex α = decidable-structure (dis (p α) (p' α)) ([ex] α)
    prf' : ∀(α β : ₂ℕ) → α ≡[ n ] β → p' α ≡ p' β
    prf' α β en = (ex α)⁻¹ · (prf α β en) · (ex β)
    min' : ∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n' ] β → p' α ≡ p' β) → n ≤ n'
    min' n' pr'' = min n' (λ α β en' → (ex α) · (pr'' α β en') · (ex β)⁻¹)


DiscreteSpace : (X : Set) → discrete X → Space
DiscreteSpace X dec = X , LC , LC-topology X dec


Lemma[discreteness] : (X : Set) (dec : discrete X) (Y : Space)
                    → ∀(f : X → U Y) → continuous (DiscreteSpace X dec) Y f
Lemma[discreteness] X dec Y f p (m , prf , _) = cond₂ Y (f ∘ p) (m , claim)
 where
  claim : ∀(s : ₂Fin m) → (f ∘ p ∘ (cons s)) ∈ Probe Y
  claim s = cond₃ Y (λ α → y) (f ∘ p ∘ (cons s)) (cond₀ Y y) claim₁
   where
    y : U Y
    y = f(p(cons s 0̄))
    claim₀ : ∀(α : ₂ℕ) → p(cons s 0̄) ≡ p(cons s α)
    claim₀ α = prf (cons s 0̄) (cons s α) (Lemma[cons-≡[]] s 0̄ α)
    claim₁ : ∀(α : ₂ℕ) → [ y ≡ f(p(cons s α)) ]
    claim₁ α = hide (ap f (claim₀ α))

\end{code}

All the uniformly continuous maps ₂ℕ → ₂ (and ₂ℕ → ℕ) are
locally constant. And hence they form a C-topology on ₂ (and ℕ).

The coproduct 1 + 1:

\begin{code}

₂Space : Space
₂Space = DiscreteSpace ₂ ₂-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) → Map ₂Space (A ⇒ A ⇒ A)
continuous-if A = IF , c-IF
 where
  IF : ₂ → U (A ⇒ A ⇒ A)
  IF b = if-b , c-if-b
   where
    if-b : U A → U (A ⇒ A)
    if-b a₀ = if-b-a₀ , c-if-b-a₀
     where
      if-b-a₀ : U A → U A
      if-b-a₀ a₁ = if b a₀ a₁
      c-if-b-a₀ : continuous A A if-b-a₀
      c-if-b-a₀ p pA = lemma b
       where
        lemma : ∀(i : ₂) → (λ a₁ → if i a₀ a₁) ∘ p ∈ Probe A
        lemma ₀ = cond₀ A a₀
        lemma ₁ = pA
    c-if-b : continuous A (A ⇒ A) if-b
    c-if-b p pA q qA t tC = lemma b
     where
      lemma : ∀(i : ₂) → (λ α → if i (p(t α)) (q α)) ∈ Probe A
      lemma ₀ = cond₁ A t tC p pA
      lemma ₁ = qA
  c-IF : continuous ₂Space (A ⇒ A ⇒ A) IF
  c-IF = Lemma[discrete-₂Space] (A ⇒ A ⇒ A) IF

\end{code}

The natural numbers object:

\begin{code}

ℕSpace : Space
ℕSpace = DiscreteSpace ℕ ℕ-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 : Map ℕSpace ℕSpace
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 = pr₁ (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 α)) (n , prf)
     where
      n : ℕ
      n = pr₁ 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         = cond₁ A (t ∘ (cons s)) ucts (λ _ → a) (cond₀ A a)
        lemma (succ k) = claim (λ α → rec a (ū(p(t(cons s α)))) k) (lemma k) id Lemma[id-UC]
         where
          claim : (λ α → pr₁ (p (t(cons s α))) k) ∈ Probe (A ⇒ A)
          claim = pNAA (λ _ → k) ( , (λ _ _ _ → 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 α = pr₁ (pr₂ 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 α)) (n , prf)
   where
    n : ℕ
    n = pr₁ 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         = 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 : (λ α → pr₁ (q(v(cons s α))) k) ∈ Probe (A ⇒ A)
        claim = qNAA (λ _ → k) ( , (λ _ _ _ → 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 α = pr₁ (pr₂ 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}

When X is an hset, local constancy of ₂ℕ → X is an hprop.

\begin{code}

Lemma[LC-[hprop]] : {X : Set} → hset X → ∀(p : ₂ℕ → X) → (lc₀ lc₁ : LC p) → [ lc₀ ≡ lc₁ ]
Lemma[LC-[hprop]] hsX p (n₀ , (prf₀ , min₀)) (n₁ , (prf₁ , min₁)) = [pair⁼] e ee
 where
  e : n₀ ≡ n₁
  e = Lemma[m≤n∧n≤m→m=n] (min₀ n₁ prf₁) (min₁ n₀ prf₀)
  prf₀'min₀' :  (∀(α β : ₂ℕ) → α ≡[ n₁ ] β → p α ≡ p β)
              × (∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n' ] β → p α ≡ p β) → n₁ ≤ n')
  prf₀'min₀' = transport _ e (prf₀ , min₀)
  prf₀' : ∀(α β : ₂ℕ) → α ≡[ n₁ ] β → p α ≡ p β
  prf₀' = pr₁ prf₀'min₀'
  eeprf : ∀(α β : ₂ℕ) → (en : α ≡[ n₁ ] β) → prf₀' α β en ≡ prf₁ α β en
  eeprf α β en = hsX (prf₀' α β en) (prf₁ α β en)
  epr : [ prf₀' ≡ prf₁ ]
  epr = funext³ eeprf
        -------
  min₀' : ∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n' ] β → p α ≡ p β) → n₁ ≤ n'
  min₀' = pr₂ prf₀'min₀'
  eemin : ∀(n' : ℕ) → (prf' : ∀(α β : ₂ℕ) → α ≡[ n' ] β → p α ≡ p β) → min₀' n' prf' ≡ min₁ n' prf'
  eemin n' prf' = Lemma[≤-hprop] (min₀' n' prf') (min₁ n' prf')
  emin : [ min₀' ≡ min₁ ]
  emin = funext² eemin
         -------
  ee : [ (prf₀' , min₀') ≡ (prf₁ , min₁) ]
  ee = [pairˣ⁼] epr emin


Lemma[Map-discrete] : (X : Space)(Y : Set)(d : discrete Y)(h : hset Y) →
                      (f g : Map X (DiscreteSpace Y d)) →
                      (∀(x : U X) → pr₁ f x ≡ pr₁ 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₀ = [pair⁼] e₀ [e₁]
   where
    W : ((p : ₂ℕ → U X) → p ∈ Probe X → ℕ) → Set
    W φ = (∀(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' : ∀(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 = pr₁ (cf' p pX)
    Φf₀ : ∀(p : ₂ℕ → U X) (pX : p ∈ Probe X)
        → ∀(α β : ₂ℕ) → α ≡[ φf p pX ] β → g(p α) ≡ g(p β)
    Φf₀ p pX = pr₁ (pr₂ (cf' p pX))
    Φf₁ : ∀(p : ₂ℕ → U X) (pX : p ∈ Probe X)
         → ∀(m : ℕ) → (∀(α β : ₂ℕ) → α ≡[ m ] β → g(p α) ≡ g(p β)) → φf p pX ≤ m
    Φf₁ p pX = pr₂ (pr₂ (cf' p pX))
    CF : Σ \(φ : (p : ₂ℕ → U X) → p ∈ Probe X → ℕ) → W φ
    CF = (φf , Φf₀ , Φf₁)

    φg : (p : ₂ℕ → U X) → p ∈ Probe X → ℕ
    φg p pX = pr₁ (cg p pX)
    Φg₀ : ∀(p : ₂ℕ → U X) (pX : p ∈ Probe X)
        → ∀(α β : ₂ℕ) → α ≡[ φg p pX ] β → g(p α) ≡ g(p β)
    Φg₀ p pX = pr₁ (pr₂ (cg p pX))
    Φg₁ : ∀(p : ₂ℕ → U X) (pX : p ∈ Probe X)
        → ∀(m : ℕ) → (∀(α β : ₂ℕ) → α ≡[ m ] β → g(p α) ≡ g(p β)) → φg p pX ≤ m
    Φg₁ p pX = pr₂ (pr₂ (cg p pX))
    CG : Σ \(φ : (p : ₂ℕ → U X) → p ∈ Probe X → ℕ) → W φ
    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φ = [pair⁼] eφ [eΦ]
     where
      Φf' : W φg
      Φf' = transport W eφ (Φf₀ , Φf₁)
      Φf₀' : ∀(p : ₂ℕ → U X) (pX : p ∈ Probe X)
           → ∀(α β : ₂ℕ) → α ≡[ φg p pX ] β → g(p α) ≡ g(p β)
      Φf₀' = pr₁ Φf'
      Φf₁' : ∀(p : ₂ℕ → U X) (pX : p ∈ Probe X)
           → ∀(m : ℕ) → (∀(α β : ₂ℕ) → α ≡[ m ] β → g(p α) ≡ g(p β)) → φg p pX ≤ m
      Φf₁' = pr₂ Φ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 (Φ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Φ] = [pairˣ⁼] [eΦ]₀ [eΦ]₁

    [E] : [ CF ≡ CG ]
    [E] = extension sclaim [eφ]

    [e₁] : [ cf' ≡ cg ]
    [e₁] = functor (ap (λ w p pX → (pr₁ w p pX , pr₁(pr₂ w) p pX , pr₂(pr₂ w) p pX))) [E]

Lemma[Map-₂-[≡]] : (X : Space) → (f g : Map X ₂Space) →
                   (∀(x : U X) → pr₁ f x ≡ pr₁ 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) → pr₁ f x ≡ pr₁ g x) → [ f ≡ g ]
Lemma[Map-ℕ-[≡]] X = Lemma[Map-discrete] X ℕ ℕ-discrete ℕ-hset

\end{code}

Assuming funext, local constancy is an hproposition.

\begin{code}

Lemma[funext→LC-hprop] : Funext → {X : Set} → hset X → ∀(p : ₂ℕ → X) → hprop (p ∈ LC)
Lemma[funext→LC-hprop] funext hsX p (n₀ , (prf₀ , min₀)) (n₁ , (prf₁ , min₁)) = pair⁼ e ee
 where
  e : n₀ ≡ n₁
  e = Lemma[m≤n∧n≤m→m=n] (min₀ n₁ prf₁) (min₁ n₀ prf₀)
  prf₀'min₀' :  (∀(α β : ₂ℕ) → α ≡[ n₁ ] β → p α ≡ p β)
             × (∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n' ] β → p α ≡ p β) → n₁ ≤ n')
  prf₀'min₀' = transport _ e (prf₀ , min₀)
  prf₀' : ∀(α β : ₂ℕ) → α ≡[ n₁ ] β → p α ≡ p β
  prf₀' α β en = pr₁ prf₀'min₀' α β en
  eepr : ∀(α β : ₂ℕ) → (en : α ≡[ n₁ ] β) → prf₀' α β en ≡ prf₁ α β en
  eepr α β en = hsX (prf₀' α β en) (prf₁ α β en)
  epr : prf₀' ≡ prf₁
  epr = funext (λ α → funext (λ β → funext (λ en → eepr α β en)))
       --------
  min₀' : ∀(n' : ℕ) → (∀(α β : ₂ℕ) → α ≡[ n' ] β → p α ≡ p β) → n₁ ≤ n'
  min₀' = pr₂ prf₀'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 (λ n' → funext (λ pr' → eemin n' pr'))
        --------
  ee : (prf₀' , min₀') ≡ (prf₁ , min₁)
  ee = pairˣ⁼ epr emin

\end{code}