The numeral chain

This chapter constructs the natural-number chain inside L from the model's empty-set, pairing, and union operations, and proves that it projects to the ambient von Neumann numerals.

The mathematical question is this. The von Neumann successor of a set a is a ∪ {a}, and the model of L supplies its own empty set, unordered pair, and union as canonical realizers: each is the centre of a contractible type of sets satisfying its membership specification, read out by the description operator ℩. Such a centre is an operation with a specification, not a computation: nothing about its definition says that, on its underlying set, it is the set the ambient hierarchy constructs from its own pairing and union. So before the chain can be compared with the hierarchy's chain of numerals, a family of projection equations is needed, each saying that one model operation, read through the underlying set, is the corresponding hierarchy operation.

The argument for each projection equation has a fixed shape. The centre of a contractible type is compared with an explicitly built realizer: for pairing, the bounded pair construction applied at a merely existing common stage for the two underlying sets, supplied by isL-directed. Contractibility then gives a path from the centre to that realizer, and congruence of the underlying-set projection turns it into an equality of sets. Each elimination of truncated data is legitimate only because its target, an equation between hierarchy sets, is a proposition, which holds because the hierarchy's carrier is an h-set. With the projection equations in hand, the internal chain and the hierarchy's chain coincide step by step, and the two pinning equations the model record demands of a numeral chain follow by transporting the hierarchy's own facts along them.

The whole chapter is constructive: no excluded middle, no resizing, and no choice beyond what the contractibility of the realizer types already provides. What it does not do is collect the numerals into a set; that collection is the content of the infinity axiom itself.

The key notion is unique realization. For pairing, the specification is λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b), and hasPairL a b certifies that the type SetOf of constructible sets realizing it is contractible: there is a canonical realizer, the centre, together with a path from the centre to every other realizer. Union is specified and certified analogously by hasUnionL. A contractibility proof is explicit data, not a bare existence statement: it includes both the centre and the contraction, and it is the centre that the operations below select. This is the only form of choice the chapter uses, and it is supplied by the contractibility itself.

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

open import Base.Prelude
module L.Axioms.Numerals {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

Two sides meet in the projection equations. On the model side stand hasPairL and hasUnionL with their realizing constructions PairOf and UnionOf, and the internal empty set ∅ʟ. On the ambient side stand the hierarchy's unordered pair ⁅ _, _ ⁆ and union ⋃_, its successor sucV, and its numerals #_. The input that binds the two sides is isL-directed, which supplies, merely, a common ordinal stage containing the underlying sets of two constructible sets; the bounded pair construction needs exactly such a stage to build its realizer. The two internal operations must first be defined before they can be compared.

import FOL.ZFModel
open import V.Model {ℓ} using ( pair-singleton; module NumPin )
open import L.Constructible {ℓ} using ( 𝒮ʟ )
open import L.Axioms.Basic {ℓ}
  using ( hasPairL; hasUnionL; module PairOf; module UnionOf; isL-directed; ∅ʟ )

A projection equation is an equality between sets of the ambient hierarchy, for example fst (pairʟ a b) ≡ ⁅ fst a , fst b ⁆. This particular equality type is a proposition because the hierarchy's carrier is an h-set, which is what setIsSet certifies. That propositionhood is what permits eliminating the truncated stage data into it; no propositionhood is claimed about arbitrary equality types.

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; ⋃_; module InfinitySet )

Two conventions make the code readable. The structure 𝒮ʟ is the constructible universe presented as a model of set theory, and opening its model package exposes SetOf, the type of a carrier element together with its realizing specification, and ℩, the operator returning the first component of the centre of a contractible SetOf type. Throughout, fst on an element of the carrier S extracts the underlying set of the ambient hierarchy, and the projection equations compare exactly those underlying sets.

open InfinitySet using ( sucV; #_ )

open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf; ℩ )

The model's own operations

The description operator turns the contractibility of the realizer types into operations: pairʟ and unionʟ select the centres of hasPairL and hasUnionL, and the successor composes them.

