nLab product category

Definition

For $C$ and $D$ two categories, the product category $C \times D$ is the category whose

• objects are ordered pairs $(c,d)$ with $c$ an object of $C$ and $d$ an object of $D$: $Obj(C \times D) = Obj(C) \times Obj(D)$.

• morphisms are ordered pairs $((c \stackrel{f}{\to} c'),(d \stackrel{g}{\to} d'))$: $Mor(C \times D) = Mor(C) \times Mor(D)$

• composition of morphisms is defined componentwise by composition in $C$ and $D$.

This operation is the cartesian product in the 1-category Cat.

In homotopy type theory

We discuss cartesian products for categories in homotopy type theory.

Note: UFP 2013 calls a category a “precategory” and a univalent category a “category”, but here we shall refer to the standard terminology of “category” and “univalent category” respectively.

Definition

For categories $A$ and $B$, their product $A \times B$ is a category with $(A\times B)_0\equiv A_0 \times B_0$ and

$$hom_{A \times B}\big((a,b),(a',b')\big)\equiv hom_A (a,a')\times hom_B (b,b')$$

Identities are defined by $1_{(a,b)}\equiv (1_a,1_b)$ and composition by

$$(g,g')(f,f') \equiv \big((gf),(g'f')\big)$$

Properties

Lemma

(Lemma 9.5.3 in UFP13)
For categories $A,B,C$, the following types are equivalent:

1. Functors $A \times B \to C$
2. Functors $A \to C^B$

Proof

Given $F : A \times B \to C$, for any $a:A$ we obviously have a functor $F_a : B \to C$. This gives a function $A_0 \to (C^B)_0$. Next, for any $f: hom_A(a,a')$, we have for any $b:B$ the morphisms $F_{(a,b),(a',b')}(f,1_b):F_a(b) \to F_{a'}(b)$.

These are the components of a natural transformation $F_a \to F_{a'}$. Functoriality in $a$ is easy to check, so we have a functor $\hat{F} : A \to C^B$.

Conversely, suppose given $G:A \to C^B$. Then for any $a:A$ and $b:B$ we have the object $G(a)(b):C$, giving a function $A_0 \times B_0 \to C_0$. And for $f:hom_A(a,a')$ and $g : hom_B(b,b')$, we have the morphism

$$G(a')_{b,b'}(g) \circ G_{a,a'}(f)_b= G_{a,a'}(f)_{b'} \circ G(a)_{b,b'}(g)$$

in $hom_C(G(a)(b),G(a')(b'))$. Functoriality is again easy to check, so we have a functor $\v{G} : A \times B \to C.$ Finally, it is also clear that these operations are inverses.

Related concepts

• enriched product category

• bifunctor

• extranatural transformation

• Yoneda lemma

References

Textbook accounts:

• Saunders MacLane, §II.3 of: Categories for the Working Mathematician, Graduate Texts in Mathematics 5 Springer (1971, second ed. 1997) [doi:10.1007/978-1-4757-4721-8]

Discussion in homotopy type theory:

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)