(** * Functor category *) (** Since there are only notations in [FunctorCategory.Notations], we can just export those. *)(** ** Definition *) Require FunctorCategory.Core. (** ** Morphisms in a functor category *) Require FunctorCategory.Morphisms. (** ** Functoriality of [(_ â _)] *) Require FunctorCategory.Functorial. (** ** Opposite functor [(C â D) â (Cá”á” â Dá”á”)á”á”] *) Require FunctorCategory.Dual. Include FunctorCategory.Core. Include FunctorCategory.Morphisms. Include FunctorCategory.Functorial. Include FunctorCategory.Dual. (** We don't want to make UTF-8 notations the default, so we don't export them. *)