The cumulative hierarchy

Part 3 opens, and the tone changes. So far every model has been hypothetical:

isZFModel is a specification, and nothing yet inhabits it. This part exhibits the inhabitant, and the universe it lives on is not built by this book at all: the cubical library ships the cumulative hierarchy V as a higher inductive type, following the HoTT book. This chapter introduces that type, plugs it into the framework as a structure, and banks the first two fields of the record for free.

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

open import Base.Prelude
open import Base.Truth

module V.Hierarchy {ℓ : Level} where

open import FOL.ZFStructure using ( ZFStructure; module hPropStructure )

import Cubical.HITs.PropositionalTruncation as PT
import Cubical.Data.Empty as Empty
import Cubical.Induction.WellFounded as WellFoundedInduction
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded; isPropAcc; wf→x≮x )
open import Cubical.HITs.CumulativeHierarchy.Base
  using ( V; setIsSet; _∈_; elimProp )
open import Cubical.HITs.CumulativeHierarchy.Base
  using ( sett )  -- lint-agda: keep (prose references link through this import)
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; extensionality )

The higher inductive type

The generating idea is the oldest one in set theory: a set is no more than the collection of its members. The constructor sett takes a small index type X : Type ℓ and a family ix : X → V ℓ, and forms the set whose members are the image of ix. Membership accordingly asks for a preimage, merely: y ∈ sett X ix is the truncation of "some i : X with ix i ≡ y". Two families with the same image should give the same set, and in a higher inductive type that "should" is a constructor: a path constructor (the library calls it seteq) makes extensional equality hold by construction, and setIsSet truncates the whole type to an h-set. The library's own header describes what this buys: a model of "ZF − power set". The missing power set, and the two schemas, are exactly what the rest of this part must supply.

The structure

The interface fit is exact: the carrier is an h-set, membership lands in

hProp, and equality is simply the path type, packaged as a proposition by set-hood, the promise the structure chapter made for the propositional side, kept. Four fields, no adapter code, and every tool of Parts 1 and 2, syntax, satisfaction, representations, Levy witnesses, absoluteness, the model record itself, is available on 𝒮ᵥ at once. The subscript is a plain v, for the hierarchy.

𝒮ᵥ : ZFStructure (hPropAlgebra (ℓ-suc ℓ))
𝒮ᵥ = record
  { S      = V ℓ
  ; isSetS = setIsSet
  ; _≈ˢ_   = λ x y → (x ≡ y) , setIsSet x y
  ; _∈ˢ_   = _∈_ }

open hPropStructure 𝒮ᵥ

One reading of the levels, worth fixing early because the next chapter revolves around it: the carrier V ℓ lives in Type (ℓ-suc ℓ), one universe above its index types, and truth values live in hProp (ℓ-suc ℓ) alongside it. The hierarchy is a large type built from small indexing data.

Two fields banked for free

The model record opens with extensionality and regularity, and the hierarchy supplies both without spending anything. Extensionality is the path constructor cashing out: the record's field wants "pointwise equal membership implies equal", the library's extensionality wants mutual inclusion, and subst carries membership along the pointwise paths to convert one into the other.

extensionalV : {a b : V ℓ} → ((x : V ℓ) → (x ∈ a) ≡ (x ∈ b)) → a ≡ b
extensionalV {a} {b} h = extensionality a b
  ( (λ x x∈ₛa → ∈∈ₛ {a = x} {b = b} .fst
      (subst ⟨_⟩ (h x) (∈∈ₛ {a = x} {b = a} .snd x∈ₛa)))
  , (λ x x∈ₛb → ∈∈ₛ {a = x} {b = a} .fst
      (subst ⟨_⟩ (sym (h x)) (∈∈ₛ {a = x} {b = b} .snd x∈ₛb))) )

(The ∈ₛ appearing through ∈∈ₛ is the library's small membership; the next chapter dwells on it. Here it is only glue.)

Regularity asks that membership be well-founded, and the proof is four lines with no axiom in sight. Accessibility is a proposition (isPropAcc), so

elimProp eliminates the HIT straight into it: the members of sett X ix are merely hit by ix, and accessibility, being propositional, transports along the connecting path from the inductive hypothesis. The path constructors impose no obligations at all.

regularityV : WellFounded _∈ᵗ_
regularityV = elimProp (λ s → isPropAcc s)
  (λ X ix rec → acc (λ y y∈ →
    PT.rec (isPropAcc y)
           (λ { (i , p) → subst (Acc _∈ᵗ_) p (rec i) })
           y∈))

Its first dividend, one line: no set belongs to itself, since a self-member would be an infinite descent. The later chapters reach for this constantly.

∈-irrefl : (A : S) → ⟨ A ∈ˢ A ⟩ → Empty.⊥
∈-irrefl A = wf→x≮x regularityV {x = A}

Recursion on membership

Regularity pays its first dividend at once. A well-founded relation supports recursion, so the library's well-founded induction instantiates on membership: to define something for every set, it suffices to define it for x given its values on the members of x, into an arbitrary type family, with the recursion equation holding propositionally. This is transfinite recursion with no ordinals in sight, and Part 4 builds its universe with it.

∈-induction : ∀ {ℓ'} {P : V ℓ → Type ℓ'}
            → (∀ x → (∀ y → y ∈ᵗ x → P y) → P x)
            → ∀ x → P x
∈-induction = WellFoundedInduction.WFI.induction regularityV

∈-induction-compute : ∀ {ℓ'} {P : V ℓ → Type ℓ'}
  (e : ∀ x → (∀ y → y ∈ᵗ x → P y) → P x) (x : V ℓ)
  → ∈-induction e x ≡ e x (λ y _ → ∈-induction e y)
∈-induction-compute = WellFoundedInduction.WFI.induction-compute regularityV

Recap

The cumulative hierarchy arrives from the library as a higher inductive type: sets are images of small families, extensional equality is a constructor, and the whole type is an h-set. 𝒮ᵥ plugs it into the framework, and extensionality (extensionalV) and regularity (regularityV) are already banked. Everything still owed lives one universe down: the next chapter builds the smallness toolkit that pays for it.