Martin Escardo, August 2026

The Brouwer ordinal codes are embedded into the inductive-recursive
universe E of ordinal codes of the module
Ordinals.InductiveRecursiveCodesInterpretations.

The embedding commutes with both the discrete and the compact
interpretations, in each case up to order equivalence rather than on
the nose.

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt

module Ordinals.BrouwerCodesIntoInductiveRecursiveCodes
        (fe : FunExt)
       where

open import CoNaturals.Type
open import MLTT.Plus-Properties
open import Notation.CanonicalMap hiding (ΞΉ)
open import Ordinals.Arithmetic fe
open import Ordinals.BrouwerCodes
open import Ordinals.BrouwerCodesDiscreteAndCompactInterpretations fe
       using (Ξ” ; Κ)
open import Ordinals.Closure fe
open import Ordinals.Equivalence
open import Ordinals.InductiveRecursiveCodesInterpretations fe
       using (E ; βŒœπŸ™βŒ ; βŒœΟ‰+πŸ™βŒ ; _⌜+⌝_ ; _βŒœΓ—βŒ_ ; ⌜Σ⌝ ; E-is-set ; π“š)
       renaming (Ξ” to Ξ”α΄± ; Κ to Κᴱ)
open import Ordinals.Injectivity
open import Ordinals.ToppedArithmetic fe
open import Ordinals.ToppedType fe
open import Ordinals.Type
open import Ordinals.Underlying
open import TypeTopology.SquashedSum fe
open import UF.Base
open import UF.Embeddings
open import UF.Equiv

open topped-ordinals-injectivity fe

private
 feβ‚€ : funext 𝓀₀ 𝓀₀
 feβ‚€ = fe 𝓀₀ 𝓀₀

\end{code}

The translation of the limit constructor works because the discrete
interpretation of the code for Ο‰ + 1 has underlying type β„• + πŸ™, which
is exactly the index that βˆ‘β‚ sums over, so that the family can be
given by cases, with the added point sent to the code for πŸ™.

\begin{code}

B-to-E : B β†’ E
B-to-E Z     = βŒœπŸ™βŒ
B-to-E (S b) = B-to-E b ⌜+⌝ βŒœπŸ™βŒ
B-to-E (L b) = ⌜Σ⌝ βŒœΟ‰+πŸ™βŒ (cases (Ξ» n β†’ B-to-E (b n)) (Ξ» _ β†’ βŒœπŸ™βŒ))

