Homotopy Type Theory category > history (Rev #1)

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.