Homotopy Type Theory
product precategory


For precategories AA and BB, their product A×BA \times B is a precategory 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}((a,b),(a',b'))\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 ((gf),(g'f'))


Lemma 9.5.3

For precategories 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

Proof. 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.

Conversly, 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. \square

See also

Category theory



functor precategory


HoTT book

category: category theory

Created on September 6, 2018 at 14:36:43. See the history of this page for a list of all contributions to it.