The counting tools for infinite constructible stages

Counting the stage Lset δ of an infinite ordinal δ inside L rests on two ingredients: a base injection Lω ↪ ω, and a way of lifting injections through finite environments. This chapter supplies both, and everything here is proved for exactly the constructs named in the text.

{-# OPTIONS --cubical --safe --guardedness #-}

The chapter works under excluded middle at the fixed universe level. This hypothesis is inherited by the constructions used throughout; its clearest local roles are to search a finite-stage tally for a name and to compare a collapse value with ω by ordinal trichotomy.

open import Base.Prelude
open import Base.Classical using ( LEM )

All constructions therefore share the single hypothesis lem : LEM (ℓ-suc ℓ). In particular, the finite search below is a consequence of excluded middle and does not invoke a choice principle.

module L.GCH.StageCountingTools {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

The internal graphs used below must be described by formulas that L itself can interpret. Equality, membership, conjunction, implication, and bounded and unbounded quantifiers provide the language for saying that a relation is a total single-valued injection and for defining its action on finite environments.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _≐_; _∈̇_; _∧̇_; _⇒̇_; ∃̇_; ∀̇_; ∀̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

There are two levels of data throughout the argument. A set in the cumulative hierarchy has a small presentation whose indices name its members, while an element of L also carries a proof of constructibility. Moving between these levels lets an internal graph act as an ordinary function on presentation indices.

open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Model {ℓ} using ( ∈sucV-inl; self∈sucV )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; #mono )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset→isL )

Ordinal structure enters twice. Numerals identify the finite domains of environments, while the order on constructible stages later gives a canonical well order of Lset ω. Trichotomy will then decide how each value of its ordinal collapse sits relative to ω.

open import L.Ordinal {ℓ} using ( ∈#-elim; mem-ord; ω-ord; numeral-ord; #∈ω )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )

A coded injection is represented by a set of ordered pairs. Its four obligations say that the graph is single-valued, has exactly the stated domain, is injective on inputs, and takes values in the stated target. The first part of the chapter starts from such an actual coded graph.

open import L.Coding.Model {ℓ} using ( prʟ; prʟ-fst; svAt; svAt-in; svAt-out; domAt; domAt-in; domAt-out; domAt-intro; appAt; appAt-adequate; envOverAt; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( numL )
open import L.Coding.Injection {ℓ} lem
  using ( injAt; injAt-in; injAt-out; module Small )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )

For each natural number n, the set of environments over A of length n has a concrete presentation. The union seqL A ranges over every finite length. Thus an entrywise map that preserves length is exactly the operation needed to map all finite sequences over A into those over B.

open import L.Coding.EnvironmentSet {ℓ} lem
  using ( Ix; envS; envSet-in; envSet-out; envOver; module Recover )
open import L.Choice.NameComparison {ℓ} lem using ( domAt-numeral; domAt-fill )
open import L.Choice.StageOrders {ℓ} lem
  using ( carry; memOf; orderAt; orderAt-step; relOf

The second part orders the members of Lset ω first by birth stage and then, when birth stages agree, by the local step order. This distinction matters: a predecessor may have the same birth stage as its successor, although every predecessor still lies in the successor of that common stage.

        ; birth-mem; module Family )
  renaming ( Mem to MemOf )
open import L.Choice.OrderTable {ℓ} lem using ( Related; IsRel; ixRel-rep; ixRel-fill )
open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-spec )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}

Collapsing this well order assigns an ordinal to each member of Lset ω. The task is then to prove that every collapse value belongs to ω. The proof will bound one predecessor segment at a time by a finite constructible stage and rule out an injection of ω into that stage.

  using ( SWO; lt; eq; gt ) renaming ( Tri to TriW )
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )

Finite-sequence coding and the collapse argument meet in later cardinal calculations. The former transports an already given coded injection coordinatewise; the latter provides the base result Lset ω ↪ ω. Neither statement asserts a bijection or counts arbitrary infinite sequences.

open import L.GCH.CardinalSquareLaw {ℓ} lem using ( isL-ord )
open import L.GCH.FiniteSequenceCoding {ℓ} lem using ( seqL; seqL-in; seqL-out )
open import L.Ordinal.SquareLaw {ℓ} lem using ( module FiniteBase )
open FiniteBase using ( fromFin; fromFin-inj )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate; ω-limit; finite-excl-ω )

A finite stage comes with a finite tally that lists all its members. Repetitions may occur, so the tally is a surjective naming device rather than a bijection. This is enough: excluded middle permits a bounded search for one name of each given member.

open import L.Choice.FiniteStageOrders {ℓ} lem
  using ( Tally; StageOrder; stageOrder; finiteStage )  -- lint-agda: keep (StageOrder used as the projection qualifier)
open import L.GCH.OrderType {ℓ} lem using ( Holds; module Code )

The chosen tally index places each member of a finite stage in a finite ordinal presentation. Composing a hypothetical injection from ω with this naming map, and then duplicating the result on the diagonal, contradicts the finite square exclusion theorem.

open import Cubical.Data.Nat.Order using ( _<_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.FinSet using ( DecΣ )
open import Cubical.Relation.Nullary using ( decRec; yes; no )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId'; inj-toℕ )

Several later equalities concern dependent pairs whose second components are proofs. Since those components are propositions, equality of the underlying sets determines equality of the packaged elements. This allows the argument to move cleanly between elements of L, their presentations, and their graph codes.

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ2; isPropΠ3 )

Numerals have a second role besides marking environment lengths. Membership in ω says merely that an ambient set is equal to some numeral, while the proof keeps no globally chosen natural-number representative. Later eliminations respect this propositional character.

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; ω; sucV )

Existence in membership and graph readings is often retained only under propositional truncation ∥_∥₁. Such a witness may be eliminated when the target is a proposition, or when uniqueness first makes the target type a proposition; the operation does not select arbitrary representatives.

open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

The same distinction applies to the final count. InjL A B retains only the proposition that some constructible graph codes an injection from A to B; it does not expose a globally selected host-level function.

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

By contrast, the sequence construction begins with a particular graph E and the full data InjCode E A B. Its host-level function can therefore be read from that graph and used coordinatewise before the resulting graph is hidden again by InjL.

module SV = hPropStructure 𝒮ᵥ using ()

Every entry read from a member of a constructible set is itself constructible, by transitivity of L. This elementary fact is what permits finite environments and the ordered pairs in their graphs to remain objects of the internal model.

module SL = hPropStructure 𝒮ʟ using ( S )
open SL using ( S )

Satisfaction notation connects the formula-level description of a graph with these ambient membership facts. Adequacy lemmas will be used in both directions, so the proof can build an internal formula from concrete graph data and later read that formula back.

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )

For a natural number k, nn k packages the numeral # k with its proof of constructibility. These packaged numerals serve as the finite domain objects in satisfaction environments.

nn : ℕ → S
nn k = # k , numL k

The graph formula below introduces several nested binders. Names i0, i1, and so on abbreviate their de Bruijn positions, with i0 always denoting the most recently bound variable.

private
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc i0

As binders are added, older variables shift to the next position. The typed abbreviations record those shifts once, so the formula can display its mathematical pattern without repeating long successor expressions.

  i2 : ∀ {k} → Fin (suc (suc (suc k)))
  i2 = suc i1
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc i2
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))

The positions through i6 will suffice to relate an input environment s, its image y, a common domain n, an index i, and the two entries connected by E.

  i4 = suc i3
  i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
  i5 = suc i4
  i6 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc k)))))))
  i6 = suc i5

