\begin{definition}[Definition:Product Functor]
Let $\mathbf C$ be a metacategory with binary products.
Let $\mathbf C \times \mathbf C$ be the product category of $\mathbf C$ with itself.
The '''product functor''' on $\mathbf C$ is the functor $\times: \mathbf C \times \mathbf C \to \mathbf C$ defined by:
{{begin-axiom}}
{{axiom|lc= Object functor:
       |m = \times \left({C, D}\right) := C \times D
}}
{{axiom|lc= Morphism functor:
       |m = \times \left({f, f'}\right) := f \times f'
}}
{{end-axiom}}
where $C \times D$ is a binary product of $C$ and $D$, and $f \times f'$ is the product of $f$ and $f'$.
That it is in fact a functor is shown on Product Functor is Functor.
\end{definition}