Proposition enriched_functor_category_enrichment_laws : enrichment_laws enriched_functor_category_enrichment_data. 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.
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.