[[!redirects functors]] ## Definition ## Let $A$ and $B$ be [[precategories]]. A **functor** $F : A \to B$ consists of * A function $F_0 : A_0 \to B_0$ * For each $a,b:A$, a function $F_{a,b}:hom_A(a,b) \to hom_B(F a,F b)$, generally also denoted $F$. * For each $a:A$, we have $F(1_a)=1_{F a}$. * For each $a,b,c: A$ and $f:hom_A(a,b)$ amd $g:hom_A(b,c)$, we have $$F(g \circ f) = F g \circ F f$$ ## Properties ## By induction on [[identity]], a functor also preserves $idtoiso$ (See [[precategory]]). ## See also ## [[Category theory]] [[natural transformation]] [[full functor]] [[faithful functor]] ## References ## [[HoTT Book]] category: category theory