10.5 The cumulative hierarchy

We can define a cumulative hierarchy V of all sets in a given universePlanetmathPlanetmath 𝒰 as a higher inductive type, in such a way that V is again a set (in a larger universe 𝒰′), equipped with a binary β€œmembership” relationMathworldPlanetmathPlanetmath x∈y which satisfies the usual laws of set theoryMathworldPlanetmath.

Definition 10.5.1.

The cumulative hierarchy V relative to a type universe U is the higher inductive type generated by the following constructors.

  1. 1.

    For every A:𝒰 and f:Aβ†’V, there is an element π—Œπ–Ύπ—β’(A,f) : V.

  2. 2.

    For all A,B:𝒰, f:Aβ†’V and g:Bβ†’V such that

    (βˆ€(a:A).βˆƒ(b:B).f(a)=Vg(b))∧(βˆ€(b:B).βˆƒ(a:A).f(a)=Vg(b)) (10.5.1)

    there is a path π—Œπ–Ύπ—β’(A,f)=Vπ—Œπ–Ύπ—β’(B,g).

  3. 3.

    The 0-truncation constructor: for all x,y:V and p,q:x=y, we have p=q.

In set-theoretic languagePlanetmathPlanetmath, π—Œπ–Ύπ—β’(A,f) can be understood as the set (in the sense of classical set theory) that is the image of A under f, i.e.Β \setoff(a)|a∈A. However, we will avoid this notation, since it would clash with our notation for subtypes (but seeΒ (10.5.2) and \autorefdef:TypeOfElements below).

The hierarchy V is bootstrapped from the empty map π—‹π–Ύπ–ΌπŸŽβ’(V):πŸŽβ†’V, which gives the empty setMathworldPlanetmath as βˆ…=π—Œπ–Ύπ—β’(𝟎,π—‹π–Ύπ–ΌπŸŽβ’(V)). Then the singleton {βˆ…} enters V through πŸβ†’V, defined as β‹†β†¦βˆ…, and so on. The type V lives in the same universe as the base universe 𝒰.

The second constructor of V has a form unlike any we have seen before: it involves not only paths in V (which in \autorefsec:hittruncations we claimed were slightly fishy) but truncations of sums of them. It certainly does not fit the general scheme described in \autorefsec:naturality, and thus it may not be obvious what its inductionMathworldPlanetmath principle should be. Fortunately, like our first definition of the 0-truncation in \autorefsec:hittruncations, it can be re-expressed using auxiliary higher inductive types. We leave it to the reader to work out the details (see \autorefex:cumhierhit).

At the end of the day, the induction principle for V (written in pattern matching language) says that given P:Vβ†’\set, in order to construct h:∏(x:V)P⁒(x), it suffices to give the following.

  1. 1.

    For any f:Aβ†’V, construct h⁒(π—Œπ–Ύπ—β’(A,f)), assuming as given h⁒(f⁒(a)) for all a:A.

  2. 2.

    Verify that if f:Aβ†’V and g:Bβ†’V satisfyΒ (10.5.1), then h⁒(π—Œπ–Ύπ—β’(A,f))=h⁒(π—Œπ–Ύπ—β’(B,g)), assuming inductively that h⁒(f⁒(a))=h⁒(g⁒(b)) whenever f⁒(a)=g⁒(b).

The second clause checks that the map being defined must respect the paths introduced in (10.5.1). As usual when we state higher induction principles using pattern matching, it may seem tautologous, but is not. The point is that β€œh⁒(f⁒(a))” is essentially a formal symbol which we cannot peek inside of, which h⁒(π—Œπ–Ύπ—β’(A,f)) must be defined in terms of. Thus, in the second clause, we assume equality of these formal symbols when appropriate, and verify that the elements resulting from the construction of the first clause are also equal. Of course, if P is a family of mere propositions, then the second clause is automatic.

