Homotopy Type Theory
Rezk completion (Rev #5)

Idea

There is a canonical way to turn any precategory into a weakly equivalent category. This can be thought of as an analogue of univalence but for isomorphisms? instead of equivalences.

Construction

Theorem 9.9.5

For any precategory AA, there is a category A^\hat{A} and a weak equivalence AA^A\to \hat{A}.

Proof. 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 precategory), 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 equivlance. \square

  • 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 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 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 ad e:aisobe: a \iso b, an equality je:ia=ibj e : i a = i b
  • For each a:Aa : A, an equality k(1 a)=refl iak(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)centerdotj(g).j(g \circ f)=j(f) \centerdot 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 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.

See also

Category theory Yoneda lemma weak equivalence of precategories

References

HoTT book

category: category theory

Revision on October 8, 2018 at 17:29:54 by Ali Caglayan. See the history of this page for a list of all contributions to it.