Martin Escardo, 5-28 April 2026.

The set of decreasing sequences of natural numbers bounded by a
natural number k is compact, aka searchable, and also totally
separated. That is, it is a Stone type. This is because it is
isomorphic to another set we know to be compact. This doesn't require
univalence. Our only assumption is function extensionality. And total
separatedness follows directly from previous results.

This result was first announced at 7FWTop [1], before the formal proof
here in Agda was completed, although the informal construction was
already in this file at that time in mathematical vernacular (see [2]
below).

[1] https://martinescardo.github.io/.talks/escardo-venice2026-stone-types.pdf

In any case, we don't obtain any new compact type here, but instead
just a, perhaps more appealing, isomorphic copy.

\begin{code}

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

open import MLTT.Spartan hiding (_+_)
open import UF.FunExt

module TypeTopology.BoundedDecreasingSequences (fe : Fun-Ext) where

open import CoNaturals.Type
open import MLTT.Two-Properties
open import Naturals.Addition
open import Naturals.Order
open import Naturals.Subtraction
open import Notation.CanonicalMap
open import Notation.Order
open import TypeTopology.CompactTypes
open import TypeTopology.GenericConvergentSequenceCompactness
open import TypeTopology.MicroTychonoff
open import TypeTopology.SquashedCantor (λ 𝓤 𝓥 → fe {𝓤} {𝓥})
open import TypeTopology.SquashedSum
open import TypeTopology.TotallySeparated
open import UF.Base
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

\end{code}

We first define the type of decreasing sequences of natural numbers
bounded by a natural number k.

\begin{code}

is-bounded-by : ℕ → (ℕ → ℕ) → 𝓤₀ ̇
is-bounded-by k α = (n : ℕ) → α n ≤ k

\end{code}

In the following "decreasing" means non-strictly decreasing. We call
it `is-decreasing'` because `is-decreasing` is already taken and
needed here, for non-strictly decreasing binary sequences.

\begin{code}

is-decreasing' : (ℕ → ℕ) → 𝓤₀ ̇
is-decreasing' α = (n : ℕ) → α n ≥ α (succ n)

\end{code}

The following immediate consequence of the above condition is going to
be useful below.

\begin{code}

is-decreasing'' : (β : ℕ → ℕ)
                → is-decreasing' β
                → (n₀ n : ℕ)
                → β n₀ ≥ β (n₀ + n)
is-decreasing'' β δ n₀         = ≤-refl (β n₀)
is-decreasing'' β δ n₀ (succ n) =
 ≤-trans (β (n₀ + succ n)) (β (n₀ + n)) (β n₀)
  (δ (n₀ + n))
  (is-decreasing'' β δ n₀ n)

\end{code}

We now combine the two notions to get the type 𝔹 k of sequences
bounded by k.

\begin{code}

is-bd : ℕ → (ℕ → ℕ) → 𝓤₀ ̇
is-bd k α = is-bounded-by k α × is-decreasing' α

being-bounded-by-is-prop : (k : ℕ) (α : ℕ → ℕ) → is-prop (is-bounded-by k α)
being-bounded-by-is-prop k α = Π-is-prop fe (λ n → ≤-is-prop-valued (α n) k)

being-decreasing'-is-prop : (α : ℕ → ℕ) → is-prop (is-decreasing' α)
being-decreasing'-is-prop α = Π-is-prop fe
                               (λ n → ≤-is-prop-valued (α (succ n)) (α n))

