Homotopy Type Theory



A precategory AA consists of the following.

  • A type A 0A_0, whose elements are called objects. Typically AA is coerced to A 0A_0 in order to write x:Ax:A for x:A 0x:A_0.

  • For each a,b:Aa,b:A, a set hom A(a,b)hom_A(a,b), whose elements are called arrows or morphisms.

  • For each a:Aa:A, a morphism 1 a:hom A(a,a)1_a:hom_A(a,a), called the identity morphism.

  • For each a,b,c:Aa,b,c:A, a function

    hom A(b,c)hom A(a,b)hom A(a,c)hom_A(b,c) \to hom_A(a,b) \to hom_A(a,c)

    called composition, and denoted infix by gfgfg \mapsto f \mapsto g \circ f, or sometimes gfgf.

  • For each a,b:Aa,b:A and f:hom A(a,b)f:hom_A(a,b), we have f=1 bff=1_b \circ f and f=f1 af=f\circ 1_a.

  • For eagh a,b,c,d:Aa,b,c,d:A,

    f:hom A(a,b),g:hom A(b,c),h:hom A(c,d)f:hom_A(a,b),\ g:hom_A(b,c),\ h:hom_A(c,d)

    we have h(gf)=(hg)fh\circ (g\circ f)=(h\circ g)\circ f.


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


Rezk completion


HoTT Book

category: category theory

Last revised on September 6, 2018 at 17:55:23. See the history of this page for a list of all contributions to it.