Definition:Product Functor

From ProofWiki
Jump to navigation Jump to search


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:

Object functor:    \(\ds \times \left({C, D}\right) := C \times D \)      
Morphism functor:    \(\ds \times \left({f, f'}\right) := f \times f' \)      

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.