Later formulas for coded injections require a few deeper positions. Extending the same naming scheme avoids changing the convention when those additional binders are introduced.

  i7 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc k))))))))
  i7 = suc i6
  i8 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc (suc k)))))))))
  i8 = suc i7
  i9 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc k))))))))))

The last abbreviation completes the range needed in this module. These names carry no mathematical assumptions; they only keep the variable bookkeeping legible.

  i9 = suc i8

Length and extensionality of environments

The first rigidity fact compares the lengths of two coded environments. If one underlying set equals both environments env h and env h', with every entry constructible, then the two lengths are equal: the domain of a coded environment is its length numeral, and the two readings of the same set are identified by the numeral projections.

env-len : (E : S) {n n' : ℕ} (h : Fin n → V ℓ) (h' : Fin n' → V ℓ)
        → ((i : Fin n) → ⟨ isL (h i) ⟩) → ((i : Fin n') → ⟨ isL (h' i) ⟩)
        → fst E ≡ env h → fst E ≡ env h' → n ≡ n'
env-len E {n} {n'} h h' cg cg' q q' =
  #-inj′ (domAt-numeral (suc zero) zero (nn n ∷ E ∷ []) n' h' cg' q'

The proof fills the domain of the first presentation with the numeral of n, reads the same domain back as the numeral of n', and applies the injectivity of numerals. The conclusion is only the equality of lengths, not an equality of the two presenting functions.

            (domAt-fill (suc zero) zero (nn n ∷ E ∷ []) n h cg q refl))

The second rigidity fact assumes that two columns already have the same length and their coded graphs are equal. Looking up the numeral key for an index in both graphs then recovers equality of the corresponding entries. The converse, constructing equality of graphs from pointwise equality, is proved later at the place where it is needed.

env-pt : {n : ℕ} (h h' : Fin n → V ℓ) → env h ≡ env h' → (i : Fin n) → h i ≡ h' i
env-pt h h' q i = subst ⟨_⟩ (lookup-spec h' i (h i))
  (subst (λ w → ⟨ pr (# (toℕ i)) (h i) ∈ w ⟩) q
    (subst ⟨_⟩ (sym (lookup-spec h i (h i))) refl))

Lifting a coded injection to finite sequences

The lifting module is stated for a constructible graph E with four data: single-valuedness, totality on A, injectivity on A, and values in B. These are exactly the four clauses of a coded injection from A into B.

module SeqMap (A B E : S)
              (sv : ⟨ (E ∷ A ∷ []) ⊨ svAt zero ⟩)
              (dm : ⟨ (E ∷ A ∷ []) ⊨ domAt zero (suc zero) ⟩)
              (ij : ⟨ (E ∷ A ∷ []) ⊨ injAt zero ⟩)
              (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst E ⟩

The final range clause says only that every value occurring in E belongs to B. It does not require every member of B to occur, so the data describe an injection rather than a surjection or a bijection.

                   → ⟨ fst y ∈ fst B ⟩) where

The extraction machinery reads the internal graph as an actual function between the presentations of A and B: single-valuedness makes the fiber of each value a proposition, so the value can be recovered without any choice principle.

  module Sm = Small E A B sv dm ij ran using ( at; fib; small; small-inj; module E )

The extracted function is kept opaque: later arguments use it through its graph and its injectivity.

  opaque
    f : ⟪ fst A ⟫ → ⟪ fst B ⟫
    f = Sm.small

The graph record states that the pair of an index's presented element and the presented image belongs to E; it is transported from the term algebra's own graph record along the identification of the presented value.

    f-graph : (m : ⟪ fst A ⟫)
            → ⟨ pr (⟪ fst A ⟫↪ m) (⟪ fst B ⟫↪ (f m)) ∈ fst E ⟩
    f-graph m = subst (λ w → ⟨ pr (⟪ fst A ⟫↪ m) w ∈ fst E ⟩)
      (sym (Sm.fib m .snd)) (Sm.E.toFun-graph (Sm.at m))

The extracted function is injective on the presentation of A, which is the pointwise injectivity that the sequence lifting will inherit.

    f-inj : (m n : ⟪ fst A ⟫) → f m ≡ f n → m ≡ n
    f-inj = Sm.small-inj

An environment entry of A is read as an ambient set through the embedding of the presentation.

  vA : {n : ℕ} → Ix A n → Fin n → V ℓ
  vA g i = ⟪ fst A ⟫↪ (g i)

Likewise for the entries of B-environments.

  vB : {n : ℕ} → Ix B n → Fin n → V ℓ
  vB h i = ⟪ fst B ⟫↪ (h i)

The lifted assignment applies the extracted function entry by entry: the image of a length-n environment of A is a length-n environment of B, so lengths never change.

  fg : {n : ℕ} → Ix A n → Ix B n
  fg g i = f (g i)

Every entry of an A-environment is constructible, by transporting the membership in A along the transitivity of constructibility.

  isLA : {n : ℕ} (g : Ix A n) (i : Fin n) → ⟨ isL (vA g i) ⟩
  isLA g i = isL-trans (member (fst A) (g i)) (snd A)

Likewise for the entries of B-environments.

  isLB : {n : ℕ} (h : Ix B n) (i : Fin n) → ⟨ isL (vB h i) ⟩
  isLB h i = isL-trans (member (fst B) (h i)) (snd B)

For an index object i, Ent y s i says merely that there are model elements u and v such that s(i)=u, y(i)=v, and the graph E sends u to v. The witnesses and all three graph-membership facts are kept under propositional truncation.

  Ent : (y s i : S) → Type (ℓ-suc ℓ)
  Ent y s i = ∥ Σ[ u ∈ S ] Σ[ v ∈ S ]
      ( ⟨ pr (fst i) (fst u) ∈ fst s ⟩
      × ⟨ pr (fst i) (fst v) ∈ fst y ⟩
      × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ ) ∥₁

The host reading Wit y s says merely that some object n is the domain of s, that y is an environment over the fixed target B with that same domain, and that every i∈n satisfies Ent y s i. Thus y has the same finite shape as s, and its entries are the pointwise E-images of those of s.

  Wit : (y s : S) → Type (ℓ-suc ℓ)
  Wit y s = ∥ Σ[ n ∈ S ]
      ( ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
      × ⟨ (B ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
      × ((i : S) → ⟨ fst i ∈ fst n ⟩ → Ent y s i) ) ∥₁

The entry formula expresses exactly the three equations hidden in Ent: two existentially bound values u and v satisfy s(i)=u, y(i)=v, and E(u)=v. The variable positions account for the surrounding parameters and the two new witnesses.

  opaque
    private
      entFo : Formula S 
      entFo = ∃̇ (∃̇ ( appAt i6 i2 i1 ∧̇ appAt i5 i2 i0 ∧̇ appC E i1 i0 ))

The full formula first binds the common domain n, then binds an object b and requires it to equal the fixed constant B. It says that y is a b-environment on n and that the entry formula holds for every i∈n; the equality b=B makes this exactly an environment over the intended target.

    fo : Formula S 
    fo = ∃̇ ( domAt i2 i0
           ∧̇ ∃̇ ( (var i0 ≐ con B)
                ∧̇ envOverAt i2 i1 i0
                ∧̇ ∀̇∈ (var i1) entFo ) )

To read an entry from the formula, the proof eliminates the two nested existential witnesses u and v. This elimination is valid because Ent y s i is itself a proposition under propositional truncation.

    private
      entOut : (y s n b i : S) → ⟨ (i ∷ b ∷ n ∷ y ∷ s ∷ []) ⊨ entFo ⟩ → Ent y s i
      entOut y s n b i = PT.rec squash₁ (λ { (u , hv) →
        PT.rec squash₁ (λ { (v , (h1 , (h2 , h3))) →
          let γ = v ∷ u ∷ i ∷ b ∷ n ∷ y ∷ s ∷ [] in

The adequacy laws for the two environment applications and for application of E convert formula satisfaction into the three ambient memberships. Packaging the recovered u, v, and these memberships produces the required truncated entry.

          ∣ u , v
          , ( subst ⟨_⟩ (appAt-adequate i6 i2 i1 γ) h1
            , subst ⟨_⟩ (appAt-adequate i5 i2 i0 γ) h2
            , subst ⟨_⟩ (appC-adequate E i1 i0 γ) h3 ) ∣₁ }) hv })

The reverse direction maps a truncated entry into satisfaction of the formula. It uses the same three adequacy equalities in reverse, turning the ambient graph memberships into the two environment-application clauses and the application clause for E.

      entIn : (y s n i : S) → Ent y s i → ⟨ (i ∷ B ∷ n ∷ y ∷ s ∷ []) ⊨ entFo ⟩
      entIn y s n i = PT.map (λ { (u , v , (h1 , h2 , h3)) →
        let γ = v ∷ u ∷ i ∷ B ∷ n ∷ y ∷ s ∷ [] in
        u , ∣ v , ( subst ⟨_⟩ (sym (appAt-adequate i6 i2 i1 γ)) h1
                  , subst ⟨_⟩ (sym (appAt-adequate i5 i2 i0 γ)) h2

After both witnesses are repackaged under the nested existential quantifiers, the graph-membership clause for E completes satisfaction of the entry formula. Hence entOut and entIn establish the exact correspondence needed for each index.

                  , subst ⟨_⟩ (sym (appC-adequate E i1 i0 γ)) h3 ) ∣₁ })

The body reader receives the three components exposed by the outer formula: n is the domain of s, the auxiliary object b has the same underlying set as B, and y is an environment over b on n whose every index satisfies the entry formula. It must convert these data into Wit y s.

      bodyOut : (y s n b : S)
              → ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
              → fst b ≡ fst B
              → ⟨ (b ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
              → ⟨ (b ∷ n ∷ y ∷ s ∷ []) ⊨ ∀̇∈ (var i1) entFo ⟩

The equality between the underlying sets of b and B transports the environment-over assertion from b to the fixed target B. Each bounded instance of the entry formula is read by entOut, and the common domain together with these two components is then packaged under propositional truncation.

              → Wit y s
      bodyOut y s n b hd eb he hS =
        ∣ n , ( hd
              , envOverAt-transport (b ∷ n ∷ y ∷ s ∷ []) (B ∷ n ∷ y ∷ s ∷ [])
                  i2 i1 i0 i2 i1 i0 refl refl eb he

The bounded universal clause is used pointwise: for each i∈n, entOut turns its satisfaction proof into Ent y s i. Together with the domain equation and the transported environment condition, these entries form the three components of the truncated witness Wit y s.

              , λ i i∈n → entOut y s n b i (hS i i∈n) ) ∣₁

To read the whole graph formula outward, we first eliminate the truncated witness n, then the truncated witness b. Their accompanying clauses give the domain condition, the equality fst b ≡ fst B, the environment condition, and the bounded step condition; bodyOut turns exactly these data into Wit y s. The eliminations are legitimate because Wit y s is itself propositionally truncated.

    fo-out : (y s : S) → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩ → Wit y s
    fo-out y s = PT.rec squash₁ (λ { (n , (hd , hb)) →
      PT.rec squash₁ (λ { (b , (eb , (he , hS))) → bodyOut y s n b hd eb he hS }) hb })

Conversely, a host-level witness supplies the outer existential with n and the inner existential with the fixed element B. Reflexivity proves that this element denotes the required target, while entIn converts every pointwise entry back into the bounded formula. Together, fo-out and fo-in establish the adequacy of fo for Wit.

    fo-in : (y s : S) → Wit y s → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩
    fo-in y s = PT.rec (snd ((y ∷ s ∷ []) ⊨ fo))
      (λ { (n , (hd , he , hS)) →
        ∣ n , ( hd , ∣ B , ( refl , he , λ i i∈n → entIn y s n i (hS i i∈n) ) ∣₁ ) ∣₁ })

Fix a sequence g of length N over A, a carrier element s, and an equation identifying the underlying set of s with the environment graph of g. This concrete representation lets us construct the coordinatewise image and then prove that any output satisfying the same graph formula has the same underlying set.

  module AtSeq (N : ℕ) (g : Ix A N) (s : S) (e : fst s ≡ fst (envS A g)) where

The intended output is the environment graph of the coordinatewise image fg g. At index j, its value is f (g j), so the source and target sequences have the same finite length and corresponding entries are related by the input graph E.

    y₀ : S
    y₀ = envS B (fg g)

The next lemma exposes the elementary membership fact needed to build this witness: each coordinate pair occurs in the graph of an environment. It remains local because the public result of the subsection is the existence and uniqueness of the whole image environment.

    private

The entry lemma says that the coded graph of a function contains the ordered pair of each natural index with its value. The proof is by the specification of the environment constructor: the pair is there by definition.

      at : {k : ℕ} (h : Fin k → V ℓ) (j : Fin k)
         → ⟨ pr (# (toℕ j)) (h j) ∈ env h ⟩
      at h j = subst ⟨_⟩ (sym (lookup-spec h j (h j))) refl

The canonical image satisfies the host predicate Wit: the numeral nn N records the common domain, he records that y₀ is an environment over B of that length, and step verifies the relation at every index below N. These three clauses are then placed under propositional truncation, preserving existence without exposing a chosen decomposition later.

    wit : Wit y₀ s
    wit = ∣ nn N , ( hd , he , step ) ∣₁
      where
      hd : ⟨ (nn N ∷ y₀ ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
      hd = domAt-fill i2 i0 (nn N ∷ y₀ ∷ s ∷ []) N (vA g) (isLA g) e refl

The fact envOver B (fg g) is initially stated in the shorter environment containing B, nn N, and y₀. The transport lemma moves this same formula to the longer assignment that also contains s; the three reflexivity proofs say that the slots used by the formula still contain exactly the same elements. Hence adding the unused source sequence does not change the environment-over assertion.

      he : ⟨ (B ∷ nn N ∷ y₀ ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
      he = envOverAt-transport (B ∷ nn N ∷ y₀ ∷ []) (B ∷ nn N ∷ y₀ ∷ s ∷ [])
             i2 i1 i0 i2 i1 i0 refl refl refl (envOver B (fg g))

The step clause at each position is proved by eliminating the numeral membership into a bounded natural number. The eliminated data names a specific index whose value is available in both sequences.

      step : (i : S) → ⟨ fst i ∈ # N ⟩ → Ent y₀ s i
      step i i∈N = PT.map atIndex (∈#-elim N (fst i) i∈N)
        where
        atIndex : Σ[ k ∈ ℕ ] ((k < N) × (fst i ≡ # k))
                → Σ[ u ∈ S ] Σ[ v ∈ S ]

For the recovered finite index j, the required entry consists of the source value vA g j, the target value vB (fg g) j, and three graph memberships: the source environment stores the first value at j, the target environment stores the second there, and E relates the first value to the second. Constructibility proofs turn both values into elements of the carrier S.

                    ( ⟨ pr (fst i) (fst u) ∈ fst s ⟩
                    × ⟨ pr (fst i) (fst v) ∈ fst y₀ ⟩
                    × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ )
        atIndex (k , p , ei) =
            (vA g j , isLA g j) , (vB (fg g) j , isLB (fg g) j)

The environment-entry lemma supplies the first two memberships, transported along the equation that identifies the given position with the numeral for j and, for the source, along the presentation equation e. The graph theorem f-graph supplies the third. The finite index j is defined immediately below from the bounded natural number obtained in the preceding step.

          , ( subst2 (λ a w → ⟨ pr a (vA g j) ∈ w ⟩) (sym qi) (sym e) (at (vA g) j)
            , subst (λ a → ⟨ pr a (vB (fg g) j) ∈ fst y₀ ⟩) (sym qi) (at (vB (fg g)) j)
            , f-graph (g j) )
          where
          j : Fin N

The internal index j is constructed from the bounded natural number by the finite decoding, and the numeral equation composes the membership transport with the recovery of the index value.

          j = fromℕ' N k p
          qi : fst i ≡ # (toℕ j)
          qi = ei ∙ cong #_ (sym (toFromId' N k p))

Uniqueness starts with an arbitrary candidate y satisfying Wit y s and aims to prove equality of its underlying set with that of y₀. The truncated witness may be eliminated because equality in the cumulative hierarchy is a proposition. Once its three clauses are exposed, the local module Only derives the desired equality from them.

    only : (y : S) → Wit y s → fst y ≡ fst y₀
    only y = PT.rec (setIsSet (fst y) (fst y₀))
      (λ { (n , (hd , he , hS)) → Only.final n hd he hS })
      where
      module Only (n : S)

The inner module collects the three clauses of the witness: the domain condition, the environment-over condition, and the step clause at every position.

                  (hd : ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩)
                  (he : ⟨ (B ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩)
                  (hS : (i : S) → ⟨ fst i ∈ fst n ⟩ → Ent y s i) where

The numeral equation identifies the unknown length with the known length N, by the adequacy of the domain coding.

        qn : fst n ≡ # N
        qn = domAt-numeral i2 i0 (n ∷ y ∷ s ∷ []) N (vA g) (isLA g) e hd

The environment condition and the recovered length determine an index function gR : Ix B N whose graph presents the candidate y. This definition is opaque because its construction eliminates truncated data; subsequent reasoning uses the recovered function through its stated equations rather than unfolding that elimination.

        opaque
          gR : Ix B N
          gR = Recover.g B N (B ∷ n ∷ y ∷ s ∷ []) i2 i1 i0 qn refl he

Recovery also proves that the underlying set of y is the environment graph generated by gR. This equation replaces the arbitrary presentation in the witness by a fixed-length coordinate presentation, so uniqueness can now be checked one coordinate at a time.

          gR-eq : fst y ≡ fst (envS B gR)
          gR-eq = Recover.recovers B N (B ∷ n ∷ y ∷ s ∷ []) i2 i1 i0 qn refl he

At each index j, the step clause yields, under propositional truncation, a source value, a candidate target value, and the three graph memberships relating them. The target equality is a proposition, so PT.rec may pass these data to read. That lemma proves equality of the represented values; injectivity of the presentation of B then gives gR j ≡ fg g j.

        pt : (j : Fin N) → gR j ≡ fg g j
        pt j = ↪-inj {a = fst B} (PT.rec (setIsSet _ _) read (hS (nn (toℕ j)) j∈n))
          where
          j∈n : ⟨ # (toℕ j) ∈ fst n ⟩
          j∈n = subst (λ w → ⟨ # (toℕ j) ∈ w ⟩) (sym qn) (#mono (toℕ j) N (toℕ<n j))

The reading lemma states what the step clause provides: two elements and three memberships, identifying the argument in the source sequence, the value in the unknown environment, and the relation fact connecting them through the coded pairing.

          read : Σ[ u ∈ S ] Σ[ v ∈ S ]
                   ( ⟨ pr (# (toℕ j)) (fst u) ∈ fst s ⟩
                   × ⟨ pr (# (toℕ j)) (fst v) ∈ fst y ⟩
                   × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ )
               → vB gR j ≡ vB (fg g) j

The equation of the source argument is recovered by the lookup specification of the source environment, transported along the identifying equation.

          read (u , v , (hu , hv , hE)) = sym qv ∙ qv'
            where
            qu : fst u ≡ vA g j
            qu = subst ⟨_⟩ (lookup-spec (vA g) j (fst u))
                   (subst (λ w → ⟨ pr (# (toℕ j)) (fst u) ∈ w ⟩) e hu)

The candidate value v has two descriptions. Looking it up in the recovered environment gives fst v ≡ vB gR j. On the other hand, hE says that E relates the recovered source argument to v; after identifying that argument with vA g j, single-valuedness of E compares this edge with f-graph (g j) and yields fst v ≡ vB (fg g) j.

            qv : fst v ≡ vB gR j
            qv = subst ⟨_⟩ (lookup-spec (vB gR) j (fst v))
                   (subst (λ w → ⟨ pr (# (toℕ j)) (fst v) ∈ w ⟩) gR-eq hv)
            qv' : fst v ≡ vB (fg g) j
            qv' = svAt-out zero (E ∷ A ∷ []) sv u v (vB (fg g) j , isLB (fg g) j) hE

The final equation composes the function-graph fact with the reversed argument equation, completing the identification of the two image values.

                    (subst (λ w → ⟨ pr w (vB (fg g) j) ∈ fst E ⟩) (sym qu) (f-graph (g j)))

It remains to pass from coordinatewise agreement to equality of the two environment graphs. The desired path begins with the recovered presentation of y and ends at the canonical graph y₀.

        final : fst y ≡ fst y₀

Function extensionality turns pt into equality of the two index functions. Applying envS B along that path identifies their environment graphs, and composing with gR-eq proves fst y ≡ fst y₀. The path-lambda expression is the direct cubical action of the environment graph along this equality.

        final = gR-eq ∙ λ i → fst (envS B (funExt pt i))

Membership in the sequence set is stated as a type so that the argument can carry it alongside each element.

  Mem : S → Type (ℓ-suc ℓ)
  Mem s = ⟨ fst s ∈ˢ fst (seqL A) ⟩

A representation is the truncated record of a length, an index function and the equation identifying the two presentations. The truncated form is what seqL-out supplies.

  Rep : S → Type (ℓ-suc ℓ)
  Rep s = ∥ Σ[ n ∈ ℕ ] Σ[ g ∈ Ix A n ] (fst s ≡ fst (envS A g)) ∥₁

Starting from membership in seqL A, seqL-out gives a propositionally truncated length n together with membership in the corresponding fixed-length environment set. For that n, envSet-out gives a truncated index function and presentation equation. Mapping and eliminating only into the truncated target combines the two stages without choosing a global representation.

  rep : (s : S) → Mem s → Rep s
  rep s m = PT.rec squash₁
    (λ { (n , hn) → PT.map (λ { (g , e) → n , g , e }) (envSet-out A n s hn) })
    (seqL-out A s m)

The recursion package uses seqL A as its domain and fo as its graph. For every member s, a truncated representation of s determines the canonical image environment; AtSeq.wit proves that this image satisfies the graph, while AtSeq.only proves that every other satisfying value has the same underlying set. Thus the graph is total and single-valued in the sense required by mereFunct.

  R : Recursion
  R = record
    { dom   = seqL A
    ; graph = fo
    ; funct = λ s m → mereFunct fo s (PT.map (λ { (n , g , e) →

For a concrete representation (n , g , e), the functionality witness consists of the canonical image AtSeq.y₀, its proof of satisfying fo, and the proof that every other satisfying carrier element is equal to it. Σ≡Prop lifts equality of underlying sets to equality in S, since constructibility proofs form proposition-valued fibres. PT.map then keeps the whole construction under truncation.

        AtSeq.y₀ n g s e
        , ( fo-in (AtSeq.y₀ n g s e) s (AtSeq.wit n g s e)
          , λ y' h → Σ≡Prop (λ v → snd (isL v)) (AtSeq.only n g s e y' (fo-out y' s h)) ) })
        (rep s m)) }

The recursion table machinery is opened, supplying the actual function, its values, and the uniqueness of values.

  module T = Of R using ( funct; val; val-uniq )

The resulting value fn s m is the unique carrier element satisfying fo at s; although its construction starts from a truncated representation of s, uniqueness makes the value independent of which length and index function represent that sequence.

  fn : (s : S) → Mem s → S
  fn = T.val

Whenever s is presented by a length n and an index function g, the computed value fn s m equals the canonical coordinatewise image AtSeq.y₀ n g s e. Both values satisfy the recursion graph at s, so the uniqueness theorem T.val-uniq supplies the equality. This equation will let later proofs reason from any available presentation of s.

  fn-code : (s : S) (m : Mem s) (n : ℕ) (g : Ix A n) (e : fst s ≡ fst (envS A g))
          → fn s m ≡ AtSeq.y₀ n g s e
  fn-code s m n g e =
    T.val-uniq s m (AtSeq.y₀ n g s e) (fo-in (AtSeq.y₀ n g s e) s (AtSeq.wit n g s e))

Membership in the target sequence set is proved by transporting along the code equation and applying the inward reading of the target sequence set.

  into : (s : S) (m : Mem s) → ⟨ fst (fn s m) ∈ˢ fst (seqL B) ⟩
  into s m = PT.rec (snd (fst (fn s m) ∈ˢ fst (seqL B)))
    (λ { (n , g , e) → subst (λ w → ⟨ fst w ∈ˢ fst (seqL B) ⟩) (sym (fn-code s m n g e))
           (seqL-in B n (envS B (fg g)) (envSet-in B (fg g))) })
    (rep s m)

These facts define a map from seqL A to seqL B: fo gives its graph, fn gives its unique value at each source member, and into proves that this value is again a finite sequence over B. The remaining task is to show that equality of two values forces equality of their source sequences.

  D : DefinableMap
  D = record
    { dom = seqL A ; cod = seqL B ; fn = fn ; into = into ; graph = fo
    ; defines = λ s m → T.funct s m .fst .snd
    ; only    = λ s m y h → sym (T.val-uniq s m y h) }

To prove injectivity, it suffices first to compare canonical presentations. Suppose two coordinatewise image environments are equal, although their displayed lengths may differ. The helper same recovers equality of the lengths, transports the second source sequence to the common finite index type, and then uses injectivity of f at every coordinate to prove equality of the source environment graphs.

  private
    same : (n : ℕ) (g : Ix A n) (n' : ℕ) (g' : Ix A n')
         → fst (envS B (fg g)) ≡ fst (envS B (fg g'))
         → fst (envS A g) ≡ fst (envS A g')
    same n g n' g' q =

The equality of the two target environment graphs determines equality of their finite lengths by env-len, because the coded domain of an environment is its numeral length. Substitution along that equality reduces the problem to two sequences indexed by the same Fin n; the local family P records the statement that remains after this alignment.

      subst P (env-len (envS B (fg g)) (vB (fg g)) (vB (fg g')) (isLB (fg g)) (isLB (fg g')) refl q)
        base g' q
      where
      P : ℕ → Type (ℓ-suc ℓ)
      P k = (h : Ix A k) → fst (envS B (fg g)) ≡ fst (envS B (fg h))

With a common length, env-pt reads equality of the target graphs as equality of their values at each index. Injectivity of the presentation of B turns this into equality f (g j) ≡ f (h j), and f-inj recovers g j ≡ h j. Function extensionality then identifies the source index functions, hence their environment graphs.

          → fst (envS A g) ≡ fst (envS A h)
      base : P n
      base h q' = λ i → fst (envS A (funExt (λ j →
        f-inj (g j) (h j) (↪-inj {a = fst B} (env-pt (vB (fg g)) (vB (fg h)) q' j))) i))

For arbitrary members s and s', their representations are available only under propositional truncation. The desired equality fst s ≡ fst s' is a proposition because cumulative-hierarchy values form a set, so PT.rec2 may expose one representation of each input locally and pass them to the canonical comparison.

  inj : (s : S) (m : Mem s) (s' : S) (m' : Mem s')
      → fst (fn s m) ≡ fst (fn s' m') → fst s ≡ fst s'
  inj s m s' m' q = PT.rec2 (setIsSet (fst s) (fst s'))
    (λ { (n , g , e) (n' , g' , e') →
        e

The code equations identify the actual outputs fn s m and fn s' m' with their respective canonical image environments. Composing these identifications with the assumed output equality gives the hypothesis required by same; finally, the presentation equations e and e' transfer the resulting equality of source environment graphs back to fst s ≡ fst s'.

      ∙ same n g n' g'
          (sym (cong fst (fn-code s m n g e)) ∙ q ∙ cong fst (fn-code s' m' n' g' e'))
      ∙ sym e' })
    (rep s m) (rep s' m')

The injectivity just proved upgrades the definable map to an internal coded injection seqL A ↪ seqL B. Its graph still records the same coordinatewise action; the conclusion retains only the propositional existence of a suitable code.

  injL : InjL (seqL A) (seqL B)
  injL = Inj.injL D inj

The exported theorem starts from an actual code E witnessing an injection from A to B: it is single-valued, has domain A, is injective, and has range contained in B. Passing these four components to SeqMap yields the propositionally truncated existence of a coded injection from seqL A to seqL B. The result concerns finite sequences of arbitrary length, not infinite sequences.

seq-map : (A B E : S) → InjCode E A B → InjL (seqL A) (seqL B)
seq-map A B E (sv , dm , ij , ran) = SeqMap.injL A B E sv dm ij ran

Pinning a quantified variable to a constant

The pinning formula binds one existential to fix a free slot to a chosen constant: it says merely that some value equals the constant and satisfies the inner formula.

pinAt : ∀ {n} → S → Formula S (suc n) → Formula S n
pinAt c φ = ∃̇ ((var zero ≐ con c) ∧̇ φ)

The inward reading exhibits the constant as the witness and the body satisfaction at the extended environment.

pin-in : ∀ {n} (c : S) (φ : Formula S (suc n)) (γ : S ^ n)
       → ⟨ (c ∷ γ) ⊨ φ ⟩ → ⟨ γ ⊨ pinAt c φ ⟩
pin-in c φ γ h = ∣ c , (refl , h) ∣₁

For the outward direction, the existential supplies a carrier element z, an equality of its underlying set with that of c, and a proof of the body at z. Since constructibility is proposition-valued, Σ≡Prop lifts the underlying-set equality to an equality z ≡ c in S; transport along it gives satisfaction at the pinned environment. Elimination from propositional truncation is valid because formula satisfaction is a proposition.

pin-out : ∀ {n} (c : S) (φ : Formula S (suc n)) (γ : S ^ n)
        → ⟨ γ ⊨ pinAt c φ ⟩ → ⟨ (c ∷ γ) ⊨ φ ⟩
pin-out c φ γ = PT.rec (snd ((c ∷ γ) ⊨ φ))
  (λ { (z , (ez , h)) → subst (λ v → ⟨ (v ∷ γ) ⊨ φ ⟩) (Σ≡Prop (λ v → snd (isL v)) ez) h })

A formula for coded injections into a fixed target

An InjCode F a b consists of four proposition-valued conditions: single-valuedness of F, the assertion that its domain is a, injectivity of its graph, and containment of its values in b. Formula satisfaction is proposition-valued, and the last condition is a dependent function into membership propositions, so their nested product is again a proposition.

isPropInjCode : (F a b : S) → isProp (InjCode F a b)
isPropInjCode F a b =
  isProp× (snd ((F ∷ a ∷ []) ⊨ svAt zero))
    (isProp× (snd ((F ∷ a ∷ []) ⊨ domAt zero (suc zero)))
      (isProp× (snd ((F ∷ a ∷ []) ⊨ injAt zero))

The remaining range condition quantifies over an argument, a value, and a proof that the graph relates them. Its conclusion is membership of the value in b, which is a proposition; repeated dependent products therefore preserve propositionality and complete the proof for InjCode.

        (isPropΠ3 (λ _ y _ → snd (fst y ∈ fst b)))))

Only the underlying sets represented by the graph and domain arguments matter to InjCode. Because constructibility proofs are propositions, equalities fst F ≡ fst F' and fst a ≡ fst a' lift uniquely to equalities in S; two-variable substitution then transports an injection code from (F , a) to (F' , a'), while the target b remains fixed.

injcode-resp : (F F' a a' b : S) → fst F ≡ fst F' → fst a ≡ fst a'
             → InjCode F a b → InjCode F' a' b
injcode-resp F F' a a' b qF qa = subst2 {x = F} {y = F'} {z = a} {w = a'}
  (λ E A → InjCode E A b)
  (Σ≡Prop (λ v → snd (isL v)) qF) (Σ≡Prop (λ v → snd (isL v)) qa)

The formula injFo b f B expresses the four conditions of an injection code using the graph in slot f and the domain in slot B. The graph is single-valued, has exactly that domain, and is injective; moreover, whenever it relates an argument to a value, that value belongs to the fixed target b. The last clause gives range containment, rather than surjectivity onto b.

injFo : ∀ {n} → S → Fin n → Fin n → Formula S n
injFo b f B = svAt f ∧̇ domAt f B ∧̇ injAt f
            ∧̇ ∀̇ (∀̇ (appAt (suc (suc f)) i1 i0 ⇒̇ (var i0 ∈̇ con b)))

To prove the reading laws for injFo, fix the target b, the two relevant slots f and B, and an assignment γ. The local names F and A denote the carrier elements found in those slots. The following arguments can then state the result directly as an InjCode F A b, keeping the bookkeeping of variable lookup out of the mathematical statement.

module InjFo {n : ℕ} (b : S) (f B : Fin n) (γ : S ^ n) where
  private
    F A : S
    F = lookup f γ
    A = lookup B γ

The reading lemma turns satisfaction of the injection formula into the four clauses of an injection code. For the domain clause, a graph witness for an input is eliminated from propositional truncation into the proposition that the input belongs to A; conversely, membership in A produces the required domain witness.

  read : ⟨ γ ⊨ injFo b f B ⟩ → InjCode F A b
  read (sv , dm , ij , ran) =
      svAt-in zero (F ∷ A ∷ []) (λ x y y' p q → svAt-out f γ sv x y y' p q)
    , domAt-intro zero (suc zero) (F ∷ A ∷ []) (λ x →
          (λ h → PT.rec (snd (fst x ∈ fst A))

Single-valuedness and injectivity are transferred by reading their semantic clauses at γ and rebuilding the corresponding clauses for the two-entry environment (F,A). The range condition uses adequacy of application to turn graph membership in F into the application atom expected by the formula, after which its last clause yields membership of the value in the fixed target b.

                   (λ { (y , p) → domAt-out f B γ dm x y p }) h)
        , (λ hx → domAt-in f B γ dm x hx))
    , injAt-in zero (F ∷ A ∷ []) (λ y x x' p q → injAt-out f γ ij y x x' p q)
    , λ x y p → ran x y (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) i1 i0 (y ∷ x ∷ γ))) p)

The filling lemma is the converse construction: from the four data of a coded injection it builds the satisfaction of the injection formula, this time reading all atoms over the structure in which the formula is stated.

  fill : InjCode F A b → ⟨ γ ⊨ injFo b f B ⟩
  fill (sv , dm , ij , ran) =
      svAt-in f γ (λ x y y' p q → svAt-out zero (F ∷ A ∷ []) sv x y y' p q)
    , domAt-intro f B γ (λ x →
          (λ h → PT.rec (snd (fst x ∈ fst A))

For totality, a truncated graph witness is eliminated only into the proposition that the input lies in A, while membership in A supplies a witness in the other direction. The remaining clauses rebuild single-valuedness and injectivity at γ, and application adequacy converts the range hypothesis into the final formula clause. Together, read and fill give both directions between formula satisfaction and the four injection-code conditions.

                   (λ { (y , p) → domAt-out zero (suc zero) (F ∷ A ∷ []) dm x y p }) h)
        , (λ hx → domAt-in zero (suc zero) (F ∷ A ∷ []) dm x hx))
    , injAt-in f γ (λ y x x' p q → injAt-out zero (F ∷ A ∷ []) ij y x x' p q)
    , λ x y p → ran x y (subst ⟨_⟩ (appAt-adequate (suc (suc f)) i1 i0 (y ∷ x ∷ γ)) p)

Reducing the infinite-stage count to L_ω

The stage at the infinite ordinal ω is presented as a constructible set: the ordinal stage Lset ω together with its ordinalness is packaged by the stage presentation.

Lω : S
Lω = LsetS ω ω-ord

The goal of the section is then stated as a type: an internal coded injection from the constructible presentation of Lset ω into the internal ω. This is the base case on which the counting of larger stages is built.

LimitStageCounted : Type (ℓ-suc ℓ)
LimitStageCounted = InjL Lω ωʟ

The move lemma transports a coded internal injection along equalities of the underlying source and target sets. The source equality gives an inclusion from the new source a' into the old source a; after the given injection is applied, the target equality gives an inclusion from the old target b into the new target b'. Composing these three injections yields InjL a' b'.

move : (a a' b b' : S) → fst a ≡ fst a' → fst b ≡ fst b' → InjL a b → InjL a' b'
move a a' b b' qa qb h =
  injl-trans a' a b' (inclusion-coded a' a (λ z hz → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym qa) hz))
    (injl-trans a b b' h (inclusion-coded b b' (λ z hz → subst (λ w → ⟨ z ∈ˢ w ⟩) qb hz)))

The base count: L_ω injects into ω

The exclusion argument works with finite stages of the form Lset (# n), and begins by taking the tally of such a finite stage: an indexed enumeration of its members.

private
  module FinNo (n : ℕ) where
    t : Tally (finiteStage n)
    t = StageOrder.tally (stageOrder n)

The tally supplies its size, its member at each index, and the covering fact that every member appears at some index.

    open Tally t using ( size; item; onto )

The search lemma names a member: for each member x of the finite stage it runs a decidable search through the finitely many indices, comparing each entry with x by excluded middle, and returns an index whose entry is x. The search returns some index; it does not claim that index to be unique, and it is a finitary decision on a finite family rather than an appeal to any choice principle.

    named : (x : V ℓ) → ⟨ x ∈ˢ finiteStage n ⟩ → Σ[ i ∈ Fin size ] (item i ≡ x)
    named x hx = decRec (λ q → q) (λ nq → Empty.rec (PT.rec Empty.isProp⊥ nq (onto x hx)))
      (DecΣ size (λ i → item i ≡ x)
        (λ i → Sum.rec yes no (lem ((item i ≡ x) , setIsSet (item i) x))))

Suppose that f injected the presentation of ω into a finite stage. Each value f x can be assigned a tally index q x; duplicating that index gives the map x ↦ (q x,q x) required by the finite exclusion theorem. Equality of these pairs forces equality of the corresponding values of f, and then injectivity of f forces equality of the original inputs.

    noinj : (f : ⟪ ω ⟫ → ⟪ Lset (# n) ⟫)
          → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥
    noinj f finj = finite-excl-ω (# size) (numeral-ord size) (#∈ω size)
      (λ x → q x , q x) (λ x y e → finj x y (qq x y (cong fst e)))
      where

The auxiliary map reads each value of f as an ambient element, certifies that it belongs to the finite stage, and names it by the finite index found above.

      vl : ⟪ ω ⟫ → V ℓ
      vl x = ⟪ Lset (# n) ⟫↪ (f x)
      mm : (x : ⟪ ω ⟫) → ⟨ vl x ∈ˢ finiteStage n ⟩
      mm x = member (Lset (# n)) (f x)
      q : ⟪ ω ⟫ → ⟪ # size ⟫

The map q converts the chosen tally index into the corresponding element of the finite ordinal presentation ⟪# size⟫. If two such names agree, injectivity of that presentation makes their natural-number indices equal, so the two tally entries agree. The presentation of Lset (# n) then turns this ambient equality back into equality of the two values of f.

      q x = fromFin size (toℕ (named (vl x) (mm x) .fst) , toℕ<n (named (vl x) (mm x) .fst))
      qq : (x y : ⟪ ω ⟫) → q x ≡ q y → f x ≡ f y
      qq x y e = ↪-inj {a = Lset (# n)}
        (sym (named (vl x) (mm x) .snd)
          ∙ cong item (inj-toℕ (cong fst (fromFin-inj size _ _ e)))

The chain of identifications is closed by the named entry of the second point, completing the proof that equal names force equal values.

          ∙ named (vl y) (mm y) .snd)

For an arbitrary index w, NoInto w is the proposition that no host-level injection exists from the presentation of ω into the presentation of Lset w. The next lemma will establish this proposition under the additional hypothesis that w belongs to ω.

  NoInto : V ℓ → Type ℓ
  NoInto w = (f : ⟪ ω ⟫ → ⟪ Lset w ⟫)
           → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥

The general form follows by transporting the finite case along the membership of g in ω: a member of ω is, merely, a numeral, and the transport moves the whole exclusion statement to the stage of that numeral. The elimination is legitimate because the target is a contradiction.

  no-inj-fin : (g : V ℓ) → ⟨ g ∈ˢ ω ⟩ → NoInto g
  no-inj-fin g g∈ω = PT.rec (isPropΠ2 (λ _ _ → Empty.isProp⊥))
    (λ { (k , e) → subst NoInto e (FinNo.noinj (lower k)) }) g∈ω

The infinite ordinal ω is constructible: its ordinalness feeds the ordinal stage construction.

hω : ⟨ isL ω ⟩
hω = isL-ord ω ω-ord

The stage order of Lset ω is implemented as a constructible set Rω of coded pairs inside L.

Rω : SL.S
Rω = relL ω hω ω-ord

The relation specification says that the coded pairs of Rω are exactly the ordered pairs of L-elements related by the stage order.

specω : IsRel ω Rω
specω = relL-spec ω hω ω-ord

The endpoint condition recovers stage membership for both endpoints of every related pair. Unfolding the coded pair yields two members of Lset ω, and the component equations identify their underlying sets with the endpoints y and x.

Rsub : (y x : SL.S) → Holds Rω y x
     → ⟨ fst y ∈ˢ Lset ω ⟩ × ⟨ fst x ∈ˢ Lset ω ⟩
Rsub y x h = PT.rec isP
  (λ { (_ , h₁) → PT.rec isP
    (λ { (a , h₂) → PT.rec isP

Both memberships are transported along the two component equations supplied by the injectivity of the ordered-pair coding.

      (λ { (b , (q , _)) →
             subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym (pr-inj q .fst)) (a .snd)
           , subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym (pr-inj q .snd)) (b .snd) })
      h₂ })
    h₁ })

The conjunction of the two memberships is a proposition, and the relatedness of the coded pair is produced from the relation specification at the constructible ordered pair.

  rel
  where
  isP : isProp (⟨ fst y ∈ˢ Lset ω ⟩ × ⟨ fst x ∈ˢ Lset ω ⟩)
  isP = isProp× (snd (fst y ∈ˢ Lset ω)) (snd (fst x ∈ˢ Lset ω))
  rel : ⟨ Related ω (pr (fst y) (fst x)) ⟩

The relatedness is transported along the identification of the coded pair with the plain ordered pair of the two underlying sets.

  rel = subst (λ w → ⟨ Related ω w ⟩) (prʟ-fst y x)
    (specω (prʟ y x) .fst
      (subst (λ w → ⟨ w ∈ˢ fst Rω ⟩) (sym (prʟ-fst y x)) h))

The order-type machinery is instantiated at the stage Lset ω with the internal relation and its endpoint condition: this fixes the small domain, the internal relation, and the collapse construction of the previous chapter.

module OT = Code Lω Rω Rsub using ( module Conjuncts; Dom; _≺_; isProp≺; ≺-in; ≺-out )

The host well order is the stage order carried to the presentation of Lset ω, so the abstract well-order machinery can be used on the small index type.

Wω : SWO ⟪ Lset ω ⟫
Wω = carry (Lset ω) (orderAt ω ω-ord)

Write a <ω b for the strict comparison supplied by this well order on the presentation of Lset ω. The next two lemmas show that this relation and the internally coded predecessor relation a OT.≺ b express the same comparison.

open SWO Wω using () renaming ( _<∙_ to _<ω_ )

The internal relation and the host stage order agree on the common presentation. The first direction reads an internal predecessor proof a OT.≺ b as the host-order comparison a <ω b, using the representation theorem for the coded relation.

≺→< : (a b : OT.Dom) → a OT.≺ b → a <ω b
≺→< a b k = ixRel-rep ω ω-ord Rω specω a b (OT.≺-out a b k)

Conversely, the filling theorem for the coded relation turns a host-order comparison a <ω b into the internal predecessor proof a OT.≺ b. These two conversions let the order-theoretic properties of the host relation be transferred to the internal one.

<→≺ : (a b : OT.Dom) → a <ω b → a OT.≺ b
<→≺ a b k = OT.≺-in a b (ixRel-fill ω ω-ord Rω specω a b k)

Well-foundedness of the internal relation follows from well-foundedness of the host order. Accessibility is transported point by point: each predecessor inside the internal relation is first converted into a host predecessor.

wfω : WellFounded OT._≺_
wfω m = go (SWO.wf∙ Wω m)
  where
  go : {n : OT.Dom} → Acc _<ω_ n → Acc OT._≺_ n
  go {n} (acc r) = acc (λ n' k → go (r n' (≺→< n' n k)))

Transitivity of the internal relation is likewise transported through the host order: two consecutive internal steps are converted, composed, and converted back.

transω : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c
transω {a} {b} {c} k k' =
  <→≺ a c (SWO.trans∙ Wω a b c (≺→< a b k) (≺→< b c k'))

For any a and b, trichotomy of the host well order gives exactly one of three forms: a <ω b, equality, or b <ω a. The result is expressed as a nested sum so that each comparison can be converted into the matching case for the internal relation.

triω : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
triω a b = go (SWO.tri∙ Wω a b)
  where
  go : TriW (a <ω b) (a ≡ b) (b <ω a)
     → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))

Each host case is converted back into the corresponding internal case: less-than, equality, or greater-than.

  go (lt h) = inl (<→≺ a b h)
  go (eq e) = inr (inl e)
  go (gt h) = inr (inr (<→≺ b a h))

Well-foundedness and transitivity now define the collapse values and their ordinal image otL. Trichotomy proves that distinct points have distinct collapse values, so the collapse graph colTable satisfies the injectivity clause and yields the code used below.

module C = OT.Conjuncts wfω transω using ( module Inj; col; col-ord; col-out; colTable; otL; otL-out )
module I = C.Inj triω using ( code; col-inj )

The birth-stage family is instantiated at the internal ω: every presented member of Lset ω has a birth stage in ω, ordered by a family relation.

private
  module F = Family ω (λ δ _ → orderAt δ) ω-ord using ( _≺_; bornAt )

The unfolded reading of the family relation is proved: at ω, the abstractly stated order equals the concrete birth-stage-then-step order.

  unfoldω : (a b : MemOf (Lset ω))
          → relOf (orderAt ω ω-ord) a b ≡ F._≺_ a b
  unfoldω a b = cong (λ z → relOf (z ω-ord) a b) (orderAt-step ω)

The birth stage of a member is read as an ambient set.

  bAt : MemOf (Lset ω) → V ℓ
  bAt a = F.bornAt a .fst

Every birth stage belongs to the internal ω, since the whole family lives below ω.

  bAt∈ω : (a : MemOf (Lset ω)) → ⟨ bAt a ∈ˢ ω ⟩
  bAt∈ω a = F.bornAt a .snd

Every birth stage is an ordinal: it is a member of the ordinal ω, and members of ordinals are ordinals.

  bAt-ord : (a : MemOf (Lset ω)) → IsOrd (bAt a)
  bAt-ord a = mem-ord {A = ω} ω-ord (bAt a) (bAt∈ω a)

Every presented member of Lset ω belongs to the stage indexed by its own birth stage raised by one: the member's constructibility is transported into that successor stage.

  self-at : (a : MemOf (Lset ω)) → ⟨ a .fst ∈ˢ Lset (sucV (bAt a)) ⟩
  self-at a = birth-mem (a .fst) (Lset→isL ω ω-ord (a .fst) (a .snd))

The step bound says: if a precedes b in the family order, then the underlying set of a belongs to the stage indexed by one plus the birth stage of b. In the strictly earlier birth case, the successor comparison is decided by ordinal linearity.

  step-bound : (a b : MemOf (Lset ω)) → F._≺_ a b
             → ⟨ a .fst ∈ˢ Lset (sucV (bAt b)) ⟩
  step-bound a b (inl h) =
    raise (suc∈or≡ (bAt a) (bAt b) (bAt-ord a) (bAt-ord b) h)
    where

In the strictly earlier-birth branch, ordinal discreteness compares sucV (bAt a) directly with bAt b. If the successor still lies below bAt b, or is equal to it, stage monotonicity carries the known membership of a in Lset (sucV (bAt a)) into Lset (sucV (bAt b)).

    raise : ⟨ sucV (bAt a) ∈ˢ bAt b ⟩ ⊎ (sucV (bAt a) ≡ bAt b)
          → ⟨ a .fst ∈ˢ Lset (sucV (bAt b)) ⟩
    raise (inl k) = Lset-mono {α = sucV (bAt b)} {β = sucV (bAt a)}
      (∈sucV-inl {A = bAt b} {x = sucV (bAt a)} k) (self-at a)
    raise (inr e) = Lset-mono {α = sucV (bAt b)} {β = sucV (bAt a)}

In the equality subcase sucV (bAt a) ≡ bAt b, the proof first places this ordinal in the successor of bAt b and then applies stage monotonicity. The other main branch has equal birth stages; there the step-order witness itself contains membership of a in the successor stage of their common birth stage, and transport along the equality gives the stated bound.

      (subst (λ w → ⟨ sucV (bAt a) ∈ˢ sucV w ⟩) e (self∈sucV (sucV (bAt a))))
      (self-at a)
  step-bound a b (inr (e , u)) =
    subst (λ w → ⟨ a .fst ∈ˢ Lset (sucV w) ⟩) (sym e) (u .fst)

Every point of the internal collapse domain is read as a presented member of Lset ω.

  atIx : OT.Dom → MemOf (Lset ω)
  atIx m = ⟪ Lset ω ⟫↪ m , memOf (Lset ω) m

For a collapse-domain point p, the guard index gOf p is the successor of the birth stage of the member represented by p. The finite stage Lset (gOf p) will contain every predecessor of p.

  gOf : OT.Dom → V ℓ
  gOf p = sucV (bAt (atIx p))

Every guard belongs to the internal ω, since it is the successor of a member of ω.

  gOf∈ω : (p : OT.Dom) → ⟨ gOf p ∈ˢ ω ⟩
  gOf∈ω p = ω-limit (bAt (atIx p)) (bAt∈ω (atIx p))

The predecessor bound says that every predecessor r of a point p presents an ambient element of the finite stage guarded by p. The proof transports the step bound through the unfolded reading of the family order.

  seg-bound : (p r : OT.Dom) → r OT.≺ p
            → ⟨ ⟪ Lset ω ⟫↪ r ∈ˢ Lset (gOf p) ⟩
  seg-bound p r k =
    step-bound (atIx r) (atIx p) (transport (unfoldω (atIx r) (atIx p)) (≺→< r p k))

A predecessor segment records a predecessor r of p together with the identification of its collapse value with a given set.

private
  Seg : OT.Dom → V ℓ → Type (ℓ-suc ℓ)
  Seg p b = Σ[ r ∈ OT.Dom ] ((r OT.≺ p) × (C.col r ≡ b))

Predecessor segments are propositions: two records with the same collapse value are identified because the collapse is injective on the small domain, the relation is proposition-valued, and the underlying sets form an h-set.

  isPropSeg : (p : OT.Dom) (b : V ℓ) → isProp (Seg p b)
  isPropSeg p b (r , _ , e) (r' , _ , e') =
    Σ≡Prop (λ z → isProp× (OT.isProp≺ z p) (setIsSet _ _))
      (I.col-inj r r' (e ∙ sym e'))

Every membership in a collapse value yields a predecessor segment: the truncated reading of the collapse is eliminated into the proposition-valued segment.

  seg : (p : OT.Dom) (b : V ℓ) → ⟨ b ∈ˢ C.col p ⟩ → Seg p b
  seg p b h = PT.rec (isPropSeg p b) (λ z → z) (C.col-out p b h)

It remains to show that each ordinal C.col p lies below ω. Ordinal trichotomy leaves two obstructing possibilities, equality with ω and membership of ω in the collapse. Both will imply the same inclusion ω ⊆ C.col p, so we first prove that such an inclusion would force an impossible injection into the finite stage Lset (gOf p).

col-fin : (p : OT.Dom) → ⟨ C.col p ∈ˢ ω ⟩
col-fin p = go (ord-tri (C.col p) (C.col-ord p) ω ω-ord)
  where
  refute : ((z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ C.col p ⟩) → Empty.⊥
  refute sub = no-inj-fin (gOf p) (gOf∈ω p) f f-inj