One distinction governs what follows. A centre selected from a contractible type is an operation with a specification, not a computation rule. The contractibility proof does not make pairʟ a b reduce, on its underlying set, to the hierarchy's pair ⁅ fst a , fst b ⁆; what it does provide is a path from the centre to every realizer, and the projection equations of the next section are obtained by comparing the centre with an explicitly built realizer along that path. All three operations are declared opaque, so every later use reads them through their specifications and through the projection equations rather than through their construction.

The operator ℩ takes a contractibility proof and returns the centre's first component, an element of the carrier S. Applying it to hasPairL a b and hasUnionL a gives two functions on constructible sets. Their inputs are carrier elements, that is, sets packaged with constructibility certificates, so each operation needs no further argument beyond what its inputs already carry.

opaque
  pairʟ : S → S → S
  pairʟ a b = ℩ (hasPairL a b)

  unionʟ : S → S
  unionʟ a = ℩ (hasUnionL a)

The internal successor composes the two: sucʟ a = unionʟ (pairʟ a (pairʟ a a)). The inner pair is the unordered pair of a with itself; the singleton law, applied to underlying sets later, identifies this inner pair with {a}, while the outer pair has entries a and that singleton, which is how the expression collapses to a ∪ {a}. It is the outer unordered pair and its two entries here, not an ordered pair or one of its components.

  sucʟ : S → S
  sucʟ a = unionʟ (pairʟ a (pairʟ a a))

Projection equations

Contractibility identifies the extracted operations with the ambient hierarchy's unordered pair and union, yielding projection equations for the internal successor.

The centre of a contractible type is not, on the face of it, the set the hierarchy would have built: the operations are opaque here, so this chapter compares them with the hierarchy through projection equations rather than by unfolding them. But contractibility says more than existence: every realizer is the centre. So the proof builds an explicit realizer from whatever stage data is at hand and applies the contraction to it, obtaining a path from the centre to it. Each such contraction is applied inside an elimination of truncated data whose target is an equality between hierarchy sets; that target is a proposition because the hierarchy's carrier is an h-set, which is what makes the elimination legal.

The statement fixes the target: the underlying set of the extracted pair must equal the hierarchy's unordered pair of the underlying sets. The elimination PT.rec opens the merely existing common-stage data isL-directed supplies, and it is legal precisely because the goal is the equality fst (pairʟ a b) ≡ ⁅ fst a , fst b ⁆, and setIsSet (fst (pairʟ a b)) ⁅ fst a , fst b ⁆ proves that this equality type is a proposition. Inside, the incoming data σ , oσ , fa∈ , fb∈ is exactly what PairOf.mkPair consumes, so mkPair builds a realizer from it. The path the certificate provides goes from the centre to that realizer, not the other way.

  pairʟ-fst : (a b : S) → fst (pairʟ a b) ≡ ⁅ fst a , fst b ⁆
  pairʟ-fst a b = PT.rec (setIsSet (fst (pairʟ a b)) ⁅ fst a , fst b ⁆)
    (λ { (σ , (oσ , (fa∈ , fb∈))) →
         cong (λ (e : SetOf (PairOf.Q a b)) → fst (fst e))
           (hasPairL a b .snd (PairOf.mkPair a b σ oσ fa∈ fb∈)) })

The last step identifies the center with the explicitly built realizer. The contraction hasPairL a b .snd sends any realizer to a path starting at the center and ending at that realizer; applied to mkPair a b σ oσ fa∈ fb∈, it yields a path in the type SetOf (PairOf.Q a b), which packages a carrier element with its realizing specification. Congruence of the projection λ e → fst (fst e), which reads out the carrier element and then its underlying set, turns that path into an equation between underlying sets, closing the goal. Note that the truncated common-stage data is eliminated only into this set equality, whose propositionhood setIsSet supplies. The union case is the same argument one input short: UnionOf.mkUnion needs a single stage containing fst a, and the certificate a .snd is exactly such merely existing stage data, so the elimination consumes it directly.

    (isL-directed (fst a) (fst b) (a .snd) (b .snd))

  unionʟ-fst : (a : S) → fst (unionʟ a) ≡ ⋃ (fst a)
  unionʟ-fst a = PT.rec (setIsSet (fst (unionʟ a)) (⋃ (fst a)))
    (λ { (σ , (oσ , fa∈)) →
         cong (λ (e : SetOf (UnionOf.Q a)) → fst (fst e))

Read the result: fst (unionʟ a) ≡ ⋃ (fst a), the underlying set of the model's union operation is the hierarchy's union of the underlying set. Together with the pairing equation, every set assembled from the model's pairing and union reads, through its underlying set, as the same set assembled from the hierarchy's operations. This is what the projection equations are for: comparing the two successor operations, and with them the two numeral chains, one step at a time.

           (hasUnionL a .snd (UnionOf.mkUnion a σ oσ fa∈)) })
    (a .snd)

