Homotopy Type Theory hom functor > history (Rev #2)


The hom-sets of a precategory are functorial in nature.


For any precategory AA, we have a hom-functor

hom A:A op×ASethom_A : A^{op} \times A \to \mathit{Set}

It takes a pair (a,b):(A op) 0×A 0A 0×A 0(a,b):(A^{op})_0 \times A_0 \equiv A_0\times A_0 to the set hom A(a,b)hom_A(a,b). For a morphism (f,f):hom A op×A((a,b),(a,b))(f,f') : hom_{A^{op} \times A}((a,b),(a',b')), by definition we have f:hom A(a,a)f:hom_A(a',a) and f:hom A(b,b)f': hom_A(b,b'), so we can define

(hom A) (a,b),(a,b)(f,f)(gfgf):hom A(a,b)hom A(a,b)(hom_A)_{(a,b),(a',b')}(f,f') \equiv (g\mapsto f' g f) : hom_A(a,b) \to hom_A(a',b')

See also

Category theory functor Yoneda lemma precategory


HoTT book

category: category theory

Revision on September 6, 2018 at 21:50:32 by Ali Caglayan. See the history of this page for a list of all contributions to it.