Proposition enriched_repr_presheaf_enrichment_laws : is_functor_enrichment enriched_repr_presheaf_enrichment_data. Proof. repeat split. - intro x ; cbn -[sym_mon_braiding]. use internal_funext. intros a h. rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite internal_beta. refine (!_). etrans. { apply maponpaths_2. apply tensor_split. } rewrite !assoc'. unfold internal_id. rewrite internal_beta. refine (!_). rewrite !assoc. rewrite tensor_sym_mon_braiding. rewrite tensor_split'. rewrite !assoc'. rewrite <- enrichment_id_right. rewrite !assoc. rewrite <- tensor_sym_mon_braiding. rewrite !assoc'. apply maponpaths. apply sym_mon_braiding_runitor. - intros x₁ x₂ x₃ ; 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. rewrite tensor_lassociator. rewrite !assoc'. refine (!_). etrans. { apply maponpaths. rewrite !assoc. etrans. { apply maponpaths_2. rewrite <- tensor_comp_mor. rewrite id_right. apply maponpaths. rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. apply idpath. } rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. apply idpath. } etrans. { apply maponpaths. rewrite !assoc. rewrite tensor_sym_mon_braiding. rewrite !tensor_comp_id_r. rewrite !assoc'. apply idpath. } rewrite enrichment_assoc. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite tensor_sym_mon_braiding. rewrite !assoc. apply maponpaths_2. rewrite sym_mon_tensor_lassociator. rewrite !assoc. rewrite mon_lassociator_rassociator. rewrite id_left. rewrite !assoc'. refine (!_). etrans. { rewrite tensor_split'. apply idpath. } rewrite !assoc'. apply maponpaths. refine (!_). etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite <- tensor_rassociator. apply idpath. } etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_id_l. rewrite <- tensor_sym_mon_braiding. rewrite tensor_comp_id_l. apply idpath. } rewrite !assoc. rewrite <- tensor_lassociator. rewrite tensor_id_id. rewrite !assoc'. apply maponpaths. etrans. { apply maponpaths. rewrite !assoc. rewrite <- sym_mon_hexagon_rassociator. rewrite !assoc'. rewrite mon_rassociator_lassociator. rewrite id_right. apply idpath. } rewrite !assoc. rewrite mon_lassociator_rassociator. apply id_left. - intros x₁ x₂ f ; cbn -[sym_mon_braiding]. use internal_funext. intros a h. rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite internal_beta. rewrite tensor_split. rewrite !assoc'. unfold internal_from_arr. rewrite internal_beta. unfold precomp_arr. rewrite !assoc. apply maponpaths_2. refine (!_). rewrite tensor_split. rewrite !assoc'. rewrite tensor_sym_mon_braiding. apply maponpaths. rewrite !assoc. apply maponpaths_2. refine (!(id_right _) @ _). rewrite <- mon_runitor_rinvunitor. rewrite !assoc. apply maponpaths_2. apply sym_mon_braiding_runitor. 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.