The successor equation is the projection equations composed, plus the hierarchy's own identification of {a, a} with {a}. Unfold the outer union, then the outer pair, then the inner pair, then collapse the doubled singleton, and what is left is the hierarchy's successor.

Each congruence rewrites one nested position at a time, so the composition runs from the outside in. The direction of each factor matters. The pair equation points from the extracted center to the hierarchy's pair, so congruence over the surrounding union-of-pair shape carries the whole term toward the hierarchy's form, and pair-singleton is used at the end in exactly its stated direction.

The first three factors rewrite the outer layers. The union projection at pairʟ a (pairʟ a a) gives fst (unionʟ ...) ≡ ⋃ (fst (pairʟ a (pairʟ a a))). Applying the function ⋃_ to the outer equation pairʟ-fst a (pairʟ a a) rewrites its argument to ⋃ ⁅ fst a , fst (pairʟ a a) ⁆. Applying λ w → ⋃ ⁅ fst a , w ⁆ to the inner equation pairʟ-fst a a then gives ⋃ ⁅ fst a , ⁅ fst a , fst a ⁆ ⁆. The inner doubled pair is equal to the singleton by pair-singleton; the final factor applies that equality inside the same surrounding function.

  sucʟ-fst : (a : S) → fst (sucʟ a) ≡ sucV (fst a)
  sucʟ-fst a =
      unionʟ-fst (pairʟ a (pairʟ a a))
    ∙ cong ⋃_ (pairʟ-fst a (pairʟ a a))
    ∙ cong (λ w → ⋃ ⁅ fst a , w ⁆) (pairʟ-fst a a)

The last factor is where the hierarchy's own law enters: pair-singleton (fst a) is the path identifying the doubled pair ⁅ fst a , fst a ⁆ with the singleton ⁅ fst a ⁆. Composed under the same congruence shape, it turns the term into ⋃ ⁅ fst a , ⁅ fst a ⁆ ⁆, which is exactly sucV (fst a). The chain of factors thus verifies the statement: the internal successor, read through its underlying set, is the hierarchy's successor.

    ∙ cong (λ w → ⋃ ⁅ fst a , w ⁆) (pair-singleton (fst a))

The chain

Primitive recursion defines numeralL from the internal zero and successor, and induction proves numeralL-fst, its equality with the ambient numeral.

With the successor equation in hand, the chain is written by ordinary recursion on a natural number, and one induction says it projects onto the hierarchy's numerals. The zero stage is the internal empty set, whose underlying set is the empty set on the nose.

What this section provides is each individual numeral as an element of the carrier, together with its membership behavior. It does not collect all numerals into a set, and it does not prove Infinity; the chain is simply the successor equation iterated, so the induction has one interesting step and the zero case is a computation.

The definition has two clauses. The zeroth stage is ∅ʟ, the internal empty set, and each later stage is the internal successor applied to the previous one. Because the recursion is on the natural number index, the chain is an explicit function ℕ → S: every stage is an element of the carrier, since ∅ʟ, pairʟ and unionʟ all return such elements, and the internal successor preserves this at every iteration. Each stage thus arrives packaged with its constructibility certificate.

  numeralL : ℕ → S
  numeralL zero    = ∅ʟ
  numeralL (suc n) = sucʟ (numeralL n)

  numeralL-fst : (n : ℕ) → fst (numeralL n) ≡ # n
  numeralL-fst zero    = refl