Observe that, by induction, for each v:V there merely exist A:𝒰 and f:Aβ†’V such that v=π—Œπ–Ύπ—β’(A,f). Thus, it is reasonable to try to define the membership relation x∈v on V by setting:


To see that the definition is valid, we must use the recursion principle of V. Thus, suppose we have a path π—Œπ–Ύπ—β’(A,f)=π—Œπ–Ύπ—β’(B,g) constructed throughΒ (10.5.1). If xβˆˆπ—Œπ–Ύπ—β’(A,f) then there merely is a:A such that x=f⁒(a), but byΒ (10.5.1) there merely is b:B such that f⁒(a)=g⁒(b), hence x=g⁒(b) and xβˆˆπ—Œπ–Ύπ—β’(B,f). The converseMathworldPlanetmath is symmetricPlanetmathPlanetmath.

The subset relation xβŠ†y is defined on V as usual by


A class may be taken to be a mere predicateMathworldPlanetmathPlanetmath onΒ V. We can say that a class C:Vβ†’π–―π—‹π—ˆπ—‰ is a V-set if there merely exists v∈V such that


We may also use the conventional notation for classes, which matches our standard notation for subtypes:

\setofx|C(x):≑λx.C(x). (10.5.2)

A class C:Vβ†’π–―π—‹π—ˆπ—‰ will be called 𝒰-small if all of its values C⁒(x) lie in 𝒰, specifically C:Vβ†’π–―π—‹π—ˆπ—‰π’°. Since V lives in the same universe 𝒰′ as does the base universe 𝒰 from which it is built, the same is true for the identity types v=Vw for any v,w:V. To obtain a well-behaved theory in the absence of propositional resizing, therefore, it will be convenient to have a 𝒰-small β€œresizing” of the identity relation, which we can define by induction as follows.

Definition 10.5.3.

Define the bisimulation relation


by double induction over V, where for set⁒(A,f) and set⁒(B,g) we let:


To verify that the definition is correct, we just need to check that it respects paths π—Œπ–Ύπ—β’(A,f)=π—Œπ–Ύπ—β’(B,g) constructed throughΒ (10.5.1), but this is obvious, and that π–―π—‹π—ˆπ—‰π’° is a set, which it is. Note that u∼v is in π–―π—‹π—ˆπ—‰π’° by construction.

Lemma 10.5.4.

For any u,v:V we have (u=Vv)=(u∼v).


An easy induction shows that ∼ is reflexiveMathworldPlanetmath, so by transport we have (u=Vv)β†’(u∼v). Thus, it remains to show that (u∼v)β†’(u=Vv). By induction on u and v, we may assume they are π—Œπ–Ύπ—β’(A,f) and π—Œπ–Ύπ—β’(B,g) respectively. Then by definition, π—Œπ–Ύπ—β’(A,f)βˆΌπ—Œπ–Ύπ—β’(B,g) implies (βˆ€(a:A).βˆƒ(b:B).f(a)∼g(b)) and conversely. But the inductive hypothesis then tells us that (βˆ€(a:A).βˆƒ(b:B).f(a)=g(b)) and conversely. So by the path-constructor for V we have π—Œπ–Ύπ—β’(A,f)=Vπ—Œπ–Ύπ—β’(B,g). ∎

Now we can use the resized identity relation to get the following useful principle.

Lemma 10.5.5.

For every u:V there is a given Au:U and monic mu:Au⁒\rightarrowtail⁒V such that u=set⁒(Au,mu).


Take any presentation u=π—Œπ–Ύπ—β’(A,f) and factor f:Aβ†’V as a surjection followed by an injection:


