#Contents# * table of contents {:toc} ## Idea ## One may consider [[nLab:internal categories]] in [[nLab:homotopy type theory]]. Under the [[nLab:relation between type theory and category theory|interpretation]] of [[nLab:HoTT]] in an [[nLab:(infinity,1)-topos]], this corresponds to the concept of a [[nLab:category object in an (infinity,1)-category]]. The general idea is presented there at _[Homotopy Type Theory Formulation](https://ncatlab.org/nlab/show/category+object+in+an+%28infinity%2C1%29-category#HomotopyTypeTheoryFormulation)_. For internal [[nLab:1-categories]] in HoTT (as opposed to more general internal [[nLab:(infinity,1)-categories]]) a comprehensive discussion was given in ([Ahrens-Kapulkin-Shulman-13](#AhrensKapulkinShulman13)). In some of the literature, the "Rezk-completeness" condition on such categories is omitted from the definition, and categories that satisfy it are called *saturated* or *univalent*. 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$. ## 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**. ## 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]]. ### Lemma 9.1.9 ### ## See also ## [[Category theory]] ## References ## * {#AhrensKapulkinShulman13} [[nLab:Benedikt Ahrens]], [[nLab:Chris Kapulkin]], [[nLab:Michael Shulman]], _Univalent categories and the Rezk completion_, Mathematical Structures in Computer Science 25.5 (2015): 1010-1039 ([arXiv:1303.0584](http://arxiv.org/abs/1303.0584)) * {#HoTTBook} [[nLab:UF-IAS-2012|Univalent Foundations Project]], chapter 9 of _[[HoTT Book|Homotopy Type Theory – Univalent Foundations of Mathematics]]_, IAS 2013 [[nLab:Coq]] code formalizing the concept of 1-categories includes the following: * _[github.com/benediktahrens/rezk_completion](https://github.com/benediktahrens/rezk_completion)_