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 , the function from Lemma 9.1.4 (see precategory) is an equivalence.
The inverse of is denoted .
In a category, the type of objects is a 1-type.
Proof. It suffices to show that for any , the type is a set. But is equivalent to which is a set.
There is a canonical way to turn a precategory into a category via the Rezk completion.
Note: All precategories given can become categories via the Rezk completion.
There is a precategory , whose type of objects is , and with . 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 , there is a category with as its type of objects and with . If is a set we call this the discrete category on . In general, we call this a groupoid.
For any type , there is a precategory with as its type of objects and with . The composition operation
is defined by induction on truncation? from concatenation of the identity type. We call this the fundamental pregroupoid of .
There is a precategory whose type of objects is and with , and composition defined by induction on truncation from ordinary composition of functions. We call this the homotopy precategory of types.
Revision on September 4, 2018 at 17:30:31 by Ali Caglayan. See the history of this page for a list of all contributions to it.