## Idea ## The hom-sets of a [[precategory]] are functorial in nature. ## Definition ## For any [[precategory]] $A$, we have a hom-functor $$hom_A : A^{op} \times A \to \mathit{Set}$$ It takes a pair $(a,b):(A^{op})_0 \times A_0 \equiv A_0\times A_0$ to the set $hom_A(a,b)$. For a morphism $(f,f') : hom_{A^{op} \times A}((a,b),(a',b'))$, by definition we have $f:hom_A(a',a)$ and $f': hom_A(b,b')$, so we can define $$(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 embedding]] [[Yoneda lemma]] [[precategory]] ## References ## [[HoTT book]] category: category theory