being-bd-is-prop : (k : ℕ) (α : ℕ → ℕ) → is-prop (is-bd k α)
being-bd-is-prop k α = ×-is-prop
                        (being-bounded-by-is-prop k α)
                        (being-decreasing'-is-prop α)

𝔹 : ℕ → 𝓤₀ ̇
𝔹 k = Σ α ꞉ (ℕ → ℕ) , is-bd k α

\end{code}

We now name some projections for the sake of clarity.

\begin{code}

𝔹-sequence : {k : ℕ} → 𝔹 k → (ℕ → ℕ)
𝔹-sequence (α , _ , _) = α

\end{code}

We use the overloaded canonical-map notation ι to denote the
underlying sequence of an element of 𝔹 k.

\begin{code}

module _ {k : ℕ} where
 instance
  canonical-map-𝔹-ℕ→ℕ : Canonical-Map (𝔹 k) (ℕ → ℕ)
  ι {{canonical-map-𝔹-ℕ→ℕ}} = 𝔹-sequence {k}

\end{code}

With this notation, we continue to name the projections.

\begin{code}

𝔹-is-bounded-by : {k : ℕ}
                  (𝕓 : 𝔹 k)
                → is-bounded-by k (ι 𝕓)
𝔹-is-bounded-by (_ , b , _) = b

\end{code}

We will let δ range over witnesses of `is-decreasing'`.

\begin{code}

𝔹-is-decreasing' : {k : ℕ}
                   (𝕓 : 𝔹 k)
                 → is-decreasing' (ι 𝕓)
𝔹-is-decreasing' (_ , _ , δ) = δ

\end{code}

The following equality criterion of elements of the type 𝔹 k amounts
to the pointwise injectivity of the inclusion map of 𝔹 k into the
Baire type (ℕ → ℕ).

\begin{code}

to-𝔹-＝ : {k : ℕ}
          (𝕓 𝕓' : 𝔹 k)
        → ι 𝕓 ∼ ι 𝕓'
        → 𝕓 ＝ 𝕓'
to-𝔹-＝ {k} (α , _) (β , _) h = to-subtype-＝ (being-bd-is-prop k) (dfunext fe h)

\end{code}

We now define 𝓑 k = 𝔻ᵏ 𝟙 by induction on k, where 𝔻 is the delay monad
defined in the module SquashedCantor. Our objective is to eventually
show that 𝔹 k ≃ 𝓑 k, in order to derive the claims made above as a
corollary.

\begin{code}

𝓑 : ℕ → 𝓤₀ ̇
𝓑         = 𝟙
𝓑 (succ k) = 𝔻 (𝓑 k )

𝔻-preserves-compactness∙ : (X : 𝓤 ̇ )
                         → is-compact∙ X
                         → is-compact∙ (𝔻 X)
𝔻-preserves-compactness∙ X κ =
 Σ-is-compact∙
  (ℕ∞-compact∙ fe)
  (λ u → micro-tychonoff fe (being-finite-is-prop fe u) (λ _ → κ))

𝔻-preserves-total-separatedness : (X : 𝓤 ̇ )
                                → is-totally-separated X
                                → is-totally-separated (𝔻 X)
𝔻-preserves-total-separatedness X τ =
 Σ¹-is-totally-separated (λ 𝓤 𝓥 → fe {𝓤} {𝓥}) (λ _ → X) (λ _ → τ)

𝓑-is-compact∙ : (k : ℕ) → is-compact∙ (𝓑 k)
𝓑-is-compact∙         = 𝟙-is-compact∙
𝓑-is-compact∙ (succ k) = 𝔻-preserves-compactness∙ (𝓑 k) (𝓑-is-compact∙ k)

𝔻-preserves-≃ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X ≃ Y → 𝔻 X ≃ 𝔻 Y
𝔻-preserves-≃ e = Σ-cong (λ u → Π-cong fe fe (λ φ → e))

𝔹-base : 𝔹  ≃ 𝟙 {𝓤}
𝔹-base = singleton-≃-𝟙
          (((λ _ → ) , unique-to-𝟙 , unique-to-𝟙) ,
          (λ (α , b , d) → to-𝔹-＝ _ _ (λ n → (zero-least'' (α n) (b n))⁻¹)))

\end{code}

The main result of this file is the following, where 𝔹-step, defined
later, is the main tool.

\begin{code}

𝔹-step : (k : ℕ) → 𝔹 (succ k) ≃ 𝔻 (𝔹 k)

\end{code}

With this we conclude that 𝔹 k ≃ 𝓑 k and hence 𝔹 k is compact, which
is what we wanted to show in this file.

\begin{code}

𝔹-and-𝓑-are-equivalent : (k : ℕ) → 𝔹 k ≃ 𝓑 k
𝔹-and-𝓑-are-equivalent         = 𝔹-base
𝔹-and-𝓑-are-equivalent (succ k) =
 𝔹 (succ k) ≃⟨ 𝔹-step k ⟩
 𝔻 (𝔹 k)    ≃⟨ 𝔻-preserves-≃ (𝔹-and-𝓑-are-equivalent k) ⟩
 𝔻 (𝓑 k)    ≃⟨ ≃-refl _ ⟩
 𝓑 (succ k) ■

𝔹-is-compact∙ : (k : ℕ) → is-compact∙ (𝔹 k)
𝔹-is-compact∙ k = compact∙-types-are-closed-under-equiv
                   (≃-sym (𝔹-and-𝓑-are-equivalent k))
                   (𝓑-is-compact∙ k)
\end{code}

[2] In order to conclude, we now construct the claimed isomorphism

     𝔹-step : 𝔹 (succ k) ≃ 𝔻 (𝔹 k)

    as follows.

    (→) Given a decreasing sequence β : ℕ → ℕ, we define α : ℕ → 𝟚 by

         α n = ₁ iff β n = succ k.

        This is decreasing, and hence gives an element x of ℕ∞.

        Now assume x is finite. This means that there is a minimal n₀ such
        that α n₀ = ₀.

        We define an element of 𝔹 k with underlying sequence γ : ℕ → ℕ defined by

         γ n = β (n + n₀),

        which is bounded by k and is decreasing.

    (←) To undo this, given α : ℕ → 𝟚 decreasing for x : ℕ∞ and
        𝕓 : is-finite x → B k, we define

         β n = succ k               if α n = ₁
               𝕓 (n₀ , e₀) (n - n₀) otherwise,

        where n₀ is the minimal number with n₀ ≤ n and e₀ : α n₀ = ₀.

The following formal construction and proof in Agda of the above is
rather laborious but routine.

Minor remark. It would have been slightly better to instead define
γ n = β (n₀ + n). This would have saved us from applying commutativity of
addition twice. But it would also require slightly changing other
things. So we'll leave it at that.

We begin with the following transport lemma, which is a generalization
of `transport-finite` in the module SquashedCantor, and will be crucial
for our purposes, but will be used much later.

\begin{code}

transport-is-finite
 : {k : ℕ}
   {u v : ℕ∞}
   (q : u ＝ v)
   (π : is-finite u → 𝔹 k)
   (φ : is-finite v)
 → transport (λ - → is-finite - → 𝔹 k) q π φ ＝ π (transport is-finite (q ⁻¹) φ)
transport-is-finite refl h φ = refl

\end{code}

We now proceed to the proof of 𝔹-step, which, in turn, requires many steps itself.

\begin{code}

𝔹-step k = qinveq f (g , gf , fg)
 where

\end{code}

We begin with auxiliary constructions and lemmas for the forward direction.

\begin{code}

  α-of : (ℕ → ℕ) → (ℕ → 𝟚)
  α-of β n = χ＝ (β n) (succ k)

  module _ (β : ℕ → ℕ) (n : ℕ) where

   α-of-₁ : β n ＝ succ k → α-of β n ＝ ₁
   α-of-₁ e = different-from-₀-equal-₁
               (λ s → pr₁ (χ＝-spec (β n) (succ k)) s e)

   α-of-₁-converse : α-of β n ＝ ₁ → β n ＝ succ k
   α-of-₁-converse p = pr₂ (χ＝-spec (β n) (succ k)) p

   α-of-₀ : α-of β n ＝ ₀ → β n ≠ succ k
   α-of-₀ p = pr₁ (χ＝-spec (β n) (succ k)) p

   α-of-₀-converse : β n ≠ succ k → α-of β n ＝ ₀
   α-of-₀-converse ne = different-from-₁-equal-₀
                         (λ p → ne (α-of-₁-converse p))

   α-of-equals-₀-gives-bounded : is-bounded-by (succ k) β
                               → α-of β n ＝ ₀
                               → β n ≤ k
   α-of-equals-₀-gives-bounded b p = ≤-down (β n) k (b n) (α-of-₀ p)

  α-of-decreasing : (β : ℕ → ℕ)
                  → is-bounded-by (succ k) β
                  → is-decreasing' β
                  → is-decreasing (α-of β)
  α-of-decreasing β b δ n = ≤₂-criterion IV
   where
    IV : α-of β (succ n) ＝ ₁ → α-of β n ＝ ₁
    IV p = α-of-₁ β n III
     where
      I : β (succ n) ＝ succ k
      I = α-of-₁-converse β (succ n) p

      II : succ k ≤ β n
      II = transport (_≤ β n) I (δ n)

      III : β n ＝ succ k
      III = ≤-anti (β n) (succ k) (b n) II

  u-of : 𝔹 (succ k) → ℕ∞
  u-of (β , b , δ) = α-of β , α-of-decreasing β b δ

  α-of-equals-₀-criterion : (𝕓 : 𝔹 (succ k))
                            (φ : is-finite (u-of 𝕓))
                          → α-of (ι 𝕓) (size φ) ＝ ₀
  α-of-equals-₀-criterion (β , _ , _) (n₀ , e) =
   α-of β n₀    ＝⟨ ap (λ - → ι - n₀) (e ⁻¹) ⟩
   ι (ι n₀) n₀  ＝⟨ ℕ-to-ℕ∞-diagonal₀ n₀ ⟩
   ₀            ∎

  π-of : (𝕓 : 𝔹 (succ k)) → is-finite (u-of 𝕓) → 𝔹 k
  π-of 𝕓@(β , b , δ) φ = γ , II , III
    where
     n₀ : ℕ
     n₀ = size φ

     γ : ℕ → ℕ
     γ n = β (n₀ + n)

     I : β n₀ ≤ k
     I = α-of-equals-₀-gives-bounded β n₀ b (α-of-equals-₀-criterion 𝕓 φ)

     II : is-bounded-by k γ
     II n = ≤-trans (β (n₀ + n)) (β n₀) k (is-decreasing'' β δ n₀ n) I

     III : is-decreasing' γ
     III n = δ (n₀ + n)

\end{code}

With this, we can complete the definition of the forward direction,
but also notice that the above constructions and lemmas will also be
useful to prove that it has a two-sided inverse.

\begin{code}

  f : 𝔹 (succ k) → 𝔻 (𝔹 k)
  f 𝕓 = u-of 𝕓 , π-of 𝕓

\end{code}

For the backward direction we again start with some auxiliary
constructions and lemmas.

\begin{code}

  module _ (n : ℕ) (u : ℕ∞) (e : ι u n ＝ ₀) where

   φ-of : is-finite u
   φ-of = case ℕ-to-ℕ∞-lemma fe u n e of
           λ (m , _ , p) → (m , (p ⁻¹))

   d-of : ℕ
   d-of = case ℕ-to-ℕ∞-lemma fe u n e of
           λ (m , le , _) → pr₁ (subtraction m n le)

   φd-property : d-of + size φ-of ＝ n
   φd-property = case ℕ-to-ℕ∞-lemma fe u n e of
                  λ (m , le , _) → pr₂ (subtraction m n le)

  module _ (u : ℕ∞) (π : is-finite u → 𝔹 k) (n : ℕ) where

   β-of : ℕ
   β-of = 𝟚-equality-cases
           (λ (e : ι u n ＝ ₀) → ι (π (φ-of n u e)) (d-of n u e))
           (λ (_ : ι u n ＝ ₁) → succ k)

   β-of-at-₀ : (e : ι u n ＝ ₀)
             → β-of ＝ ι (π (φ-of n u e)) (d-of n u e)
   β-of-at-₀ = 𝟚-equality-cases₀

   β-of-at-₁ : ι u n ＝ ₁
             → β-of ＝ succ k
   β-of-at-₁ = 𝟚-equality-cases₁

  β-of-at-finite : (u : ℕ∞)
                   (π : is-finite u → 𝔹 k)
                   (n : ℕ)
                   (φ@(n₀ , e₀) : is-finite u)
                   (e : ι u (n₀ + n) ＝ ₀)
                 → β-of u π (n₀ + n) ＝ ι (π φ) n
  β-of-at-finite u π n φ@(n₀ , e₀) e =
   β-of u π (n₀ + n) ＝⟨ β-of-at-₀ u π (n₀ + n) e ⟩
   ι (π φ') d        ＝⟨ ap (ι (π φ')) IV ⟩
   ι (π φ') n        ＝⟨ ap (λ - → ι (π -) n) I ⟩
   ι (π φ) n         ∎
    where
     φ' : is-finite u
     φ' = φ-of (n₀ + n) u e

     d : ℕ
     d = d-of (n₀ + n) u e

     I : φ' ＝ φ
     I = being-finite-is-prop fe u _ _

     II : size φ' ＝ n₀
     II = ap size I

     III = n₀ + d      ＝⟨ addition-commutativity n₀ d ⟩
           d + n₀      ＝⟨ ap (d +_) (II ⁻¹) ⟩
           d + size φ' ＝⟨ φd-property (n₀ + n) u e ⟩
           n₀ + n      ∎

     IV : d ＝ n
     IV = addition-left-cancellable d n n₀ III

  β-of-bounded : (u : ℕ∞)
                 (π : is-finite u → 𝔹 k)
               → is-bounded-by (succ k) (β-of u π)
  β-of-bounded u π n = 𝟚-equality-cases bounded₀ bounded₁
   where
    bounded₀ : ι u n ＝ ₀ → β-of u π n ≤ succ k
    bounded₀ e = transport (_≤ succ k) (I ⁻¹) III
     where
      φ : is-finite u
      φ = φ-of n u e

      d : ℕ
      d = d-of n u e

      I : β-of u π n ＝ ι (π φ) d
      I = β-of-at-₀ u π n e

      II : ι (π φ) d ≤ k
      II = 𝔹-is-bounded-by (π φ) d

      III : ι (π φ) d ≤ succ k
      III = ≤-trans (ι (π φ) d) k (succ k) II (≤-succ k)

    bounded₁ : ι u n ＝ ₁ → β-of u π n ≤ succ k
    bounded₁ p = transport (_≤ succ k) ((β-of-at-₁ u π n p) ⁻¹) (≤-refl (succ k))

  β-of-decreasing' : (u : ℕ∞) (π : is-finite u → 𝔹 k)
                   → is-decreasing' (β-of u π)
  β-of-decreasing' u π n = 𝟚-equality-cases I₀ I₁
   where
    I₀ : ι u (succ n) ＝ ₀ → β-of u π (succ n) ≤ β-of u π n
    I₀ z' = 𝟚-equality-cases
             (λ (z : ι u n ＝ ₀) → II₀ z' z)
             (λ (p : ι u n ＝ ₁) → II₁ z' p)
     where
      II₀ : ι u (succ n) ＝ ₀
          → ι u n ＝ ₀
          → β-of u π (succ n) ≤ β-of u π n
      II₀ e' e = transport₂ _≤_ (III' ⁻¹) (III ⁻¹) XIV
       where
        φ' : is-finite u
        φ' = φ-of (succ n) u z'

        d' : ℕ
        d' = d-of (succ n) u z'

        φ : is-finite u
        φ = φ-of n u e

        d : ℕ
        d = d-of n u e

        III' : β-of u π (succ n) ＝ ι (π φ') d'
        III' = β-of-at-₀ u π (succ n) z'

        III : β-of u π n ＝ ι (π φ) d
        III = β-of-at-₀ u π n e

        IV : φ' ＝ φ
        IV = being-finite-is-prop fe u φ' φ

        V : ι (π φ') ＝ ι (π φ)
        V = ap (λ - → ι (π -)) IV

        m  = size φ
        m' = size φ'

        VI : m' ＝ m
        VI = ap size IV

        VII : d + m ＝ n
        VII = φd-property n u e

        VIII : d' + m' ＝ succ n
        VIII = φd-property (succ n) u z'

        IX : d' + m ＝ succ n
        IX = transport (λ - → d' + - ＝ succ n) VI VIII

        X = d' + m       ＝⟨ IX ⟩
            succ n       ＝⟨ ap succ (VII ⁻¹) ⟩
            succ (d + m) ＝⟨ succ-left d m ⁻¹ ⟩
            succ d + m   ∎

        XI : d' ＝ succ d
        XI = addition-right-cancellable d' (succ d) m X

        XII : is-decreasing' (ι (π φ))
        XII = 𝔹-is-decreasing' (π φ)

        XIII = ι (π φ') d'       ＝⟨ ap (ι (π φ')) XI ⟩
               ι (π φ') (succ d) ＝⟨ ap (λ - → - (succ d)) V ⟩
               ι (π φ)  (succ d) ∎

        XIV : ι (π φ') d' ≤ ι (π φ) d
        XIV = transport (_≤ ι (π φ) d) (XIII ⁻¹) (XII d)

      II₁ : ι u (succ n) ＝ ₀ → ι u n ＝ ₁
          → β-of u π (succ n) ≤ β-of u π n
      II₁ z' p = transport (_≤ β-of u π n) (III ⁻¹) VI
       where
        φ' : is-finite u
        φ' = φ-of (succ n) u z'

        d' : ℕ
        d' = d-of (succ n) u z'

        III : β-of u π (succ n) ＝ ι (π φ') d'
        III = β-of-at-₀ u π (succ n) z'

        IV : ι (π φ') d' ≤ k
        IV = pr₁ (pr₂ (π φ')) d'

        V : β-of u π n ＝ succ k
        V = β-of-at-₁ u π n p

        VI : ι (π φ') d' ≤ β-of u π n
        VI = transport
              (ι (π φ') d' ≤_)
              (V ⁻¹)
              (≤-trans (ι (π φ') d') k (succ k) IV (≤-succ k))

    I₁ : ι u (succ n) ＝ ₁ → β-of u π (succ n) ≤ β-of u π n
    I₁ p' = 𝟚-equality-cases
             (λ (e : ι u n ＝ ₀)
                   → 𝟘-elim
                      (zero-is-not-one
                       (₀     ＝⟨ e ⁻¹ ⟩
                        ι u n ＝⟨ ≤₂-criterion-converse (pr₂ u n) p' ⟩
                        ₁     ∎)))
             (λ (p : ι u n ＝ ₁)
                   → transport₂ _≤_
                      ((β-of-at-₁ u π (succ n) p') ⁻¹)
                      ((β-of-at-₁ u π n p) ⁻¹)
                      (≤-refl (succ k)))

\end{code}

With this we can define an inverse g of the function f defined above.

\begin{code}

  g : 𝔻 (𝔹 k) → 𝔹 (succ k)
  g (u , π) = β-of u π , β-of-bounded u π , β-of-decreasing' u π

\end{code}

To conclude, we now show that f and g are indeed mutually inverse.

\begin{code}

  gf : g ∘ f ∼ id
  gf 𝕓@(β , _ , _) = to-𝔹-＝ _ _ I
   where
    u : ℕ∞
    u = u-of 𝕓

    π : is-finite u → 𝔹 k
    π = π-of 𝕓

    I : (n : ℕ) → β-of u π n ＝ β n
    I n = 𝟚-equality-cases I₀ I₁
     where
      I₀ : ι u n ＝ ₀ → β-of u π n ＝ β n
      I₀ e =
       β-of u π n                      ＝⟨ β-of-at-₀ u π n e ⟩
       ι (π (φ-of n u e)) (d-of n u e) ＝⟨ refl ⟩
       β (m + d)                       ＝⟨ ap β II ⟩
       β n                             ∎
       where
        m : ℕ
        m = size (φ-of n u e)

        d : ℕ
        d = d-of n u e

        II = m + d ＝⟨ addition-commutativity m d ⟩
             d + m ＝⟨ φd-property n u e ⟩
             n     ∎

      I₁ : ι u n ＝ ₁ → β-of u π n ＝ β n
      I₁ p = β-of u π n ＝⟨ β-of-at-₁ u π n p ⟩
             succ k     ＝⟨ (α-of-₁-converse β n p) ⁻¹ ⟩
             β n        ∎

  fg : f ∘ g ∼ id
  fg 𝕕@(u , π) = to-Σ-＝ (IV , V)
   where
    β : ℕ → ℕ
    β = β-of u π

    I : is-bounded-by (succ k) β
    I = β-of-bounded u π

    II : is-decreasing' β
    II = β-of-decreasing' u π

    𝕕' : 𝔻 (𝔹 k)
    𝕕' = f (g 𝕕)

    u' : ℕ∞
    u' = 𝔻-time 𝕕'

    π' : is-finite u' → 𝔹 k
    π' = 𝔻-value 𝕕'

    III : (n : ℕ) → α-of β n ＝ ι u n
    III n = 𝟚-equality-cases III₀ III₁
     where
      III₀ : ι u n ＝ ₀ → α-of β n ＝ ι u n
      III₀ e = α-of β n  ＝⟨ α-of-₀-converse β n ⦅4⦆ ⟩
               ₀         ＝⟨ e ⁻¹ ⟩
               ι u n     ∎
       where
        φ : is-finite u
        φ = φ-of n u e

        d : ℕ
        d = d-of n u e

        ⦅1⦆ : β n ＝ ι (π φ) d
        ⦅1⦆ = β-of-at-₀ u π n e

        ⦅2⦆ : ι (π φ) d ≤ k
        ⦅2⦆ = pr₁ (pr₂ (π φ)) d

        ⦅3⦆ : β n ≤ k
        ⦅3⦆ = transport (_≤ k) (⦅1⦆ ⁻¹) ⦅2⦆

        ⦅4⦆ : β n ≠ succ k
        ⦅4⦆ r = not-less-than-itself k (transport (_≤ k) r ⦅3⦆)

      III₁ : ι u n ＝ ₁ → α-of β n ＝ ι u n
      III₁ p = α-of β n  ＝⟨ α-of-₁ β n (β-of-at-₁ u π n p) ⟩
               ₁         ＝⟨ p ⁻¹ ⟩
               ι u n     ∎

    IV : u' ＝ u
    IV = ℕ∞-to-ℕ→𝟚-lc fe (dfunext fe III)

    V : transport (λ - → is-finite - → 𝔹 k) IV π' ＝ π
    V = dfunext fe V₁
     where
      module _ (φ@(n₀ , e₀) : is-finite u) where

       φ' φ'' : is-finite u'
       φ'  = n₀ , (e₀ ∙ IV ⁻¹)
       φ'' = transport is-finite (IV ⁻¹) φ

       V₀ : (n : ℕ) → ι (π' φ') n ＝ ι (π φ) n
       V₀ n = ι (π' φ') n ＝⟨ refl ⟩
              β (n₀ + n)  ＝⟨ β-of-at-finite u π n φ (+-stays-zero u n₀ e₀ n) ⟩
              ι (π φ) n   ∎

       V₁ = transport (λ - → is-finite - → 𝔹 k) IV π' φ ＝⟨ ⦅1⦆ ⟩
            π' φ''                                      ＝⟨ ⦅2⦆ ⟩
            π' φ'                                       ＝⟨ ⦅3⦆ ⟩
            π φ                                         ∎
        where
         ⦅1⦆ = transport-is-finite IV π' φ
         ⦅2⦆ = ap π' (being-finite-is-prop fe u' φ'' φ')
         ⦅3⦆ = to-𝔹-＝ _ _ V₀

\end{code}