Definition. Functor [dm-000J]

Liam O'Connor

A functor $F$ from a category $\mathbf {C}$ to a category $\mathbf {D}$ consists of an object mapping that maps objects of $\mathbf {C}$ to objects of $\mathbf {D}$ , and a morphism mapping that maps morphisms of $\mathbf {C}$ to morphisms of $\mathbf {D}$ such that:

For each $A \xrightarrow {m} B$ in $\mathbf {C}$ , we have a morphism $F(A) \xrightarrow {F(m)} F(B)$ in $\mathbf {D}$ .
For each object $A$ in $\mathbf {C}$ , the equation $F(\mathsf {id}_A) = \mathsf {id}_{F(A)}$ holds in $\mathbf {D}$ .
For a pair of morphism $A \xrightarrow {f} B \xrightarrow {g} C$ in $\mathbf {C}$ , the equation $F (g \circ f) = F(g) \circ F(f)$ holds in $\mathbf {D}$ .

$\pi _0 \circ \langle f , g \rangle = f$
$\pi _1 \circ \langle f , g \rangle = g$
$\langle \pi _0 \circ h , \pi _1 \circ h \rangle = h$