Definition enriched_functor_precategory_data (A B : enriched_precat) : precategory_data. Proof. use make_precategory_data. - use make_precategory_ob_mor. + exact (enriched_functor A B). + intros F G. exact (enriched_nat_trans F G). - intros c. apply enriched_nat_trans_identity. - intros a b c f g. exact (enriched_nat_trans_comp f g). Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Core.Isos. Import MonoidalNotations.