Proposition enriched_yoneda_enrichment_data_eq (y₁ y₂ : C) : enriched_yoneda_enrichment_data_ob y₁ y₂ · @enriched_functor_left_map V (C^opp) _ _ _ _ PV' (enriched_repr_presheaf_functor y₁) _ (enriched_repr_presheaf_enrichment y₂) = enriched_yoneda_enrichment_data_ob y₁ y₂ · enriched_functor_right_map _ _ _ _ (enriched_repr_presheaf_enrichment y₁). Proof. use ProductArrow_eq. intros x. unfold enriched_functor_left_map, enriched_functor_right_map. rewrite !assoc'. refine (maponpaths (λ z, _ · z) (ProductPrCommutes (C × C) V _ _ _ _ _) @ _). refine (_ @ !(maponpaths (λ z, _ · z) (ProductPrCommutes (C × C) V _ _ _ _ _))). rewrite !assoc. cbn. refine (maponpaths (λ z, z · _) (ProductPrCommutes C V _ _ _ _ _) @ _). refine (_ @ !(maponpaths (λ z, z · _) (ProductPrCommutes C V _ _ _ _ _))). use internal_funext. intros a h. rewrite !tensor_comp_r_id_r. unfold enriched_functor_left_map_ob, enriched_functor_right_map_ob. rewrite !assoc'. rewrite !internal_beta. cbn -[sym_mon_braiding]. use internal_funext. intros a' h'. rewrite !tensor_comp_r_id_r. rewrite !assoc'. unfold internal_comp. rewrite !internal_beta. rewrite !assoc'. etrans. { do 2 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'. rewrite internal_beta. apply idpath. } etrans. { rewrite !assoc. rewrite <- tensor_comp_mor. rewrite tensor_sym_mon_braiding. rewrite tensor_comp_mor. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. rewrite <- tensor_comp_mor. rewrite id_right. rewrite internal_beta. apply idpath. } refine (!_). etrans. { apply maponpaths. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_id_l. rewrite internal_beta. apply idpath. } etrans. { rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_right. rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. apply idpath. } rewrite !tensor_comp_id_l. rewrite !assoc'. rewrite enrichment_assoc'. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite tensor_sym_mon_braiding. refine (!_). etrans. { do 3 apply maponpaths. apply tensor_split. } rewrite !assoc. apply maponpaths_2. etrans. { rewrite tensor_split'. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_id_id. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite tensor_sym_mon_braiding. rewrite !assoc'. apply maponpaths. rewrite <- tensor_comp_mor. rewrite id_left, id_right. apply idpath. } refine (!_). etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_id_l. rewrite tensor_sym_mon_braiding. rewrite tensor_comp_id_l. rewrite !assoc'. apply maponpaths. rewrite tensor_rassociator. apply idpath. } rewrite !assoc. apply maponpaths_2. rewrite !assoc'. refine (_ @ id_right _). rewrite <- mon_lassociator_rassociator. rewrite !assoc. apply maponpaths_2. refine (!_). rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. apply sym_mon_hexagon_lassociator. } rewrite !assoc. rewrite <- tensor_comp_id_r. rewrite sym_mon_braiding_inv. rewrite tensor_id_id. rewrite id_left. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory. 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.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Import MonoidalNotations.