Proposition is_functor_enriched_precomp : is_functor enriched_precomp_data. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory. Require Import UniMath.CategoryTheory.Monoidal.Categories.