Homotopy Type Theory category > history (Rev #4)

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$.

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

HoTT Book