proposition: Proposition mor_to_enriched_functor_hom_pr {v : V} (fv : ∏ (i : C₁) , v --> E₂ ⦃ F i, G i ⦄) (p : ∏ (x y : C₁), fv x · σ x y = fv y · ρ x y) (i : C₁) : mor_to_enriched_functor_hom fv p · enriched_functor_hom_pr i = fv i.
proof: Proof. unfold mor_to_enriched_functor_hom, enriched_functor_hom_pr. rewrite !assoc. rewrite EqualizerCommutes. apply (ProductPrCommutes _ _ _ P₁). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.Examples.HomFunctor UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products