Showing changes from revision #1 to #2:
Added | Removed | Changed

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}:{\mathrm{hom}}_{A}(a,b)\to {\mathrm{hom}}_{B}(\mathrm{FaF}a,\mathrm{FbF}b)$ F_{a,b}:hom_A(a,b) \to hom_B(Fa,Fb) 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).