nLab Rezk completion



Category theory

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts




There is a canonical way to turn any internal category in homotopy type theory into a weakly equivalent univalent category. This can be thought of as an analogue of univalence but for isomorphisms instead of equivalence.


These results are from UFP13. Note: UFP13 calls an internal category in HoTT a “precategory” and a univalent category a “category”, but here we shall refer to the standard terminology of “category” and “univalent category” respectively.


(Theorem 9.9.5 in UFP13) For any category AA, there is a univalent category A^\hat{A} and a weak equivalence AA^A\to \hat{A}.


Let A^ 0\hat{A}_0 be the type of representable objects of Set A op\mathit{Set}^{A^{\mathrm{op}}}, with hom-sets inherited from Set A op\mathit{Set}^{A^{\mathrm{op}}}. Then the inclusion A^Set A op\hat{A} \to \mathit{Set}^{A^{\mathrm{op}}} is fully faithful and an embedding on objects. Since Set A op\mathit{Set}^{A^{\mathrm{op}}} is a category by Theorem 9.2.5 (see functor category), A^\hat{A} is also a category. Let AA^A \to \hat{A} be the Yoneda embedding. This is fully faithful by corollary 9.5.6 (See Yoneda embedding), and essentially surjective by definition of A^ 0\hat{A}_0. Thus it is a weak equivalence.

  • A^ 0 (F:Set A op) (a:A)yaF\hat{A}_0\equiv \sum_{(F : \mathit{Set}^{A^{\mathrm{op}}})} \sum_{(a:A)} \mathbf{y} a \cong F

This has the unfortunate side affect of raising the universe level. If AA is a univalent category in a universe 𝒰\mathcal{U}, then in this proof Set\mathit{Set} must at least be as large as Set 𝒰\mathit{Set}_{\mathcal{U}}. Hence the univalent category Set 𝒰\mathit{Set}_{\mathcal{U}} is in a higher universe than 𝒰\mathcal{U} hence Set A op\mathit{Set}^{A^{\mathrm{op}}} must also be in a higher universe and finally A^\hat{A} is also in a higher universe than 𝒰\mathcal{U}.

Now this can all be avoided by constructing a higher inductive type A^\hat{A} with constructors:

  • A function i:A 0A^ 0i : A_0 \to \hat{A}_0.
  • For each a,b:Aa,b:A and e:aisobe: a \iso b, an equality je:ia=ibj e : i a = i b
  • For each a:Aa : A, an equality j(1 a)=refl iaj(1_a)=refl_{i a}.
  • For each a,b,c:Aa,b,c:A, f:abf : a \cong b, and g:bcg : b \cong c, an equality j(gf)=j(f)j(g).j(g \circ f)=j(f) \cdot j(g).
  • 1-truncation: for all x,y:A^ 0x,y:\hat{A}_0 and p,q:x=yp,q: x = y and r,s:p=qr,s : p = q, an equality r=sr=s.

If we ignore the last constructor we could also write the above as A^ 0 1\| \hat{A}_0 \|_1.

We now go on to build a univalent category A^\hat{A} with a weak equivalence AA^A \to \hat{A} by taking the type of objects as A^ 0\hat{A}_0 and defining hom-sets by double induction. The advantage of this approach is that it preserves universe levels, there are a lot of things to check but it is an easy proof. The kind of proof that is well suited to a proof assistant. For the complete proof see Theorem 9.9.5 of the HoTT book.


The relation between Segal completeness (now often “Rezk completion”) for internal categories in HoTT and the univalence axiom had been pointed out in:

This was developed in

See also:

category: category theory

Last revised on June 7, 2022 at 11:10:48. See the history of this page for a list of all contributions to it.