9.9 The Rezk completion

In this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath we will give a universalPlanetmathPlanetmathPlanetmath way to replace a precategory by a categoryMathworldPlanetmath. In fact, we will give two. Both rely on the fact that “categories see weak equivalencesMathworldPlanetmath as equivalences”.

To prove this, we begin with a couple of lemmas which are completely standard category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath, phrased carefully so as to make sure we are using the eliminator for -1 correctly. One would have to be similarly careful in classical category theory if one wanted to avoid the axiom of choiceMathworldPlanetmath: any time we want to define a function, we need to characterize its values uniquely somehow.

Lemma 9.9.1.

If A,B,C are precategories and H:AB is an essentially surjective functor, then (H):CBCA is faithfulPlanetmathPlanetmath.


Let F,G:BC, and γ,δ:FG be such that γH=δH; we must show γ=δ. Thus let b:B; we want to show γb=δb. This is a mere proposition, so since H is essentially surjective, we may assume given an a:A and an isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath f:Hab. But now we have

Lemma 9.9.2.

If A,B,C are precategories and H:AB is essentially surjective and full, then (H):CBCA is fully faithful.


It remains to show fullness. Thus, let F,G:BC and γ:FHGH. We claim that for any b:B, the type

(g:homC(Fb,Gb))(a:A)(f:Hab)(γa=Gf-1gFf) (9.9.3)

is contractibleMathworldPlanetmath. Since contractibility is a mere property, and H is essentially surjective, we may assume given a0:A and h:Ha0b.

Now take g:Ghγa0Fh-1. Then given any other a:A and f:Hab, we must show γa=Gf-1gFf. Since H is full, there merely exists a morphism k:homA(a,a0) such that Hk=h-1f. And since our goal is a mere proposition, we may assume given some such k. Then we have

γa =GHk-1γa0FHk

Thus, (9.9.3) is inhabited. It remains to show it is a mere proposition. Let g,g:homC(Fb,Gb) be such that for all a:A and f:Hab, we have both (γa=Gf-1gFf) and (γa=Gf-1gFf). The dependent product types are mere propositions, so all we have to prove is g=g. But this is a mere proposition, so we may assume a0:A and h:Ha0b, in which case we have


This proves that (9.9.3) is contractible for all b:B. Now we define δ:FG by taking δb to be the unique g in (9.9.3) for that b. To see that this is natural, suppose given f:homB(b,b); we must show Gfδb=δbFf. As before, we may assume a:A and h:Hab, and likewise a:A and h:Hab. Since H is full as well as essentially surjective, we may also assume k:homA(a,a) with Hk=h-1fh.

Since γ is natural, GHkγa=γaFHk. Using the definition of δ, we have

Gfδb =GfGhγaFh-1

Thus, δ is natural. Finally, for any a:A, applying the definition of δHa to a and 1a, we obtain γa=δHa. Hence, δH=γ. ∎

The rest of the theorem follows almost exactly the same lines, with the category-ness of C 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 C is a category, then isomorphism is equality, and we have the appropriate sort of uniqueness (namely, living in a contractible space).

Theorem 9.9.4.

If A,B are precategories, C is a category, and H:AB is a weak equivalence, then (H):CBCA is an isomorphism.


By \autorefct:functor-cat, CB and CA are categories. Thus, by \autorefct:eqv-levelwise it will suffice to show that (H) 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 F:AC; we want there to merely exist a G:BC such that GHF.

For each b:B, let Xb be the type whose elements consist of:

  1. 1.

    An element c:C; and

  2. 2.

    For each a:A and h:Hab, an isomorphism ka,h:Fac; such that

  3. 3.

    For each (a,h) and (a,h) as in 2 and each f:homA(a,a) such that hHf=h, we have ka,hFf=ka,h.

We claim that for any b:B, the type Xb is contractible. As this is a mere proposition, we may assume given a0:A and h0:Ha0b. Let c0:Fa0. Next, given a:A and h:Hab, since H is fully faithful there is a unique isomorphism ga,h:aa0 with Hga,h=h0-1h; define ka,h0:Fga,h. Finally, if hHf=h, then h0-1hHf=h0-1h, hence ga,hf=ga,h and thus ka,h0Ff=ka,h0. Therefore, Xb is inhabited.

