Library HoTT.Categories.Functor.Pointwise

Pointwise functors (functoriality of the functor category construction)