Clearly u=π—Œπ–Ύπ—β’(Au,mu) if only Au is still in 𝒰, which holds if the kernel of eu:A⁒\twoheadrightarrow⁒Au is in 𝒰. But the kernel of eu:A⁒\twoheadrightarrow⁒Au is the pullbackPlanetmathPlanetmath along f:Aβ†’V of the identityPlanetmathPlanetmathPlanetmathPlanetmath on V, which we just showed to be 𝒰-small, up to equivalence. Now, this construction of the pair (Au,mu) with mu:Au⁒\rightarrowtail⁒V and u=π—Œπ–Ύπ—β’(Au,mu) from u:V is unique up to equivalence over V, and hence up to identity by univalence. Thus by the principle of unique choice (LABEL:cor:UC) there is a map c:Vβ†’βˆ‘(A:𝒰)(Aβ†’V) such that c⁒(u)=(Au,mu), with mu:Au⁒\rightarrowtail⁒V and u=π—Œπ–Ύπ—β’(c⁒(u)), as claimed. ∎

Definition 10.5.6.

For u:V, the just constructed monic presentation mu:Au⁒\rightarrowtail⁒V such that u=set⁒(Au,mu) may be called the type of members of u and denoted mu:[u]⁒\rightarrowtail⁒V, or even [u]⁒\rightarrowtail⁒V. We can think of [u] as the β€œsubclass of V consisting of members of u”.

Theorem 10.5.7.

The following hold for (V,∈):

  1. 1.


  2. 2.

    empty set: for all x:V, we have ¬⁑(xβˆˆβˆ…).

  3. 3.

    pairing: for all u,v:V, the class uβˆͺv:≑\setofx|x=u∨x=v is a V-set.

  4. 4.

    infinityMathworldPlanetmath: there is a v:V with βˆ…βˆˆv and x∈v implies xβˆͺ{x}∈v.

  5. 5.

    union: for all v:V, the class βˆͺv:≑\setofx|βˆƒ(u:V).x∈u∈v is a V-set.

  6. 6.

    function set: for all u,v:V, the class vu:≑\setofx|x:uβ†’v is a V-set.11Here x:uβ†’v means that x is an appropriate set of ordered pairs, according to the usual way of encoding functions in set theory.

  7. 7.

    ∈-induction: if C:Vβ†’π–―π—‹π—ˆπ—‰ is a class such that C⁒(a) holds whenever C⁒(x) for all x∈a, then C⁒(v) for all v:V.

  8. 8.

    replacement: given any r:V→V and a:V, the class


    is a V-set.

  9. 9.

    separationPlanetmathPlanetmath: given any a:V and 𝒰-small C:Vβ†’π–―π—‹π—ˆπ—‰π’°, the class


    is a V-set.

