product category in nLab
For CC and DD two categories, the product category C×DC \times D is the category whose
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.
For categories AA and BB, their product A×BA \times B is a category with (A×B) 0≡A 0×B 0(A\times B)_0\equiv A_0 \times B_0 and
hom A×B((a,b),(a′,b′))≡hom A(a,a′)×hom B(b,b′)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)≡(1 a,1 b)1_{(a,b)}\equiv (1_a,1_b) and composition by
Proof
Given F:A×B→CF : A \times B \to C, for any a:Aa:A we obviously have a functor F a:B→CF_a : B \to C. This gives a function A 0→(C B) 0A_0 \to (C^B)_0. Next, for any f:hom A(a,a′)f: hom_A(a,a'), we have for any b:Bb:B the morphisms F (a,b),(a′,b′)(f,1 b):F a(b)→F a′(b)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→F a′F_a \to F_{a'}. Functoriality in aa is easy to check, so we have a functor F^:A→C B\hat{F} : A \to C^B.
Conversely, suppose given G:A→C BG:A \to C^B. Then for any a:Aa:A and b:Bb:B we have the object G(a)(b):CG(a)(b):C, giving a function A 0×B 0→C 0A_0 \times B_0 \to C_0. And for f:hom A(a,a′)f:hom_A(a,a') and g:hom B(b,b′)g : hom_B(b,b'), we have the morphism
G(a′) b,b′(g)∘G a,a′(f) b=G a,a′(f) b′∘G(a) b,b′(g)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′))hom_C(G(a)(b),G(a')(b')). Functoriality is again easy to check, so we have a functor vG:A×B→C.\v{G} : A \times B \to C. Finally, it is also clear that these operations are inverses.