Definition enriched_functor_category (A B : enriched_precat) : category. Proof. use make_category. - use make_precategory. + exact (enriched_functor_precategory_data A B). + repeat split;simpl. * abstract (intros; apply enriched_nat_trans_eq; intro; cbn; rewrite underlying_morphism_compose_swap; rewrite precompose_identity; apply id_right). * abstract (intros; apply enriched_nat_trans_eq; intro; cbn; rewrite postcompose_identity; apply id_right). * abstract (intros; apply enriched_nat_trans_assoc). * abstract (intros; apply pathsinv0; apply enriched_nat_trans_assoc). - intros a b. apply isaset_enriched_nat_trans. 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.