10.5 The cumulative hierarchy
We can define a cumulative hierarchy of all sets in a given universe as a higher inductive type, in such a way that is again a set (in a larger universe ), equipped with a binary “membership” relation which satisfies the usual laws of set theory.
The cumulative hierarchy relative to a type universe is the higher inductive type generated by the following constructors.
For every and , there is an element : V.
For all , and such that
there is a path .
The 0-truncation constructor: for all and , we have .
In set-theoretic language, can be understood as the set (in the sense of classical set theory) that is the image of under , i.e. . 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 is bootstrapped from the empty map , which gives the empty set as . Then the singleton enters through , defined as , and so on. The type lives in the same universe as the base universe .
The second constructor of has a form unlike any we have seen before: it involves not only paths in (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 induction 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 (written in pattern matching language) says that given , in order to construct , it suffices to give the following.
For any , construct , assuming as given for all .
Verify that if and satisfy (10.5.1), then , assuming inductively that whenever .
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 “” is essentially a formal symbol which we cannot peek inside of, which 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 is a family of mere propositions, then the second clause is automatic.
Observe that, by induction, for each there merely exist and such that . Thus, it is reasonable to try to define the membership relation on by setting:
To see that the definition is valid, we must use the recursion principle of . Thus, suppose we have a path constructed through (10.5.1). If then there merely is such that , but by (10.5.1) there merely is such that , hence and . The converse is symmetric.
The subset relation is defined on as usual by
A class may be taken to be a mere predicate on . We can say that a class is a -set if there merely exists such that
We may also use the conventional notation for classes, which matches our standard notation for subtypes:
A class will be called -small if all of its values lie in , specifically . Since lives in the same universe as does the base universe from which it is built, the same is true for the identity types for any . 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.
Define the bisimulation relation
by double induction over , where for and we let:
To verify that the definition is correct, we just need to check that it respects paths constructed through (10.5.1), but this is obvious, and that is a set, which it is. Note that is in by construction.
For any we have .
An easy induction shows that is reflexive, so by transport we have . Thus, it remains to show that . By induction on and , we may assume they are and respectively. Then by definition, implies and conversely. But the inductive hypothesis then tells us that and conversely. So by the path-constructor for we have . ∎
Now we can use the resized identity relation to get the following useful principle.
For every there is a given and monic such that .
Clearly if only is still in , which holds if the kernel of is in . But the kernel of is the pullback along of the identity on , which we just showed to be -small, up to equivalence. Now, this construction of the pair with and from is unique up to equivalence over , and hence up to identity by univalence. Thus by the principle of unique choice (LABEL:cor:UC) there is a map such that , with and , as claimed. ∎
For , the just constructed monic presentation such that may be called the type of members of and denoted , or even . We can think of as the “subclass of consisting of members of ”.
The following hold for :
empty set: for all , we have .
pairing: for all , the class is a -set.
infinity: there is a with and implies .
union: for all , the class is a -set.
-induction: if is a class such that holds whenever for all , then for all .
replacement: given any and , the class
is a -set.
separation: given any and -small , the class
is a -set.
Sketch of proof.
Empty set: suppose . Then , which is absurd.
Pairing: given and , let .
Infinity: take , where is given by the recursion and .
Union: Take any and any presentation with . Then let , where is the type of members from \autorefdef:TypeOfElements. is plainly -small, and we have .
Function set: given , take the types of elements and , and the function type . We want to define a map
with “”, but in order for this to make sense we must first define the ordered pair , and then we take the map , and then we can put . But the ordered pair can be defined in terms of unordered pairing as usual.
-induction: let be a class such that holds whenever for all , and take any . To show that by induction, assume that for all . For every there merely exists some with , and so . Thus .
Replacement: the statement “ is a -set” is a mere proposition, so we may proceed by induction as follows. Supposing is , we claim that is the set we are looking for. If then there merely exists and such that and , therefore . Conversely, if then there merely exists such that , so if we take we see that holds.
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 -set. One such familiar condition is being “”, which means that the expression is built up from equality and membership , using only mere-propositional connectives , , , and quantifiers , over particular sets, i.e. of the form and (these are called bounded quantifiers).
If the class is in the above sense, then it is separable.
Recall that we have a -small resizing of identity . Since is defined in terms of , we also have a -small resizing of membership
Now, let be a expression for , so that as classes (strictly speaking, we should distinguish expressions from their meanings, but we will blur the difference). Let be the result of replacing all occurrences of and by their resized equivalents and . Clearly then also expresses , in the sense that for all , , and hence by univalence. It now suffices to show that is -small, for then it will be separable by the theorem.
We show that is -small by induction on the construction of the expression. The base cases are and , which have already been resized into . It is also clear that is closed under the mere-propositional operations (and -truncation), so it just remains to check the bounded quantifiers and . By definition,
Let us consider . Although the body is -small since is so by the inductive hypothesis, the quantification over need not stay inside . However, in the present case we can replace this with a quantification over the type of members of , and easily show that
The right-hand side does remain in , since both and are in . The case of is analogous, using . ∎
We have shown that in type theory with a universe , the cumulative hierarchy is a model of a “constructive set theory” with many of the standard axioms. However, as far as we know, it lacks the strong collection and subset collection axioms which are included in Constructive Zermelo–Fraenkel Set Theory [AczelCZF]. In the usual interpretation 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 , but it seems unlikely. Since 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 choice 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 is a topos with subobject classifier , by \autorefthm:settopos. In this case, we have , and so all classes are separable. Thus we have shown:
In type theory with , the law of (full) separation holds for : given any class and , the class is a -set.
In type theory with and a universe , the cumulative hierarchy 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 sets for all . But since we have these are simply function types . Thus 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|