Proposition enriched_functor_hom_comp_laws (x y : C₁) : enriched_functor_hom_comp_data x · enriched_functor_left_map_ob EH x y = enriched_functor_hom_comp_data y · enriched_functor_right_map_ob EF x y. Proof. unfold enriched_functor_hom_comp_data. 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. etrans. { etrans. { apply maponpaths. rewrite !assoc. rewrite tensor_sym_mon_braiding. apply idpath. } rewrite !assoc. rewrite tensor_sym_mon_braiding. rewrite !assoc'. do 2 apply maponpaths. rewrite !assoc. rewrite <- tensor_split. rewrite tensor_split'. rewrite !assoc'. rewrite enrichment_assoc'. rewrite !assoc. rewrite <- tensor_id_id. rewrite tensor_rassociator. apply idpath. } etrans. { etrans. { apply maponpaths. rewrite !assoc. rewrite tensor_rassociator. apply idpath. } rewrite !assoc. do 4 apply maponpaths_2. refine (!(id_left _) @ _). rewrite <- mon_lassociator_rassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. apply sym_mon_hexagon_rassociator. } etrans. { rewrite !assoc'. do 3 apply maponpaths. rewrite !assoc. rewrite <- !tensor_comp_mor. rewrite !id_left. rewrite !id_right. do 2 apply maponpaths_2. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_right. rewrite tensor_comp_r_id_l. apply idpath. } rewrite !assoc. rewrite <- tensor_sym_mon_braiding. rewrite !assoc'. apply maponpaths. exact (enriched_functor_hom_eq' EG EH x y). } etrans. { do 3 apply maponpaths. rewrite !assoc. rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite enrichment_assoc. rewrite !assoc. do 2 apply maponpaths_2. rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite tensor_lassociator. rewrite !assoc. rewrite tensor_lassociator. apply idpath. } etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite mon_rassociator_lassociator. apply idpath. } etrans. { apply maponpaths. rewrite !assoc. rewrite id_right. rewrite <- tensor_comp_id_l. rewrite <- !tensor_comp_mor. rewrite id_left, id_right. apply maponpaths_2. apply maponpaths. rewrite tensor_split'. rewrite !assoc. rewrite <- tensor_sym_mon_braiding. rewrite !assoc'. apply maponpaths. rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)). rewrite <- tensor_split. exact (enriched_functor_hom_eq' EF EG x y). } etrans. { apply maponpaths. rewrite !assoc. rewrite tensor_comp_l_id_r. rewrite !assoc'. rewrite enrichment_assoc'. apply idpath. } rewrite !assoc. apply maponpaths_2. etrans. { apply maponpaths_2. rewrite <- !tensor_comp_mor. rewrite id_left. rewrite <- tensor_lassociator. rewrite !assoc'. rewrite mon_lassociator_rassociator. rewrite id_right. apply idpath. } rewrite !assoc'. rewrite <- tensor_split'. rewrite <- !tensor_comp_mor. rewrite id_right. 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.whiskering. 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. Section EnrichmentFromArr. End EnrichmentFromArr.