Now suppose given another (c1,k1):Xb. Then ka0,h01:c0Fa0c1. Since C is a category, we have p:c0=c1 with idtoiso(p)=ka0,h01. And for any a:A and h:Hab, by 3 for (c1,k1) with f:ga,h, we have


This gives the requisite data for an equality (c0,k0)=(c1,k1), completing the proof that Xb is contractible.

Now since Xb is contractible for each b, the type (b:B)Xb is also contractible. In particular, it is inhabited, so we have a function assigning to each b:B a c and a k. Define G0(b) to be this c; this gives a function G0:B0C0.

Next we need to define the action of G on morphisms. For each b,b:B and f:homB(b,b), let Yf be the type whose elements consist of:

  1. 1.

    A morphism g:homC(Gb,Gb), such that

  2. 2.

    For each a:A and h:Hab, and each a:A and h:Hab, and any :homA(a,a), we have


We claim that for any b,b and f, the type Yf is contractible. As this is a mere proposition, we may assume given a0:A and h0:Ha0b, and each a0:A and h0:Ha0b. Then since H is fully faithful, there is a unique 0:homA(a0,a0) such that h0H0=fh0. Define g0:ka0,h0F0(ka0,h0)-1.

Now for any a,h,a,h, and such that (hH=fh), we have h-1h0:Ha0Ha, hence there is a unique m:a0a with Hm=h-1h0 and hence hHm=h0. Similarly, we have a unique m:a0a with hHm=h0. Now by 3, we have ka,hFm=ka0,h0 and ka,hFm=ka0,h0. We also have

HmH0 =(h)-1h0H0

and hence m0=m since H is fully faithful. Finally, we can compute

g0ka,h =ka0,h0F0(ka0,h0)-1ka,h

This completesPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath the proof that Yf is inhabited. To show it is contractible, since hom-sets are sets, it suffices to take another g1:homC(Gb,Gb) satisfying 2 and show g0=g1. However, we still have our specified a0,h0,a0,h0,0 around, and 2 implies both g0 and g1 must be equal to ka0,h0F0(ka0,h0)-1.

This completes the proof that Yf is contractible for each b,b:B and f:homB(b,b). Therefore, there is a function assigning to each such f its unique inhabitant; denote this function Gb,b:homB(b,b)homC(Gb,Gb). The proof that G is a functorMathworldPlanetmath is straightforward; in each case we can choose a,h and apply 2.

Finally, for any a0:A, defining c:Fa0 and ka,h:Fg, where g:homA(a,a0) is the unique isomorphism with Hg=h, gives an element of XHa0. Thus, it is equal to the specified one; hence GHa=Fa. Similarly, for f:homA(a0,a0) we can define an element of YHf by transporting along these equalities, which must therefore be equal to the specified one. Hence, we have GH=F, and thus GHF as desired. ∎

Therefore, if a precategory A admits a weak equivalence functor AA^, then that is its “reflection” into categories: any functor from A into a category will factor essentially uniquely through A^. We now give two constructions of such a weak equivalence.

Theorem 9.9.5.

For any precategory A, there is a category A^ and a weak equivalence AA^.

First proof.

Let A^0:\setofF:𝒮etAop|(a:A).(𝐲aF), with hom-sets inherited from 𝒮etAop. Then the inclusion A^𝒮etAop is fully faithful and an embedding on objects. Since 𝒮etAop is a category (by \autorefct:functor-cat, since 𝒮et is so by univalence), A^ is also a category.

Let AA^ be the Yoneda embedding. This is fully faithful by \autorefct:yoneda-embedding, and essentially surjective by definition of A^0. Thus it is a weak equivalence. ∎

This proof is very slick, but it has the drawback that it increases universePlanetmathPlanetmath level. If A is a category in a universe 𝒰, then in this proof 𝒮et must be at least as large as 𝒮et𝒰. Then 𝒮et𝒰 and (𝒮et𝒰)Aop are not themselves categories in 𝒰, but only in a higher universe, and a priori the same is true of A^. 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.

