9.9 The Rezk completion
To prove this, we begin with a couple of lemmas which are completely standard category theory, phrased carefully so as to make sure we are using the eliminator for correctly. One would have to be similarly careful in classical category theory if one wanted to avoid the axiom of choice: any time we want to define a function, we need to characterize its values uniquely somehow.
If are precategories and is an essentially surjective functor, then is faithful.
If are precategories and is essentially surjective and full, then is fully faithful.
It remains to show fullness. Thus, let and . We claim that for any , the type
Now take . Then given any other and , we must show . Since is full, there merely exists a morphism such that . And since our goal is a mere proposition, we may assume given some such . Then we have
Thus, (9.9.3) is inhabited. It remains to show it is a mere proposition. Let be such that for all and , we have both and . The dependent product types are mere propositions, so all we have to prove is . But this is a mere proposition, so we may assume and , in which case we have
This proves that (9.9.3) is contractible for all . Now we define by taking to be the unique in (9.9.3) for that . To see that this is natural, suppose given ; we must show . As before, we may assume and , and likewise and . Since is full as well as essentially surjective, we may also assume with .
Since is natural, . Using the definition of , we have
Thus, is natural. Finally, for any , applying the definition of to and , we obtain . Hence, . ∎
The rest of the theorem follows almost exactly the same lines, with the category-ness of inserted in one crucial step, which we have italicized below for emphasis. This is the point at which we are trying to define a function into objects without using choice, and so we must be careful about what it means for an object to be “uniquely specified”. In classical category theory, all one can say is that this object is specified up to unique isomorphism, but in set-theoretic foundations this is not a sufficient amount of uniqueness to give us a function without invoking . In univalent foundations, however, if is a category, then isomorphism is equality, and we have the appropriate sort of uniqueness (namely, living in a contractible space).
If are precategories, is a category, and is a weak equivalence, then is an isomorphism.
By \autorefct:functor-cat, and are categories. Thus, by \autorefct:eqv-levelwise it will suffice to show that is an equivalence. But since we know from the preceding two lemmas that it is fully faithful, by \autorefct:catweq it will suffice to show that it is essentially surjective. Thus, suppose ; we want there to merely exist a such that .
For each , let be the type whose elements consist of:
An element ; and
For each and , an isomorphism ; such that
For each and as in 2 and each such that , we have .
We claim that for any , the type is contractible. As this is a mere proposition, we may assume given and . Let . Next, given and , since is fully faithful there is a unique isomorphism with ; define . Finally, if , then , hence and thus . Therefore, is inhabited.
Now suppose given another . Then . Since is a category, we have with . And for any and , by 3 for with , we have
This gives the requisite data for an equality , completing the proof that is contractible.
Now since is contractible for each , the type is also contractible. In particular, it is inhabited, so we have a function assigning to each a and a . Define to be this ; this gives a function .
Next we need to define the action of on morphisms. For each and , let be the type whose elements consist of:
A morphism , such that
For each and , and each and , and any , we have
We claim that for any and , the type is contractible. As this is a mere proposition, we may assume given and , and each and . Then since is fully faithful, there is a unique such that . Define .
Now for any , and such that , we have , hence there is a unique with and hence . Similarly, we have a unique with . Now by 3, we have and . We also have
and hence since is fully faithful. Finally, we can compute
This completes the proof that is inhabited. To show it is contractible, since hom-sets are sets, it suffices to take another satisfying 2 and show . However, we still have our specified around, and 2 implies both and must be equal to .
This completes the proof that is contractible for each and . Therefore, there is a function assigning to each such its unique inhabitant; denote this function . The proof that is a functor is straightforward; in each case we can choose and apply 2.
Finally, for any , defining and , where is the unique isomorphism with , gives an element of . Thus, it is equal to the specified one; hence . Similarly, for we can define an element of by transporting along these equalities, which must therefore be equal to the specified one. Hence, we have , and thus as desired. ∎
Therefore, if a precategory admits a weak equivalence functor , then that is its “reflection” into categories: any functor from into a category will factor essentially uniquely through . We now give two constructions of such a weak equivalence.
For any precategory , there is a category and a weak equivalence .
Let be the Yoneda embedding. This is fully faithful by \autorefct:yoneda-embedding, and essentially surjective by definition of . Thus it is a weak equivalence. ∎
This proof is very slick, but it has the drawback that it increases universe level. If is a category in a universe , then in this proof must be at least as large as . Then and are not themselves categories in , but only in a higher universe, and a priori the same is true of . One could imagine a resizing axiom that could deal with this, but it is also possible to give a direct construction using higher inductive types.
We define a higher inductive type with the following constructors:
A function .
For each and , an equality .
For each , an equality .
For each , , and , an equality .
1-truncation: for all and and , an equality .
Note that for any and , we have . This follows by path induction on and the third constructor.
The type will be the type of objects of ; we now build all the rest of the structure. (The following proof is of the sort that can benefit a lot from the help of a computer proof assistant: it is wide and shallow with many short cases to consider, and a large part of the work consists of writing down what needs to be checked.)
Step 1: We define a family by double induction on . Since \setis a 1-type, we can ignore the 1-truncation constructor. When and are of the form and , we take . It remains to consider all the other possible pairs of constructors.
Let us keep fixed at first. If varies along the identity , for some , we require an identity . By univalence, it suffices to give an equivalence . We take this to be the function . To see that this is an equivalence, we give its inverse as , with witnesses to inversion coming from the fact that is the inverse of in .
As varies along the identity , we require an identity ; this follows from the identity axiom of a precategory. Similarly, as varies along the identity , we require an identity , which follows from associativity.
Now we consider the other constructors for . Say that varies along the identity , for some ; we again must deal with all the constructors for . If is , then we require an identity . By univalence, this may come from an equivalence, and for this we can use , with inverse .
Still with varying along , suppose now that also varies along for some . Then we need to know that the two concatenated identities
are identical. This follows from associativity: . The other two constructors for are trivial, since they are 2-fold equalities in sets.
For the next two constructors of , all but the first constructor for is likewise trivial. When varies along and is , we use the identity axiom again. Similarly, when varies along , we use associativity again. This completes the construction of .
Step 2: We give the precategory structure on , always by induction on . We are now eliminating into sets (the hom-sets of ), so all but the first two constructors are trivial to deal with.
For identities, if is then we have and we define . If varies along for , we must show that . But by definition of , transporting along is given by composing with and , and we have .
For composition, if are respectively, then reduces to and we can define composition in to be composition in . And when , , or varies along , then we verify the following equalities:
Finally, the associativity and unitality axioms are mere propositions, so all constructors except the first are trivial. But in that case, we have the corresponding axioms in .
Step 3: We show that is a category. That is, we must show that for all , the function is an equivalence. First we define, for all , a function by induction. As before, since our goal is a set, it suffices to deal with the first two constructors.
When and are and respectively, we have , with composition and identities inherited as well, so that is equivalent to . But now we have the constructor .
Next, if varies along for some , we must show that for we have . But by definition of on equalities, transporting along is equivalent to post-composing with , so this equality follows from the last constructor of . The remaining case when varies along for is similar. This completes the definition of .
Now one thing we must show is that if , then . By induction on , we may assume it is , and hence . Now we argue by induction on , and since our goal is a mere proposition (since is a 1-type), all constructors except the first are trivial. But if is , then , which is equal to by the third constructor of .
To complete the proof that is a category, we must show that if , then . By induction we may assume that and are and respectively, in which case must arise from an isomorphism and we have . However, for any we have , so in particular . And by definition of on equalities, this is given by composing with the equivalence , hence is equal to .
Note the similarity of this step to the encode-decode method used in \autorefsec:compute-coprod,sec:compute-nat,cha:homotopy. Once again we are characterizing the identity types of a higher inductive type (here, ) by defining recursively a family of codes (here, ) and encoding and decoding functions by induction on and on paths.
Step 4: We define a weak equivalence . We take , and by construction of we have functions forming a functor . This functor is fully faithful by construction, so it remains to show it is essentially surjective. That is, for all we want there to merely exist an such that . As always, we argue by induction on , and since the goal is a mere proposition, all but the first constructor are trivial. But if is , then of course we have and , hence . (Note that if we were trying to prove to be split essentially surjective, we would be stuck, because we know nothing about equalities in and thus have no way to deal with any further constructors.) ∎
We have seen that most precategories arising in practice are categories, since they are constructed from , which is a category by the univalence axiom. However, there are a few cases in which the Rezk completion is necessary to obtain a category.
Recall from \autorefct:hoprecat that there is a precategory whose type of objects is and with . Its Rezk completion may be called the homotopy category of types. Its type of objects can be identified with (see \autorefct:ex:hocat).
The Rezk completion also allows us to show that the notion of “category” is determined by the notion of “weak equivalence of precategories”. Thus, insofar as the latter is inevitable, so is the former.
A precategory is a category if and only if for every weak equivalence of precategories , the induced functor is an isomorphism of precategories.
“Only if” is \autorefct:cat-weq-eq. In the other direction, let be . Then since is an equivalence, there exists such that . Hence , but again since is an equivalence, this implies . By \autorefct:isoprecatLABEL:item:ct:ipc3, is an isomorphism of precategories. But then since is a category, so is . ∎
|Title||9.9 The Rezk completion|