Rezk completion (changes)

Showing changes from revision #5 to #6:
Added | ~~Removed~~ | ~~Chan~~ged

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?~~isomorphisms instead of equivalences.

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

**Proof.** Let $\hat{A}_0$ be the type of representable? objects of $\mathit{Set}^{A^{\mathrm{op}}}$, with hom-sets inherited from $\mathit{Set}^{A^{\mathrm{op}}}$. Then the inclusion $\hat{A} \to \mathit{Set}^{A^{\mathrm{op}}}$ is fully faithful and an embedding on objects?. Since $\mathit{Set}^{A^{\mathrm{op}}}$ is a category by Theorem 9.2.5 (see functor precategory), $\hat{A}$ is also a category. Let $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 $\hat{A}_0$. Thus it is a weak equivlance. $\square$

- $\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~~~~$A$~~universe ~~ is~~ level.~~ a~~ If$A$ is a category in a universe $\mathcal{U}$, then in this proof $\mathit{Set}$ must at least be as large as $\mathit{Set}_{\mathcal{U}}$. Hence the category $\mathit{Set}_{\mathcal{U}}$ is in a higher universe than $\mathcal{U}$ hence $\mathit{Set}^{A^{\mathrm{op}}}$ must also be in a higher universe and finally $\hat{A}$ is also in a higher universe than $\mathcal{U}$.

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

- A function $i : A_0 \to \hat{A}_0$.
- For each $a,b:A$ ad $e: a \iso b$, an equality $j e : i a = i b$
- For each $a : A$, an equality $k(1_a)=refl_{i a}$.
- For each $a,b,c:A$, $f : a \cong b$, and $g : b \cong c$, an equality $j(g \circ f)=j(f) \centerdot j(g).$
- 1-truncation: for all $x,y:\hat{A}_0$ and $p,q: x = y$ and $r,s : p = q$, an equality $r=s$.

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

We now go on to build a category $\hat{A}$ with a~~ weak~~~~ equivalence~~~~$A \to \hat{A}$~~weak equivalence~~ ~~~~ by~~~~ taking~~~~ the~~~~ type~~~~ of~~~~ objects~~~~ as~~${\hat{A}}_{0}A\to \hat{A}$~~ \hat{A}_0~~ A \to \hat{A} ~~ and~~~~ defining~~~~ hom-sets~~ by~~ double~~ taking~~ 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~~ type~~ proof~~~~ see~~~~ Theorem~~~~ 9.9.5~~ of~~ the~~ objects as$\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.

Category theory Yoneda lemma weak equivalence of precategories

category: category theory

Last revised on October 11, 2018 at 06:26:50. See the history of this page for a list of all contributions to it.