proposition: Proposition presheaf_enrichment_naturality (F G : C ⟶ V) {x y : C} (f : x --> y) : (EqualizerArrow (presheaf_enrichment_hom F G) · ProductPr _ _ _ x) #⊗ identity _ · internal_eval (F x) (G x) · # G f = (EqualizerArrow (presheaf_enrichment_hom F G) · ProductPr _ _ _ y) #⊗ identity _ · identity _ #⊗ # F f · internal_eval (F y) (G y).
proof: Proof. refine (_ @ presheaf_enrichment_naturality_help F G f @ _). - refine (!_). etrans. { etrans. { do 2 apply maponpaths_2. unfold presheaf_enrichment_hom_eq_left. rewrite !assoc'. apply maponpaths. exact (ProductPrCommutes (∑ (x y : C), x --> y) V _ _ _ _ (x ,, y ,, f)). } cbn. rewrite !tensor_comp_r_id_r. rewrite !assoc'. unfold internal_comp. rewrite internal_beta. etrans. { do 3 apply maponpaths. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite tensor_id_id. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. rewrite !assoc'. unfold internal_from_arr. rewrite internal_beta. rewrite !assoc. rewrite tensor_lunitor. apply idpath. } do 2 apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. rewrite !assoc'. rewrite mon_lunitor_triangle. rewrite <- tensor_comp_id_r. rewrite mon_linvunitor_lunitor. apply tensor_id_id. } rewrite id_left. rewrite !assoc. rewrite <- tensor_comp_id_r. apply idpath. - etrans. { etrans. { do 2 apply maponpaths_2. unfold presheaf_enrichment_hom_eq_right. rewrite !assoc'. apply maponpaths. exact (ProductPrCommutes (∑ (x y : C), x --> y) V _ _ _ _ (x ,, y ,, f)). } cbn. rewrite !tensor_comp_r_id_r. rewrite !assoc'. unfold internal_comp. rewrite internal_beta. etrans. { do 3 apply maponpaths. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_id_l. unfold internal_from_arr. rewrite internal_beta. rewrite tensor_comp_id_l. apply idpath. } do 2 apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. rewrite !assoc'. rewrite <- mon_triangle. rewrite <- tensor_comp_id_r. rewrite mon_rinvunitor_runitor. apply tensor_id_id. } rewrite id_left. rewrite !assoc. rewrite <- tensor_comp_id_r. apply idpath. 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