## 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. ## 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$ ## Examples ## The [[univalence axiom]] implies immediately that $\mathcal{Set}$ is a category. One can also show that any [[precategory]] of set-level structures such as groups, rings topologicial spaces, etc. is a category.