Homotopy Type Theory
category (Rev #1)


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.


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


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.

Revision on September 4, 2018 at 12:10:24 by Ali Caglayan. See the history of this page for a list of all contributions to it.