B-to-E-lc : left-cancellable B-to-E
B-to-E-lc {Z}   {Z}    p = refl
B-to-E-lc {S b} {S b'} p = ap S (B-to-E-lc (ap plus-left p))
 where
  plus-left : E β†’ E
  plus-left βŒœπŸ™βŒ       = βŒœπŸ™βŒ
  plus-left βŒœΟ‰+πŸ™βŒ     = βŒœπŸ™βŒ
  plus-left (ν ⌜+⌝ μ) = ν
  plus-left (Ξ½ βŒœΓ—βŒ ΞΌ) = βŒœπŸ™βŒ
  plus-left (⌜Σ⌝ Ξ½ A) = βŒœπŸ™βŒ
B-to-E-lc {L b} {L b'} p = ap L (dfunext feβ‚€ I)
 where
  sigma-family : E β†’ (β„• + πŸ™ β†’ E)
  sigma-family βŒœπŸ™βŒ                = Ξ» _ β†’ βŒœπŸ™βŒ
  sigma-family βŒœΟ‰+πŸ™βŒ              = Ξ» _ β†’ βŒœπŸ™βŒ
  sigma-family (Ξ½ ⌜+⌝ ΞΌ)          = Ξ» _ β†’ βŒœπŸ™βŒ
  sigma-family (Ξ½ βŒœΓ—βŒ ΞΌ)          = Ξ» _ β†’ βŒœπŸ™βŒ
  sigma-family (⌜Σ⌝ βŒœπŸ™βŒ A)        = Ξ» _ β†’ βŒœπŸ™βŒ
  sigma-family (⌜Σ⌝ βŒœΟ‰+πŸ™βŒ A)      = A
  sigma-family (⌜Σ⌝ (Ξ½ ⌜+⌝ ΞΌ) A)  = Ξ» _ β†’ βŒœπŸ™βŒ
  sigma-family (⌜Σ⌝ (Ξ½ βŒœΓ—βŒ ΞΌ) A)  = Ξ» _ β†’ βŒœπŸ™βŒ
  sigma-family (⌜Σ⌝ (⌜Σ⌝ Ξ½ A) A') = Ξ» _ β†’ βŒœπŸ™βŒ

  I : (n : β„•) β†’ b n ＝ b' n
  I n = B-to-E-lc (happly (ap sigma-family p) (inl n))

\end{code}

Since the inductive-recursive universe is a set, this makes the
inclusion an embedding.

\begin{code}

B-to-E-is-embedding : is-embedding B-to-E
B-to-E-is-embedding = lc-maps-into-sets-are-embeddings
                       B-to-E
                       B-to-E-lc
                       E-is-set

\end{code}

The inclusion commutes with the discrete interpretations, up to order
equivalence.

\begin{code}

Ξ”-agreement : (b : B) β†’ [ Ξ” b ] ≃ₒ [ Ξ”α΄± (B-to-E b) ]
Ξ”-agreement Z     = ≃ₒ-refl [ πŸ™α΅’ ]
Ξ”-agreement (S b) = βˆ‘-≃ₒ
                     πŸšα΅’
                     (cases (Ξ» _ β†’ Ξ” b) (Ξ» _ β†’ πŸ™α΅’))
                     (cases (Ξ» _ β†’ Ξ”α΄± (B-to-E b)) (Ξ» _ β†’ πŸ™α΅’))
                     (dep-cases
                       (Ξ» _ β†’ Ξ”-agreement b)
                       (Ξ» _ β†’ ≃ₒ-refl [ πŸ™α΅’ ]))
Ξ”-agreement (L b) = βˆ‘-≃ₒ
                     (succβ‚’ Ο‰)
                     ((Ξ” ∘ b) β†— (over , over-embedding))
                     (Ξ”α΄± ∘ cases (Ξ» n β†’ B-to-E (b n)) (Ξ» _ β†’ βŒœπŸ™βŒ))
                     I
 where
  I : (z : β„• + πŸ™)
    β†’ [ ((Ξ” ∘ b) β†— (over , over-embedding)) z ]
    ≃ₒ [ Ξ”α΄± (cases (Ξ» n β†’ B-to-E (b n)) (Ξ» _ β†’ βŒœπŸ™βŒ) z) ]
  I (inl n) = ≃ₒ-trans
               [ ((Ξ” ∘ b) β†— (over , over-embedding)) (inl n) ]
               [ Ξ” (b n) ]
               [ Ξ”α΄± (B-to-E (b n)) ]
               (β†—-propertyβ‚’ (Ξ” ∘ b) (over , over-embedding) n)
               (Ξ”-agreement (b n))
  I (inr ⋆) = β†—-out-of-range
               (Ξ” ∘ b)
               (over , over-embedding)
               (inr ⋆)
               (Ξ» n β†’ +disjoint)

\end{code}

The inclusion also commutes with the compact interpretations.

\begin{code}

Κ-agreement : (b : B) β†’ [ Κ b ] ≃ₒ [ Κᴱ (B-to-E b) ]
Κ-agreement Z     = ≃ₒ-refl [ πŸ™α΅’ ]
Κ-agreement (S b) = βˆ‘-≃ₒ
                     πŸšα΅’
                     (cases (Ξ» _ β†’ Κ b) (Ξ» _ β†’ πŸ™α΅’))
                     (cases (Ξ» _ β†’ Κᴱ (B-to-E b)) (Ξ» _ β†’ πŸ™α΅’))
                     (dep-cases
                       (Ξ» _ β†’ Κ-agreement b)
                       (Ξ» _ β†’ ≃ₒ-refl [ πŸ™α΅’ ]))
Κ-agreement (L b) = βˆ‘-≃ₒ β„•βˆžα΅’ ((Κ ∘ b) β†— embedding-β„•-to-β„•βˆž feβ‚€) (π“š βŒœΟ‰+πŸ™βŒ A) I
 where
  A : β„• + πŸ™ β†’ E
  A = cases (Ξ» n β†’ B-to-E (b n)) (Ξ» _ β†’ βŒœπŸ™βŒ)

  ΞΊ ΞΊα΄± : β„• β†’ Ordinal 𝓀₀
  κ  n = [ Κ (b n) ]
  κᴱ n = [ Κᴱ (B-to-E (b n)) ]

  h : (n : β„•) β†’ ⟨ ΞΊ n ⟩ β†’ ⟨ ΞΊα΄± n ⟩
  h n = ≃ₒ-to-fun (ΞΊ n) (ΞΊα΄± n) (Κ-agreement (b n))

  h⁻¹ : (n : β„•) β†’ ⟨ ΞΊα΄± n ⟩ β†’ ⟨ ΞΊ n ⟩
  h⁻¹ n = ≃ₒ-to-fun⁻¹ (ΞΊ n) (ΞΊα΄± n) (Κ-agreement (b n))

  he : (n : β„•) β†’ is-order-equiv (ΞΊ n) (ΞΊα΄± n) (h n)
  he n = ≃ₒ-to-fun-is-order-equiv (ΞΊ n) (ΞΊα΄± n) (Κ-agreement (b n))

  hi : (n : β„•) β†’ is-equiv (h n)
  hi n = order-equivs-are-equivs (ΞΊ n) (ΞΊα΄± n) (he n)

  I : (u : β„•βˆž)
    β†’ [ ((Κ ∘ b) β†— embedding-β„•-to-β„•βˆž feβ‚€) u ] ≃ₒ [ π“š βŒœΟ‰+πŸ™βŒ A u ]
  I u = f ,
        order-preserving-reflecting-equivs-are-order-equivs
         [ ((Κ ∘ b) β†— embedding-β„•-to-β„•βˆž feβ‚€) u ]
         [ π“š βŒœΟ‰+πŸ™βŒ A u ]
         f
         f-is-equiv
         f-is-order-preserving
         f-is-order-reflecting
   where
    f : ⟨ ((Κ ∘ b) β†— embedding-β„•-to-β„•βˆž feβ‚€) u ⟩ β†’ ⟨ π“š βŒœΟ‰+πŸ™βŒ A u ⟩
    f Ο† (inl n , p) = h n (Ο† (n , p))
    f Ο† (inr ⋆ , p) = ⋆

    g : ⟨ π“š βŒœΟ‰+πŸ™βŒ A u ⟩ β†’ ⟨ ((Κ ∘ b) β†— embedding-β„•-to-β„•βˆž feβ‚€) u ⟩
    g ψ (n , p) = h⁻¹ n (ψ (inl n , p))

    gf : g ∘ f ∼ id
    gf Ο† = dfunext feβ‚€
            (Ξ» (n , p) β†’ inverses-are-retractions (h n) (hi n) (Ο† (n , p)))

    fg : f ∘ g ∼ id
    fg ψ = dfunext feβ‚€ Ξ³
     where
      Ξ³ : (w : fiber ΞΉπŸ™ u) β†’ f (g ψ) w ＝ ψ w
      γ (inl n , p) = inverses-are-sections (h n) (hi n) (ψ (inl n , p))
      Ξ³ (inr ⋆ , p) = refl

    f-is-equiv : is-equiv f
    f-is-equiv = qinvs-are-equivs f (g , gf , fg)

    f-is-order-preserving : is-order-preserving
                             (((Κ ∘ b) β†— embedding-β„•-to-β„•βˆž feβ‚€) u)
                             (π“š βŒœΟ‰+πŸ™βŒ A u)
                             f
    f-is-order-preserving Ο† Ο†' ((n , p) , l) =
     (inl n , p) ,
     order-equivs-are-order-preserving (ΞΊ n) (ΞΊα΄± n) (he n)
      (Ο† (n , p)) (Ο†' (n , p)) l

    f-is-order-reflecting : is-order-reflecting
                             (((Κ ∘ b) β†— embedding-β„•-to-β„•βˆž feβ‚€) u)
                             (π“š βŒœΟ‰+πŸ™βŒ A u)
                             f
    f-is-order-reflecting Ο† Ο†' ((inl n , p) , l) =
     (n , p) ,
     order-equivs-are-order-reflecting (ΞΊ n) (ΞΊα΄± n) (h n) (he n)
      (Ο† (n , p)) (Ο†' (n , p)) l
    f-is-order-reflecting Ο† Ο†' ((inr ⋆ , p) , l) = 𝟘-elim l

\end{code}