## Definition ## For [[precategories]] $A$ and $B$, their **product** $A \times B$ is a precategory with $(A\times B)_0\equiv A_0 \times B_0$ and $$hom_{A \times B}((a,b),(a',b'))\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 ((gf),(g'f'))$$ ## Properties ## ### Lemma 9.5.3 ### For [[precategories]] $A,B,C$, the following types are [[equivalent]]: 1. Functors $A \times B \to C$ 1. 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$. Conversly, 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. $\square$ ## See also ## [[Category theory]] [[precategory]] [[functor]] [[functor precategory]] ## References ## [[HoTT book]] category: category theory