nLab product category




For CC and DD two categories, the product category C×DC \times D is the category whose

  • objects are ordered pairs (c,d)(c,d) with cc an object of CC and dd an object of DD: Obj(C×D)=Obj(C)×Obj(D)Obj(C \times D) = Obj(C) \times Obj(D).

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

  • composition of morphisms is defined componentwise by composition in CC and DD.

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.


For categories AA and BB, their product A×BA \times B is a category with (A×B) 0A 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

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



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

  1. Functors A×BCA \times B \to C
  2. Functors AC BA \to C^B


Given F:A×BCF : A \times B \to C, for any a:Aa:A we obviously have a functor F a:BCF_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 aF aF_a \to F_{a'}. Functoriality in aa is easy to check, so we have a functor F^:AC B\hat{F} : A \to C^B.

Conversely, suppose given G:AC 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 0C 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) bG(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×BC.\v{G} : A \times B \to C. Finally, it is also clear that these operations are inverses.


Textbook accounts:

Discussion in homotopy type theory:

Last revised on June 3, 2023 at 08:31:51. See the history of this page for a list of all contributions to it.