Proposition is_functor_enrichment_enriched_yoneda : is_functor_enrichment enriched_yoneda_enrichment_data. Proof. repeat split. - intros x ; cbn. use EqualizerInsEq. rewrite !assoc'. unfold enriched_functor_hom_id, mor_to_enriched_functor_hom. rewrite !EqualizerCommutes. use ProductArrow_eq. intro y. rewrite !assoc'. cbn. etrans. { apply maponpaths. exact (ProductPrCommutes C V _ _ _ _ _). } refine (_ @ !(ProductPrCommutes C V _ _ _ _ _)). use internal_funext. intros a h. rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite internal_beta. refine (!_). rewrite tensor_split. rewrite !assoc'. unfold internal_id. rewrite internal_beta. rewrite enrichment_id_left. rewrite !assoc. rewrite <- tensor_split. apply idpath. - intros x y z ; cbn. use EqualizerInsEq. rewrite !assoc'. unfold enriched_functor_hom_comp, mor_to_enriched_functor_hom. rewrite !EqualizerCommutes. use ProductArrow_eq. intro w. rewrite !assoc'. etrans. { apply maponpaths. exact (ProductPrCommutes C V _ _ _ _ _). } refine (!_). etrans. { apply maponpaths. exact (ProductPrCommutes C V _ _ _ _ _). } unfold enriched_functor_hom_comp_data, enriched_functor_hom_pr. rewrite !assoc. rewrite <- tensor_comp_mor. rewrite !assoc. rewrite !EqualizerCommutes. etrans. { apply maponpaths_2. etrans. { apply maponpaths. exact (ProductPrCommutes C V _ _ _ _ _). } apply maponpaths_2. exact (ProductPrCommutes C V _ _ _ _ _). } refine (!_). use internal_funext ; cbn. intros a h. rewrite !tensor_comp_r_id_r. rewrite !assoc'. unfold internal_comp. rewrite !internal_beta. refine (!_). 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 maponpaths_2. apply maponpaths. rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. apply idpath. } refine (!_). rewrite tensor_split. rewrite !assoc'. rewrite enrichment_assoc. rewrite !assoc. apply maponpaths_2. rewrite <- tensor_id_id. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite tensor_comp_id_l. apply idpath. - intros x y f ; cbn. use EqualizerInsEq. rewrite !assoc'. unfold enriched_functor_hom_from_arr, mor_to_enriched_functor_hom. rewrite !EqualizerCommutes. use ProductArrow_eq. intro z. rewrite !assoc'. cbn. refine (ProductPrCommutes C V _ _ _ _ _ @ !_). etrans. { apply maponpaths. exact (ProductPrCommutes C V _ _ _ _ _). } use internal_funext. intros a h. rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite internal_beta. refine (!_). rewrite tensor_split. rewrite !assoc'. unfold internal_from_arr. rewrite internal_beta. unfold postcomp_arr. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite mon_lunitor_linvunitor. apply id_left. } rewrite <- tensor_split. 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.