## Idea ## Similarly to the [[univalence axiom]] we make two notions of sameness the same. This leads to some nice concequences. ## Definition ## A **category** is a [[precategory]] such that for all $a,b:A$, the function $idtoiso_{a,b}$ from Lemma 9.1.4 (see [[precategory]]) is an equivalence. The inverse of $idtoiso$ is denoted $isotoid$. ## Properties ## ### Lemma 9.1.8 ### In a category, the type of objects is a 1-type. **Proof.** It suffices to show that for any $a,b:A$, the type $a=b$ is a set. But $a=b$ is equivalent to $a \cong b$ which is a set. $\square$ There is a canonical way to turn a [[precategory]] into a category via the [[Rezk completion]]. ## Examples ## Note: All precategories given can become categories via the [[Rezk completion]]. * There is a precategory $\mathit{Set}$, whose type of objects is $Set$, and with $hom_{\mathit{Set}}(A,B)\equiv (A \to B)$. Under [[univalence]] this becomes a [[category]]. One can also show that any [[precategory]] of set-level structures such as groups, rings topologicial spaces, etc. is also a category. * For any 1-type $X$, there is a category with $X$ as its type of objects and with $hom(x,y)\equiv(x=y)$. If $X$ is a set we call this the **discrete category** on $X$. In general, we call this a **groupoid**. * For any type $X$, there is a precategory with $X$ as its type of objects and with $hom(x,y)\equiv \| x= y \|_0$. The composition operation $$\|y=z\|_0 \to \|x=y\|_0 \to \|y=z\|_0$$ is defined by induction on [[truncation]] from concatenation of the [[identity type]]. We call this the **fundamental pregroupoid** of $X$. * There is a precategory whose type of objects is $\mathcal{U}$ and with $hom(X,Y)\equiv \| X \to Y\|_0$, and composition defined by induction on truncation from ordinary composition of functions. We call this the **homotopy precategory of types**. ## See also ## [[Category theory in HoTT]] ## References ## [[HoTT Book]]