proposition: Proposition is_functor_enriched_precomp : is_functor enriched_precomp_data.
proof: Proof. split. - intros G. use subtypePath ; [ intro ; apply isaprop_nat_trans_enrichment | ]. use nat_trans_eq ; [ apply homset_property | ]. intro x ; cbn. apply idpath. - intros G₁ G₂ G₃ τ₁ τ₂. use subtypePath ; [ intro ; apply isaprop_nat_trans_enrichment | ]. use nat_trans_eq ; [ apply homset_property | ]. intro x ; cbn. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory UniMath.CategoryTheory.Monoidal.Categories