proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.Examples.HomFunctor UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products