Definition enriched_functor_eq {A B : enriched_precat} {F G : enriched_functor A B} : (enriched_functor_to_enriched_functor_data F = enriched_functor_to_enriched_functor_data G) -> F = G. Proof. intro H. use total2_paths_b. - assumption. - apply proofirrelevance. apply isapropdirprod. + apply impred_isaprop. intro. apply homset_property. + repeat (apply impred_isaprop;intro). apply homset_property. 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.