Sketch of proof.

  1. 1.

    Extensionality: if π—Œπ–Ύπ—β’(A,f)βŠ†π—Œπ–Ύπ—β’(B,g) then f⁒(a)βˆˆπ—Œπ–Ύπ—β’(B,g) for every a:A, therefore for every a:A there merely exists b:B such that f⁒(a)=g⁒(b). The assumptionPlanetmathPlanetmath π—Œπ–Ύπ—β’(B,g)βŠ†π—Œπ–Ύπ—β’(A,f) gives the other half ofΒ (10.5.1), therefore π—Œπ–Ύπ—β’(A,f)=π—Œπ–Ύπ—β’(B,g).

  2. 2.

    Empty set: suppose xβˆˆβˆ…=π—Œπ–Ύπ—β’(𝟎,π—‹π–Ύπ–ΌπŸŽβ’(V)). Then βˆƒ(a:𝟎).x=π—‹π–Ύπ–ΌπŸŽ(V,a), which is absurd.

  3. 3.

    Pairing: given u and v, let w=π—Œπ–Ύπ—β’(𝟐,π—‹π–Ύπ–ΌπŸβ’(V,u,v)).

  4. 4.

    Infinity: take w=π—Œπ–Ύπ—β’(β„•,I), where I:β„•β†’V is given by the recursion I(0):β‰‘βˆ… and I(n+1):≑I(n)βˆͺ{I(n)}.

  5. 5.

    Union: Take any v:V and any presentation f:Aβ†’V with v=π—Œπ–Ύπ—β’(A,f). Then let A~:β‰‘βˆ‘(a:A)[fa], where mf⁒a:[f⁒a]⁒\rightarrowtail⁒V is the type of members from \autorefdef:TypeOfElements. A~ is plainly 𝒰-small, and we have βˆͺv:β‰‘π—Œπ–Ύπ—(A~,Ξ»x.mf⁒(𝗉𝗋1⁒(x))(𝗉𝗋2(x))).

  6. 6.

    Function set: given u,v:V, take the types of elements [u]⁒\rightarrowtail⁒V and [u]⁒\rightarrowtail⁒V, and the function type [u]β†’[v]. We want to define a map


    with β€œr(f)=\setof(x,f(x))|x:[u]”, but in order for this to make sense we must first define the ordered pair (x,y), and then we take the map rβ€²:x↦(x,f(x)), and then we can put r(f):β‰‘π—Œπ–Ύπ—([u],rβ€²). But the ordered pair can be defined in terms of unordered pairing as usual.

  7. 7.

    ∈-induction: let C:Vβ†’π–―π—‹π—ˆπ—‰ be a class such that C⁒(a) holds whenever C⁒(x) for all x∈a, and take any v=π—Œπ–Ύπ—β’(B,g). To show that C⁒(v) by induction, assume that C⁒(g⁒(b)) for all b:B. For every x∈v there merely exists some b:B with x=g⁒(b), and so C⁒(x). Thus C⁒(v).

  8. 8.

    Replacement: the statement β€œC is a V-set” is a mere proposition, so we may proceed by induction as follows. Supposing x is π—Œπ–Ύπ—β’(A,f), we claim that w:β‰‘π—Œπ–Ύπ—(A,r∘f) is the set we are looking for. If C⁒(y) then there merely exists z:V and a:A such that z=f⁒(a) and y=r⁒(z), therefore y∈w. Conversely, if y∈w then there merely exists a:A such that y=r⁒(f⁒(a)), so if we take z:≑f(a) we see that C⁒(y) holds.

  9. 9.

    Let us say that a class C:Vβ†’π–―π—‹π—ˆπ—‰ is separablePlanetmathPlanetmath if for any a:V the class


    is a V-set. We need to show that any 𝒰-small C:Vβ†’π–―π—‹π—ˆπ—‰π’° is separable. Indeed, given a=π—Œπ–Ύπ—β’(A,f), let Aβ€²=βˆƒ(x:A).C(fx), and take fβ€²=f∘i, where i:Aβ€²β†’A is the obvious inclusion. Then we can take aβ€²=π—Œπ–Ύπ—β’(Aβ€²,fβ€²) and we have x∈a∧C⁒(x)⇔x∈aβ€² as claimed. We needed the assumption that C lands in 𝒰 in order for Aβ€²=βˆƒ(x:A).C(fx) to be in 𝒰.∎

It is also convenient to have a strictly syntactic criterion of separability, so that one can read off from the expression for a class that it produces a V-set. One such familiar condition is being β€œΞ”0”, which means that the expression is built up from equality x=Vy and membership x∈y, using only mere-propositional connectivesMathworldPlanetmath Β¬, ∧, ∨, β‡’ and quantifiersMathworldPlanetmath βˆ€, βˆƒ over particular sets, i.e.Β of the form βˆƒ(x∈a) and βˆ€(y∈b) (these are called boundedPlanetmathPlanetmathPlanetmathPlanetmath quantifiers).

Corollary 10.5.8.

If the class C:V→Prop is Δ0 in the above sense, then it is separable.


Recall that we have a 𝒰-small resizing x∼y of identity x=y. Since x∈y is defined in terms of x=y, we also have a 𝒰-small resizing of membership


