proposition: Proposition presheaf_enrichment_naturality_help (F G : C ⟶ V) {x y : C} (f : x --> y) : (EqualizerArrow (presheaf_enrichment_hom F G) · presheaf_enrichment_hom_eq_left F G · ProductPr _ _ _ (x ,, y ,, f)) #⊗ identity _ · internal_eval _ _ = (EqualizerArrow (presheaf_enrichment_hom F G) · presheaf_enrichment_hom_eq_right F G · ProductPr _ _ _ (x ,, y ,, f)) #⊗ identity _ · internal_eval _ _.
proof: Proof. do 3 apply maponpaths_2. apply EqualizerEqAr. 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.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