The alignment with the ambient numerals is proved by induction on n. At zero, both sides compute to the empty set, so the path is refl. At the successor, the equation sucʟ-fst applied at numeralL n identifies fst (numeralL (suc n)) with sucV (fst (numeralL n)), and congruence of sucV over the induction hypothesis fst (numeralL n) ≡ # n moves the induction step inside the successor. The composite has exactly the shape of the defining recursion of # (suc n), so the two chains agree at every stage.

  numeralL-fst (suc n) = sucʟ-fst (numeralL n) ∙ cong sucV (numeralL-fst n)

The two pinning equations

numeralL-zero proves that internal zero has no members, while numeralL-suc characterizes the next numeral as the preceding members together with its predecessor.

The model record demands these two laws of a numeral chain: zero must be empty, and each successor must have exactly the members of its predecessor together with the predecessor itself, both stated through membership rather than through the derived operations. That phrasing is what keeps the proofs short: each is a fact about the hierarchy's numerals, transported along the projection family numeralL-fst. Nothing here unfolds a description operator.

The vehicle is the module NumPin, which takes a hierarchy-valued chain a : ℕ → V ℓ together with an alignment q : (n : ℕ) → a n ≡ # n and returns the two pinning equations for that chain. Our chain supplies the underlying-set family λ k → fst (numeralL k) and the alignment numeralL-fst.

The zero equation has the shape of a refutation: a member z of the chain's zeroth stage yields an inhabitant of the empty host type. The resulting function type is itself a proposition in the hProp setting. pinZero transports the assumed membership along the alignment at stage zero, turning membership in fst (numeralL zero) into membership in # zero, and the hierarchy's own fact that nothing is a member of ∅ then closes the proof. The transport runs one way only: from the chain to the library numeral.

numeralL-zero : (z : S) → ⟨ z ∈ˢ numeralL zero ⟩ → Empty.⊥
numeralL-zero z = NumPin.pinZero (λ k → fst (numeralL k)) numeralL-fst (fst z)

numeralL-suc : (n : ℕ) (z : S)
             → (⟨ z ∈ˢ numeralL (suc n) ⟩
                  → ⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩)

The successor equation is a pair of implications, and its second component speaks of the structure equality ≈ˢ; for this restriction structure, that relation is the underlying path fst z ≡ fst (numeralL n). Forward, a member of numeralL (suc n) is transported along the alignment at stage suc n into membership in # (suc n), where the hierarchy's own analysis of membership in sucV splits it, merely, between a member of # n and the case of # n itself; each branch is then transported back along the reverse alignment at stage n. Backward, a member of numeralL n is transported to # n and placed into # (suc n) by ∈sucV-inl, and an element equal to numeralL n transports its path to # n and uses the hierarchy's fact that a set belongs to its own successor. Both directions are pinSuc's output for the chain λ k → fst (numeralL k) and the alignment numeralL-fst, instantiated at fst z.

             × (⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩
                  → ⟨ z ∈ˢ numeralL (suc n) ⟩)
numeralL-suc n z = NumPin.pinSuc (λ k → fst (numeralL k)) numeralL-fst n (fst z)

Recap

numeralL is an internal copy of the von Neumann numerals inside L, with the exact zero and successor membership laws the model record requires.

The chapter's argument has three layers. The internal successor is built from the operations that unique existence hands over as contractibility centres, and the projection equations identify, propositionally, the underlying sets of those operations with the hierarchy's unordered pair, union, and successor. Recursion on a natural number then iterates the internal successor from the internal empty set, and induction proves numeralL-fst, the family of paths aligning each stage's underlying set with the ambient numeral # n. Finally numeralL-zero and numeralL-suc follow by applying NumPin to that alignment, so the two membership laws hold for the internal chain while all the case analysis happens at the hierarchy's numerals.

What has been established concerns individual numerals: each numeralL n exists inside L and has the right membership behavior. No statement here collects the stages into a set, and infinity is not proved in this chapter. Beyond the numerals, the projection equations say that anything assembled from the model's pairing and union reads, through its underlying set, as the same thing assembled from the hierarchy's operations.