---
title: "The numeral chain"
module: L.Axioms.Numerals
lang: en
site: "Bedrock"
description: "The numeral chain"
stage: "Constructible stages and the axioms"
reading_order: 38
canonical: https://bedrock.institute/en/L.Axioms.Numerals.html
html: L.Axioms.Numerals.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Axioms/Numerals.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.ZFModel, V.Model, L.Constructible, L.Axioms.Basic]
routes: [constructible-axioms]
translations: [https://bedrock.institute/zh/L.Axioms.Numerals.md, https://bedrock.institute/ja/L.Axioms.Numerals.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
  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.

```agda
  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.

```agda
    (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.

```agda
           (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.

```agda
  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.

```agda
    ∙ 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.

```agda
  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.

```agda
  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.

```agda
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`.

```agda
             × (⟨ (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.