Homotopy Type Theory



A precategory AA consists of the following.


There are two notions of “sameness” for objects of a precategory. On one hand we have an isomorphism? between objects aa and bb on the other hand we have equality of objects aa and bb.

There is a special kind of precategory called a category where these two notions of equality coincide and some very nice properties arise.

Lemma 9.1.4 (idtoiso)

if AA is a precategory and a,b:Aa,b:A, then there is a map

idtoiso:(a=b)(ab)idtoiso : (a=b) \to (a \cong b)

Proof. By induction on identity, we may assume aa and bb are the same. But then we have 1 a:hom A(a,a)1_a:hom_A(a,a), which is clearly an isomorphism. \square


See category

See also

Category theory category Rezk completion


HoTT Book

category: category theory