proposition: Proposition enriched_functor_category_enrichment_laws : enrichment_laws enriched_functor_category_enrichment_data.
proof: Proof. repeat split. - intros F G. use mor_to_enriched_functor_unique. intro x ; cbn. rewrite !assoc'. refine (!_). etrans. { apply maponpaths. apply enriched_functor_hom_comp_comm. } rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_left. etrans. { do 2 apply maponpaths_2. apply enriched_functor_hom_id_comm. } rewrite tensor_split. rewrite !assoc'. rewrite <- tensor_lunitor. apply maponpaths. refine (!_). apply enrichment_id_left. - intros F G. use mor_to_enriched_functor_unique. intro x ; cbn. rewrite !assoc'. refine (!_). etrans. { apply maponpaths. apply enriched_functor_hom_comp_comm. } rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_left. etrans. { apply maponpaths_2. apply maponpaths. apply enriched_functor_hom_id_comm. } rewrite tensor_split'. rewrite !assoc'. rewrite <- tensor_runitor. apply maponpaths. refine (!_). apply enrichment_id_right. - intros F₁ F₂ F₃ F₄. use mor_to_enriched_functor_unique. intro x ; cbn. rewrite !assoc'. etrans. { apply maponpaths. apply enriched_functor_hom_comp_comm. } rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_left. etrans. { do 2 apply maponpaths_2. apply enriched_functor_hom_comp_comm. } rewrite tensor_comp_r_id_l. rewrite !assoc'. etrans. { apply maponpaths. rewrite tensor_split. rewrite !assoc'. apply maponpaths. apply enrichment_assoc. } rewrite !assoc. rewrite <- !tensor_comp_mor. rewrite id_left, id_right. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. refine (!_). etrans. { apply maponpaths. apply enriched_functor_hom_comp_comm. } rewrite !assoc. apply maponpaths_2. rewrite <- tensor_comp_mor. rewrite id_left. etrans. { apply maponpaths. apply enriched_functor_hom_comp_comm. } rewrite !tensor_comp_l_id_r. apply idpath. - intros F G τ. use subtypePath. { intro. apply isaprop_nat_trans_enrichment. } use nat_trans_eq ; [ apply homset_property | ]. intro x ; cbn. unfold enrichment_functor_hom_to_arr_data. etrans. { apply maponpaths. apply enriched_functor_hom_from_arr_comm. } apply enriched_to_from_arr. - intros F G τ. use mor_to_enriched_functor_unique. intro x ; cbn. etrans. { apply enriched_functor_hom_from_arr_comm. } cbn. apply enriched_from_to_arr. - intros F. use subtypePath. { intro. apply isaprop_nat_trans_enrichment. } use nat_trans_eq ; [ apply homset_property | ]. intro x ; cbn. unfold enrichment_functor_hom_to_arr_data. etrans. { apply maponpaths. apply enriched_functor_hom_id_comm. } apply enriched_to_arr_id. - intros F G H τ θ. use subtypePath. { intro. apply isaprop_nat_trans_enrichment. } use nat_trans_eq ; [ apply homset_property | ]. intro x ; cbn. unfold enrichment_functor_hom_to_arr_data. refine (!_). etrans. { rewrite !assoc'. apply maponpaths. etrans. { do 2 apply maponpaths. apply enriched_functor_hom_comp_comm. } rewrite !assoc. apply maponpaths_2. rewrite !assoc'. apply maponpaths. rewrite <- tensor_comp_mor. rewrite !enriched_functor_hom_from_arr_comm. apply idpath. } refine (!_). apply enriched_to_arr_comp. 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