---
title: "The cumulative hierarchy"
module: V.Hierarchy
lang: en
site: "Bedrock"
description: "The cumulative hierarchy"
stage: "The ambient hierarchy"
reading_order: 20
canonical: https://bedrock.institute/en/V.Hierarchy.html
html: V.Hierarchy.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Hierarchy.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure]
routes: [ambient-model]
translations: [https://bedrock.institute/zh/V.Hierarchy.md, https://bedrock.institute/ja/V.Hierarchy.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# The cumulative hierarchy

Every model of the language of set theory needs a carrier of "sets" together with an equality and a membership, both valued in propositions. This chapter builds that carrier. It is the cumulative hierarchy `V`, a higher inductive type built on the oldest idea in set theory, that a set is nothing over and above its members. The type takes the idea literally. Every set is presented by a family of sets indexed by a small type, one member for each index, and to be a member of it is just to have an index of that family that hits the element. Two presentations with the same members present the same set, so extensionality is not an axiom this model has to demand but the way the type is constructed.

On this carrier the chapter then builds the structure `𝒮ᵥ` and proves the first set-theoretic properties, from extensionality to a recursion principle along membership. The hierarchy natively supplies what a structure asks for: equality between sets is the path type, proposition-valued because the hierarchy is an h-set, and membership is the hierarchy's own `∈`, already valued in `hProp`. One universe level `ℓ` is fixed once, and every construction in the chapter is stated at that level.

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

open import Base.Prelude

module V.Hierarchy {ℓ : Level} where

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

Two ideas carry the hardest proof of the chapter. The first is propositional truncation. The statement "some index does the job" is kept as a mere existence, with no chosen witness, and a truncated statement may be eliminated only into propositions. The second is accessibility, the inductive data `Acc` that accompanies a well-founded relation: an element is accessible when every step down, from the element to one of its members, lands at an element that is itself accessible. The two fit because membership in the hierarchy is itself truncated. The proof of well-foundedness must turn a merely existing index into an accessibility proof; accessibility is a proposition, and only into propositions may a truncated statement be eliminated.

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

The hierarchy itself deserves a close reading, for everything that follows rests on it. Its constructor `sett` forms, from a small index type and a family into the hierarchy, the set that is the image of that family. Membership `y ∈ sett X ix` is a truncated preimage: it holds when some `i : X` has `ix i ≡ y`, and only so. A path constructor identifies any two `sett` presentations whose members agree, which is extensionality built into the type itself. This type is not defined here; the chapter builds the structure `𝒮ᵥ` on top of it and proves the set-theoretic properties of that structure.

```agda
  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 type turns the idea into data with two restrictions worth noting. Index types must be small, of the form `X : Type ℓ`, so every set is assembled from `ℓ`-small data; and the whole type is an h-set by `setIsSet`, so that however presentations are identified, no distinguishable structure remains between the results.

## The structure

The packaging question is what the structure record asks for, and the answer here is that the hierarchy already has all of it. A carrier of sets: `V ℓ` supplies one, and its h-set condition is not an extra requirement but a fact the hierarchy proves of itself. An equality valued in propositions: paths between elements of an h-set form a proposition, so the path type qualifies. A membership valued in propositions: the hierarchy's own `∈` already lands in `hProp`. Nothing has to be manufactured; the fields assemble into the structure `𝒮ᵥ`, on which the first-order language is interpreted. The subscript is a plain `v`, for the hierarchy.

The equality field makes the choice explicit: `_≈ˢ_` sends `x` and `y` to the pair of the path type `x ≡ y` and the proof `setIsSet x y` that this type is a proposition, which is exactly the shape of an element of `hProp (ℓ-suc ℓ)`. The same h-set theorem has two roles in the structure: `setIsSet` supplies the field `isSetS`, while `setIsSet x y` proves that the path type used for equality is a proposition. The paths themselves need no conversion: for an h-set, the type of paths between two elements already is a proposition, and the field simply records that type together with the certificate it comes with.

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

The membership field `_∈ˢ_` is simply the hierarchy's own `∈`, whose value at each pair is already an element of `hProp (ℓ-suc ℓ)`. Since the structure's relations are proposition-valued, many later arguments need the underlying type of a proposition rather than the proposition itself. Opening `hPropStructure 𝒮ᵥ` provides that reading: `x ∈ᵗ y` names the type `⟨ x ∈ˢ y ⟩` of inhabitants of the membership proposition. They are the same relation read two ways, `∈ˢ` giving the proposition and `∈ᵗ` its underlying type. Well-foundedness and induction will be stated for this reading.

```agda
  ; _∈ˢ_   = _∈_ }

open hPropStructure 𝒮ᵥ
```

Before the proofs begin, one feature of the levels deserves comment. The carrier `V ℓ` lives in `Type (ℓ-suc ℓ)`, one universe above its index types, and the values of the relations live in `hProp (ℓ-suc ℓ)` alongside it: the hierarchy is a large type built from small indexing data. A small membership `∈ₛ`, connected to the large one by `∈∈ₛ`, will reappear in the proofs below.

## Extensionality and well-founded membership

Suppose two sets `a` and `b` agree at every point: for each `x`, there is a path between the propositions `x ∈ a` and `x ∈ b`. Then any member of `a` transports along that path to a member of `b`, and conversely, so `a` and `b` mutually include each other. The library's `extensionality` turns exactly this mutual inclusion into a path `a ≡ b`, and `subst` carries membership along the pointwise paths to produce it. Extensionality for the hierarchy is thus a consequence of its definition, not an additional assumption.

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

The hypothesis `h` gives, for every `x`, a path between the propositions `x ∈ a` and `x ∈ b`; the goal is the path `a ≡ b`. The library's `extensionality` expects small membership, so the proof runs through the bridge `∈∈ₛ` in one direction. An input `x∈ₛa` is a small membership of `x` in `a`. Its conversion `∈∈ₛ .snd x∈ₛa` goes from small to large, producing an inhabitant of `x ∈ a`. Then `subst ⟨_⟩ (h x)` transports that inhabitant along the pointwise path, and since `h x` says the two membership propositions agree at `x`, the transported value inhabits `x ∈ b`. Finally `∈∈ₛ .fst` converts back from large to small, yielding a small membership of `x` in `b`. That is the forward component of the mutual inclusion that `extensionality` takes as input.

```agda
      (subst ⟨_⟩ (sym (h x)) (∈∈ₛ {a = x} {b = b} .snd x∈ₛb))) )
