Proposition yoneda_inv_left : yoneda_inv · enriched_yoneda_enrichment E EqV PV PV' x y = identity _. Proof. cbn. use EqualizerInsEq. rewrite !assoc'. rewrite EqualizerCommutes. rewrite id_left. refine (_ @ id_right _). use ProductArrow_eq. intro z. rewrite !assoc'. rewrite id_left. etrans. { do 5 apply maponpaths. exact (ProductPrCommutes C V _ _ _ _ _). } use internal_funext. intros a h. rewrite !tensor_comp_r_id_r. rewrite !assoc'. rewrite internal_beta. pose (EqualizerEqAr (enriched_functor_hom (op_enrichment V E) (self_enrichment V) EqV PV PV' (enriched_repr_presheaf_enrichment E x) (enriched_repr_presheaf_enrichment E y))) as p₁. cbn in p₁. unfold enriched_functor_left_map, enriched_functor_right_map in p₁. unfold enriched_functor_left_map_ob, enriched_functor_right_map_ob in p₁. pose (maponpaths (λ f, f · ProductPr (C ^opp × C ^opp) V _ (x ,, z)) p₁ : _ = _) as p₂. rewrite !assoc' in p₂. pose (!(maponpaths (λ z, _ · z) (ProductPrCommutes (C^opp × C^opp) V _ _ _ _ _)) @ p₂ @ maponpaths (λ z, _ · z) (ProductPrCommutes (C^opp × C^opp) V _ _ _ _ _)) as p₃. cbn -[sym_mon_braiding] in p₃. pose (maponpaths (λ z, z #⊗ h · internal_eval _ _) p₃) as p. cbn -[sym_mon_braiding] in p. refine (_ @ maponpaths (λ f, f · mon_rinvunitor _ · (identity _ #⊗ enriched_id E x) · internal_eval _ _) p @ _). - rewrite !tensor_comp_r_id_r. rewrite !assoc'. do 2 apply maponpaths. rewrite !assoc. rewrite internal_beta. refine (!_). etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite tensor_rinvunitor. rewrite tensor_comp_id_r. rewrite !assoc'. apply maponpaths. etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. rewrite !assoc'. unfold internal_comp. rewrite internal_beta. rewrite !assoc'. apply idpath. } rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. rewrite !assoc'. 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. } rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite tensor_sym_mon_braiding. rewrite !assoc. apply maponpaths_2. rewrite <- tensor_id_id. rewrite !assoc'. etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. rewrite tensor_sym_mon_braiding. apply idpath. } rewrite !assoc. apply maponpaths_2. rewrite <- mon_rinvunitor_triangle. rewrite !assoc. rewrite <- tensor_sym_mon_braiding. rewrite !assoc'. refine (_ @ id_right _). apply maponpaths. etrans. { apply maponpaths. rewrite !assoc. rewrite mon_rassociator_lassociator. apply id_left. } apply sym_mon_braiding_inv. - rewrite !tensor_comp_r_id_r. rewrite !assoc'. do 2 apply maponpaths. rewrite !assoc. rewrite internal_beta. rewrite tensor_rinvunitor. rewrite !assoc'. etrans. { apply maponpaths. rewrite tensor_comp_id_r. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. rewrite !assoc'. unfold internal_comp. rewrite internal_beta. rewrite <- tensor_id_id. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply idpath. } rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_id_l. etrans. { do 2 apply maponpaths_2. apply maponpaths. rewrite <- tensor_split'. rewrite tensor_split. apply idpath. } rewrite tensor_comp_id_l. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_id_l. rewrite internal_beta. apply idpath. } refine (_ @ id_left _). rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite <- tensor_comp_id_l. etrans. { do 3 apply maponpaths. rewrite !assoc. rewrite tensor_sym_mon_braiding. rewrite !assoc'. rewrite <- enrichment_id_left. apply idpath. } rewrite sym_mon_braiding_lunitor. rewrite <- mon_runitor_triangle. refine (_ @ mon_rinvunitor_runitor _). apply maponpaths. rewrite !assoc. rewrite mon_lassociator_rassociator. apply id_left. 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.EnrichedCats.Examples.Yoneda. 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.