Homotopy Type Theory
category (Rev #4)


Similarly to the univalence axiom we make two notions of sameness the same. This leads to some nice concequences.


A category is a precategory such that for all a,b:Aa,b:A, the function idtoiso a,bidtoiso_{a,b} from Lemma 9.1.4 (see precategory) is an equivalence.

The inverse of idtoisoidtoiso is denoted isotoidisotoid.


Note: All precategories given can become categories via the Rezk completion.

  • There is a precategory Set\mathit{Set}, whose type of objects is SetSet, and with hom Set(A,B)(AB)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 XX, there is a category with XX as its type of objects and with hom(x,y)(x=y)hom(x,y)\equiv(x=y). If XX is a set we call this the discrete category on XX. In general, we call this a groupoid.

  • For any type XX, there is a precategory with XX as its type of objects and with hom(x,y)x=y 0hom(x,y)\equiv \| x= y \|_0. The composition operation

    y=z 0x=y 0y=z 0\|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 XX.

  • There is a precategory whose type of objects is 𝒰\mathcal{U} and with hom(X,Y)XY 0hom(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.


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:Aa,b:A, the type a=ba=b is a set. But a=ba=b is equivalent to aba \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


HoTT Book

Revision on September 5, 2018 at 14:26:28 by Ali Caglayan. See the history of this page for a list of all contributions to it.