```

The second component is the same run of the bridge in reverse: a small membership of `x` in `b` is converted to large, transported backward along `sym (h x)`, and converted back to a small membership of `x` in `a`. Together the two components form the mutual inclusion from which `extensionality` produces `a ≡ b`, the path `extensionalV` returns.

(The `∈ₛ` appearing through `∈∈ₛ` is the library's *small* membership; the chapter "Small presentations of sets" discusses it in detail. Here it serves only to connect the two.)

Regularity, in this development, is the statement that membership is well-founded: every element of the carrier is accessible under `∈ᵗ`, in the sense of the accessibility data `Acc` introduced above. The proof eliminates the higher inductive type into the family `λ s → Acc _∈ᵗ_ s`. Elimination into an arbitrary family is not always available; what makes it legitimate here is that each `Acc _∈ᵗ_ s` is a proposition, and `isPropAcc s` supplies precisely that certificate. In the `sett` case, the branch receives the family `ix` and an induction hypothesis `rec i : Acc _∈ᵗ_ (ix i)` for every index. It must assemble `Acc _∈ᵗ_ (sett X ix)`, which by the shape of `acc` amounts to providing accessibility for an arbitrary member `y` of the set.

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

For such a member `y`, the witness `y∈` gives only the propositional truncation of a pair `(i , p)` with `p : ix i ≡ y`. The call `PT.rec (isPropAcc y)` may eliminate this truncated preimage because its actual target, `Acc _∈ᵗ_ y`, is a proposition, as certified by `isPropAcc y`. Inside the branch, `subst (Acc _∈ᵗ_) p (rec i)` transports the induction hypothesis from `ix i` to `y`. The proof thus uses the index without ever choosing one globally.

```agda
           y∈))
```

The first consequence of regularity is irreflexivity: no set belongs to itself. In terms of accessibility this is immediate. An element standing in a well-founded relation to itself would contradict the accessibility data, which requires every step down to land at an accessible element. The derivation uses the `Acc` statement proved above; it is not claimed here to capture every classical formulation of Foundation.

The hypothesis `⟨ A ∈ˢ A ⟩` is an inhabitant of the underlying type of the membership proposition, which is precisely the relation `∈ᵗ` on which `regularityV` was proved. For any well-founded relation, no element can stand in the relation to itself: this is the library's irreflexivity theorem `wf→x≮x`, applied here with `regularityV` as its well-foundedness input. The result is a contradiction, witnessed by the empty type `Empty.⊥`.

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

## Recursion on membership

Well-foundedness has a computational payoff: a well-founded relation supports recursion. A value at `x` may depend on the values at every member `y` of `x`, and this dependence terminates because membership is well-founded. The target may be an arbitrary dependent type family `P`, not merely a proposition, which is what makes this a recursion principle rather than a proof principle. This is the type-theoretic form of recursion along membership, stated without an ordinal-indexed hierarchy: instead of recursing along stage indices, one recurses directly along the membership relation. Its recursion equation also holds as a propositional equality, so later arguments can compute with it.

Read the type of `∈-induction` from the outside in. The family `P` assigns to each set a type in an arbitrary universe `Type ℓ'`, so the value being constructed may genuinely vary with the set. The step function `e` receives a set `x` together with recursive values `P y` for every member `y` of `x`, where membership appears through `∈ᵗ`, the Type-valued reading of the membership proposition, and returns `P x`. What justifies the definition is `regularityV`: the library's `WFI.induction`, instantiated at this well-founded relation, converts the step function into a total family. No fresh proof of well-foundedness is needed.

```agda
∈-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 ℓ'}
```

The computation law exposes the recursive call at each member as an equation rather than leaving it hidden in the definition: `∈-induction e x` equals the step applied to `x` and to `∈-induction e y` at every member `y`. The equation is stated as a propositional equality, so it may or may not hold definitionally; stating it explicitly lets later proofs rewrite a recursively defined value by this equation whenever reduction is not definitional. The law is `WFI.induction-compute` from the library, proved for any well-founded relation, instantiated here at membership.

```agda
  (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 hierarchy `V` is a higher inductive type in which sets are images of small families and the whole type is an h-set; packaged as the structure `𝒮ᵥ`, it carries the path type as equality and the native membership as membership, both proposition-valued. Extensionality (`extensionalV`) follows from the extensional path constructor via the small-membership bridge, and well-foundedness of membership (`regularityV`) follows by elimination into accessibility. Well-foundedness in turn yields irreflexivity and the recursion principle `∈-induction` with its computation law `∈-induction-compute`. The small membership `∈ₛ` and its bridge to `∈` are taken up in the chapter "Small presentations of sets".