Now, let Ξ¦ be a Ξ”0 expression for C, so that as classes Ξ¦=C (strictly speaking, we should distinguish expressions from their meanings, but we will blur the differencePlanetmathPlanetmath). Let Ξ¦~ be the result of replacing all occurrences of = and ∈ by their resized equivalentsMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath ∼ and ∈~. Clearly then Ξ¦~ also expresses C, in the sense that for all x:V, Ξ¦~⁒(x)⇔C⁒(x), and hence Ξ¦~=C by univalence. It now suffices to show that Ξ¦~ is 𝒰-small, for then it will be separable by the theoremMathworldPlanetmath.

We show that Ξ¦~ is 𝒰-small by induction on the construction of the expression. The base cases are x∼y and x∈~y, which have already been resized into 𝒰. It is also clear that 𝒰 is closed underPlanetmathPlanetmath the mere-propositional operations (and (-1)-truncation), so it just remains to check the bounded quantifiers βˆƒ(x∈a) and βˆ€(y∈b). By definition,

βˆƒ(x∈a)P(x) :≑βˆ₯βˆ‘x:V(x∈~a∧P(x))βˆ₯,
βˆ€(y∈b)P(x) :β‰‘βˆx:V(x∈~aβ†’P(x)).

Let us consider βˆ₯βˆ‘(x:V)(x∈~a∧P(x))βˆ₯. Although the body (x∈~a∧P⁒(x)) is 𝒰-small since P⁒(x) is so by the inductive hypothesis, the quantification over V need not stay inside 𝒰. However, in the present case we can replace this with a quantification over the type [a]⁒\rightarrowtail⁒V of members of a, and easily show that


The right-hand side does remain in 𝒰, since both [a] and P⁒(x) are in 𝒰. The case of ∏(x:V)(x∈~aβ†’P(x)) is analogous, using ∏(x:V)(x∈~aβ†’P(x))=∏(x:[a])P(x). ∎

We have shown that in type theoryPlanetmathPlanetmath with a universe 𝒰, the cumulative hierarchy V is a model of a β€œconstructive set theory” with many of the standard axioms. However, as far as we know, it lacks the strong collectionMathworldPlanetmath and subset collection axioms which are included in Constructive Zermelo–Fraenkel Set TheoryΒ [AczelCZF]. In the usual interpretationMathworldPlanetmathPlanetmath of this set theory into type theory, these two axioms are consequences of the setoid-like definition of equality; while in other constructed models of set theory, strong collection may hold for other reasons. We do not know whether either of these axioms holds in our model (V,∈), but it seems unlikely. Since V is a higher inductive type inside the system, rather than being an external construction, it is not surprising that it differs in some ways from prior interpretations.

Finally, consider the result of adding the axiom of choiceMathworldPlanetmath for sets to our type theory, in the form 𝖠𝖒 from \autorefsubsec:emacinsets above. This has the consequence that 𝖫𝖀𝖬 then also holds, by \autorefthm:1surj_to_surj_to_pem, and so \set is a topos with subobject classifier 𝟐, by \autorefthm:settopos. In this case, we have π–―π—‹π—ˆπ—‰=𝟐:𝒰, and so all classes are separable. Thus we have shown:

Lemma 10.5.9.

In type theory with AC, the law of (full) separation holds for V: given any class C:Vβ†’Prop and a:V, the class a∩C is a V-set.

Theorem 10.5.10.

In type theory with AC and a universe U, the cumulative hierarchy V is a model of Zermelo–Fraenkel set theory with choice, ZFC.


We have all the axioms listed in \autorefthm:VisCST, plus full separation, so we just need to show that there are power setsMathworldPlanetmath 𝒫⁒(a):V for all a:V. But since we have 𝖫𝖀𝖬 these are simply function types 𝒫(a)=(aβ†’πŸ). Thus V is a model of Zermelo–Fraenkel set theory ZF. We leave the verification of the set-theoretic axiom of choice from 𝖠𝖒 as an easy exercise. ∎

Title 10.5 The cumulative hierarchy