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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.HomFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Import MonoidalNotations.