The numeral chain

Infinity is stated in this book in its strong form: the numerals form a set. That statement has two halves, and they are of very different difficulty. First the chain itself has to exist inside L, with zero at the bottom and each numeral the successor of the last; then that chain has to be collected, which is the axiom proper. This chapter does the first half, and it does it for free, because the previous chapter already built everything a successor is made of.

The point worth watching is a mismatch. Inside the model, the successor of a is a ∪ {a}, spelled with the model's own pairing and union, and those are ℩-projections out of unique-existence proofs rather than the library's set operations. Outside, the ambient hierarchy has its own successor, and its own chain of numerals built from it. The two chains ought to agree, but nothing so far says they do: one is assembled from contractibility centres, the other from constructors. So this chapter's real content is a family of projection equations, saying that the model's operations, read through the underlying set, are the hierarchy's operations. With those in hand the two chains coincide step by step, and the two pinning equations that the model record demands of a numeral chain follow by transporting the hierarchy's own facts along them.

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

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

open import FOL.ZFStructure using ( module hPropStructure )
import FOL.ZFModel
open import V.Model {ℓ}
  using ( pair-singleton; ∈sucV-elim; ∈sucV-inl; self∈sucV )
open import L.Constructible {ℓ} using ( 𝒮ʟ )
open import L.Axioms.Basic {ℓ}
  using ( hasPairL; hasUnionL; module PairOf; module UnionOf; isL-directed; ∅ʟ )

open import Cubical.Data.Sum using ( inl; inr )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; ⁅_,_⁆; ⋃_; module InfinitySet )
open InfinitySet using ( sucV; #_ )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ

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

The model's own operations

Unique existence hands over an operation: the description operator takes the contractibility proof to its centre. Pairing and union become functions on the constructible sets, and the successor is written the way the model record writes it, as the union of a pair of pairs.

The chain is sealed, and the seal is not tidiness. Everything below reads these through their projection equations and nothing reads them through their construction, so the seal costs nothing here; what it buys is one module application elsewhere. Instantiating the coding chapter at this model rather than at the hierarchy means every code is an element of L by construction, and the coding chapter proves its shape lemma by twelve refls, each of which forces whatever a pair unfolds to through normalization. Unsealed, that application does not finish in ten minutes; sealed, it costs about a third of a second.

The rule is the development's own, at a scale it had not been seen at: a constructibility certificate is expensive to carry through conversion, so seal it where the element is built. What is new is that a module application is a conversion site too, and a large one, since it re-elaborates every definition in the chapter being applied.

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

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

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

Projection equations

Now the mismatch. The centre of a contractibility proof is not, on the face of it, the set the hierarchy would have built: the proof went through a merely existing witness, so nothing computes. But contractibility says more than existence, it says every witness is the centre; and the previous chapter's construction, applied to any stage that works, is a witness. So the two agree. The truncation is harmless because the goal is an equation between sets, and the hierarchy's carrier is a set.

  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∈)) })
    (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))
           (hasUnionL a .snd (UnionOf.mkUnion a σ oσ fa∈)) })
    (a .snd)

The successor equation is the three of them 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.

  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)
    ∙ cong (λ w → ⋃ ⁅ fst a , w ⁆) (pair-singleton (fst a))

The chain

The chain is now written by ordinary recursion on a natural number, and one induction says it projects onto the hierarchy's numerals. Zero is the empty set built in the previous chapter, whose projection is the empty set on the nose.

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

  numeralL-fst : (n : ℕ) → fst (numeralL n) ≡ # n
  numeralL-fst zero    = refl
  numeralL-fst (suc n) = sucʟ-fst (numeralL n) ∙ cong sucV (numeralL-fst n)

The two pinning equations

The model record does not take the chain on trust: it demands that zero be empty and that each successor 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 deliberate, and it is what makes these two proofs cheap: each is a fact about the hierarchy's numerals, transported along the projection equation. Nothing here ever unfolds a description operator.

numeralL-zero : (z : S) → ⟨ z ∈ˢ numeralL zero ⟩ → Empty.⊥
numeralL-zero z z∈ = ∅-empty (fst z)
  (∈∈ₛ {a = fst z} {b = ∅} .fst
    (subst (λ w → ⟨ fst z ∈ w ⟩) (numeralL-fst zero) z∈))

numeralL-suc : (n : ℕ) (z : S)
             → (⟨ z ∈ˢ numeralL (suc n) ⟩
                  → ⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩)
             × (⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩
                  → ⟨ z ∈ˢ numeralL (suc n) ⟩)
numeralL-suc n z = fwd , bwd
  where
  up : ⟨ z ∈ˢ numeralL (suc n) ⟩ → ⟨ fst z ∈ sucV (# n) ⟩
  up z∈ = subst (λ w → ⟨ fst z ∈ w ⟩) (numeralL-fst (suc n)) z∈

  fwd : ⟨ z ∈ˢ numeralL (suc n) ⟩
      → ⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩
  fwd z∈ = ∈sucV-elim {A = # n} {x = fst z}
    (snd ((z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n)))
    (up z∈)
    (λ fz∈#n → ∣ inl (subst (λ w → ⟨ fst z ∈ w ⟩) (sym (numeralL-fst n)) fz∈#n) ∣₁)
    (λ fz≡#n → ∣ inr (fz≡#n ∙ sym (numeralL-fst n)) ∣₁)

  bwd : ⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩
      → ⟨ z ∈ˢ numeralL (suc n) ⟩
  bwd = PT.rec (snd (z ∈ˢ numeralL (suc n)))
    (λ { (inl z∈n) →
           subst (λ w → ⟨ fst z ∈ w ⟩) (sym (numeralL-fst (suc n)))
             (∈sucV-inl {A = # n}
               (subst (λ w → ⟨ fst z ∈ w ⟩) (numeralL-fst n) z∈n))
       ; (inr z≡n) →
           subst (λ w → ⟨ fst z ∈ w ⟩) (sym (numeralL-fst (suc n)))
             (subst (λ w → ⟨ w ∈ sucV (# n) ⟩)
               (sym (z≡n ∙ numeralL-fst n)) (self∈sucV (# n))) })

Recap

numeralL is the chain inside L, with numeralL-fst identifying it with the hierarchy's own numerals, and numeralL-zero and

numeralL-suc the two equations the model record demands of it. All of it is constructive, which is why it is a chapter of its own: the excluded middle enters infinity only at the collection step, and that step is the next chapter.

The projection equations are reusable beyond the numerals. Anything built from the model's pairing and union reads, through the underlying set, as the same thing built from the hierarchy's, and a later chapter needing a numeral as a constant of the object language takes its constructibility from here rather than from the axiom.