Library HoTT.categories.Functor.Prod

Functors involving product categories, and their properties

Definitions of various functors

Universal property

Functoriality