(** * Functors involving product categories, and their properties *)
(** ** Definitions of various functors *)
Require Functor.Prod.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
(** ** Universal property *)
Require Functor.Prod.Universal.
(** ** Functoriality *)
Require Functor.Prod.Functorial.

Include Functor.Prod.Core.
Include Functor.Prod.Universal.
Include Functor.Prod.Functorial.

Module Export FunctorProdNotations.
  Include Functor.Prod.Core.FunctorProdCoreNotations.
End FunctorProdNotations.