Second proof.

We define a higher inductive type A^0 with the following constructors:

  • A function i:A0A^0.

  • For each a,b:A and e:ab, an equality je:ia=ib.

  • For each a:A, an equality j(1a)=𝗋𝖾𝖿𝗅ia.

  • For each (a,b,c:A), (f:ab), and (g:bc), an equality j(gf)=j(f)\centerdotj(g).

  • 1-truncation: for all x,y:A^0 and p,q:x=y and r,s:p=q, an equality r=s.

Note that for any a,b:A and p:a=b, we have j(𝗂𝖽𝗍𝗈𝗂𝗌𝗈(p))=i(p). This follows by path inductionMathworldPlanetmath on p and the third constructor.

The type A^0 will be the type of objects of A^; we now build all the rest of the structureMathworldPlanetmath. (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 homA^:A^0A^0\set by double induction on A^0. Since \setis a 1-type, we can ignore the 1-truncation constructor. When x and y are of the form ia and ib, we take homA^(ia,ib):homA(a,b). It remains to consider all the other possible pairs of constructors.

Let us keep x=ia fixed at first. If y varies along the identityPlanetmathPlanetmathPlanetmath je:ib=ib, for some e:bb, we require an identity homA(a,b)=homA(a,b). By univalence, it suffices to give an equivalence homA(a,b)homA(a,b). We take this to be the function (e):homA(a,b)homA(a,b). To see that this is an equivalence, we give its inverseMathworldPlanetmathPlanetmathPlanetmath as (e-1), with witnesses to inversion coming from the fact that e-1 is the inverse of e in A.

As y varies along the identity j(1b)=𝗋𝖾𝖿𝗅ib, we require an identity (1b)=𝗋𝖾𝖿𝗅homA(a,b); this follows from the identity axiom 1bg=g of a precategory. Similarly, as y varies along the identity j(gf)=j(f)\centerdotj(g), we require an identity ((gf))=(g(f)), which follows from associativity.

Now we consider the other constructors for x. Say that x varies along the identity j(e):ia=ia, for some e:aa; we again must deal with all the constructors for y. If y is ib, then we require an identity homA(a,b)=homA(a,b). By univalence, this may come from an equivalence, and for this we can use (e-1), with inverse (e).

Still with x varying along j(e), suppose now that y also varies along j(f) for some f:bb. Then we need to know that the two concatenated identities

homA(a,b)=homA(a,b)=homA(a,b)\mathrlap  and

are identical. This follows from associativity: (f)e-1=f(e-1). The other two constructors for y are trivial, since they are 2-fold equalities in sets.

For the next two constructors of x, all but the first constructor for y is likewise trivial. When x varies along j(1a)=𝗋𝖾𝖿𝗅ia and y is ib, we use the identity axiom again. Similarly, when x varies along j(gf)=j(f)\centerdotj(g), we use associativity again. This completes the construction of homA^:A^0A^0\set.

Step 2: We give the precategory structure on A^, always by induction on A^0. We are now eliminating into sets (the hom-sets of A^), so all but the first two constructors are trivial to deal with.

For identities, if x is ia then we have homA^(x,x)homA(a,a) and we define 1x:1ia. If x varies along je for e:aa, we must show that 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍xhomA^(x,x)(je,1ia)=1ia. But by definition of homA^, transporting along je is given by composing with e and e-1, and we have e1iae-1=1ia.

For compositionMathworldPlanetmath, if x,y,z are ia,ib,ic respectively, then homA^ reduces to homA and we can define composition in A^ to be composition in A. And when x, y, or z varies along je, then we verify the following equalities:

e(gf) =(eg)f,
gf =(ge-1)(ef),
(gf)e-1 =g(fe-1).

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 A.

Step 3: We show that A^ is a category. That is, we must show that for all x,y:A^, the function 𝗂𝖽𝗍𝗈𝗂𝗌𝗈:(x=y)(xy) is an equivalence. First we define, for all x,y:A^, a function kx,y:(xy)(x=y) by induction. As before, since our goal is a set, it suffices to deal with the first two constructors.

When x and y are ia and ib respectively, we have homA^(ia,ib)homA(a,b), with composition and identities inherited as well, so that (iaib) is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to (ab). But now we have the constructor j:(ab)(ia=ib).

Next, if y varies along j(e) for some e:bb, we must show that for f:ab we have j(j(e)*(f))=j(f)\centerdotj(e). But by definition of homA^ on equalities, transporting along j(e) is equivalent to post-composing with e, so this equality follows from the last constructor of A^0. The remaining case when x varies along j(e) for e:aa is similar. This completes the definition of k:(x,y:A^0)(xy)(x=y).

Now one thing we must show is that if p:x=y, then k(𝗂𝖽𝗍𝗈𝗂𝗌𝗈(p))=p. By induction on p, we may assume it is 𝗋𝖾𝖿𝗅x, and hence 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(p)1x. Now we argue by induction on x:A^0, and since our goal is a mere proposition (since A^0 is a 1-type), all constructors except the first are trivial. But if x is ia, then k(1ia)j(1a), which is equal to 𝗋𝖾𝖿𝗅ia by the third constructor of A^0.

To complete the proof that A^ is a category, we must show that if f:xy, then 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(k(f))=f. By induction we may assume that x and y are ia and ib respectively, in which case f must arise from an isomorphism g:ab and we have k(f)j(g). However, for any p we have 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(p)=p*(1), so in particular 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(j(g))=j(g)*(1ia). And by definition of homA^ on equalities, this is given by composing 1ia with the equivalence g, hence is equal to g.

Note the similarity of this step to the encode-decode method used in \autorefsec:compute-coprod,sec:compute-nat,cha:homotopyMathworldPlanetmathPlanetmath. Once again we are characterizing the identity types of a higher inductive type (here, A^0) by defining recursively a family of codes (here, (x,y)(xy)) and encoding and decoding functions by induction on A^0 and on paths.

Step 4: We define a weak equivalence I:AA^. We take I0:i:A0A^0, and by construction of homA^ we have functions Ia,b:homA(a,b)homA^(Ia,Ib) forming a functor I:AA^. This functor is fully faithful by construction, so it remains to show it is essentially surjective. That is, for all x:A^ we want there to merely exist an a:A such that Iax. As always, we argue by induction on x, and since the goal is a mere proposition, all but the first constructor are trivial. But if x is ia, then of course we have a:A and Iaia, hence Iaia. (Note that if we were trying to prove I to be split essentially surjective, we would be stuck, because we know nothing about equalities in A0 and thus have no way to deal with any further constructors.) ∎

We call the construction AA^ the Rezk completion, although there is also an argument (coming from higher topos semantics) for calling it the stack completion.

We have seen that most precategories arising in practice are categories, since they are constructed from 𝒮et, 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.

Example 9.9.6.

Recall from \autorefct:fundgpd that for any type X there is a pregroupoid with X as its type of objects and hom(x,y):x=y0. Its Rezk completion is the fundamental groupoidMathworldPlanetmathPlanetmathPlanetmath of X. Recalling that groupoidsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath are equivalent to 1-types, it is not hard to identify this groupoid with X1.

Example 9.9.7.

Recall from \autorefct:hoprecat that there is a precategory whose type of objects is U and with hom(X,Y):XY0. Its Rezk completion may be called the homotopy category of types. Its type of objects can be identified with U1 (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.

Theorem 9.9.8.

A precategory C is a category if and only if for every weak equivalence of precategories H:AB, the induced functor (H):CBCA is an isomorphism of precategories.


“Only if” is \autorefct:cat-weq-eq. In the other direction, let H be I:AA^. Then since (I)0 is an equivalence, there exists R:A^A such that RI=1A. Hence IRI=I, but again since (I)0 is an equivalence, this implies IR=1A^. By \autorefct:isoprecatLABEL:item:ct:ipc3, I is an isomorphism of precategories. But then since A^ is a category, so is A. ∎

Title 9.9 The Rezk completion