Proposition presheaf_enrichment_comp_laws (F G H : C ⟶ V) : presheaf_enrichment_comp_data F G H · presheaf_enrichment_hom_eq_left F H = presheaf_enrichment_comp_data F G H · presheaf_enrichment_hom_eq_right F H. Proof. use ProductArrow_eq. intros xyf. etrans. { rewrite !assoc'. apply maponpaths. exact (ProductPrCommutes (∑ (x y : C), x --> y) V _ _ _ _ _). } cbn. etrans. { rewrite !assoc. unfold presheaf_enrichment_comp_data. do 3 apply maponpaths_2. exact (ProductPrCommutes C V _ _ _ _ _). } refine (!_). etrans. { rewrite !assoc'. apply maponpaths. exact (ProductPrCommutes (∑ (x y : C), x --> y) V _ _ _ _ _). } cbn. etrans. { rewrite !assoc. unfold presheaf_enrichment_comp_data. do 3 apply maponpaths_2. exact (ProductPrCommutes C V _ _ _ _ _). } refine (!_). use internal_funext. intros a h. induction xyf as [ x [ y f ]] ; cbn. rewrite !tensor_comp_r_id_r. rewrite !assoc'. etrans. { do 5 apply maponpaths. apply internal_beta. } etrans. { do 4 apply maponpaths. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite tensor_id_id. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. rewrite !assoc'. unfold internal_from_arr. rewrite internal_beta. rewrite !assoc. rewrite tensor_lunitor. apply idpath. } etrans. { do 3 apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. rewrite !assoc'. rewrite mon_lunitor_triangle. rewrite <- tensor_comp_id_r. rewrite mon_linvunitor_lunitor. apply tensor_id_id. } rewrite id_left. etrans. { do 2 apply maponpaths. rewrite !assoc. apply maponpaths_2. apply internal_beta. } etrans. { rewrite !assoc. do 3 apply maponpaths_2. rewrite !assoc'. rewrite tensor_lassociator. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite tensor_id_id. rewrite <- tensor_comp_mor. rewrite id_right. apply idpath. } refine (!_). etrans. { do 5 apply maponpaths. apply internal_beta. } etrans. { do 4 apply maponpaths. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. apply maponpaths_2. rewrite <- tensor_comp_id_l. unfold internal_from_arr. rewrite internal_beta. rewrite tensor_comp_id_l. apply idpath. } etrans. { do 3 apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. rewrite !assoc'. rewrite <- mon_triangle. rewrite <- tensor_comp_id_r. rewrite mon_rinvunitor_runitor. apply tensor_id_id. } rewrite id_left. etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. rewrite !assoc'. apply maponpaths. apply internal_beta. } etrans. { rewrite !assoc. do 2 apply maponpaths_2. rewrite !assoc'. rewrite <- tensor_id_id. rewrite tensor_lassociator. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite tensor_lassociator. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite tensor_id_id. rewrite <- tensor_comp_mor. rewrite id_right. apply idpath. } rewrite !assoc'. apply maponpaths. refine (!_). etrans. { rewrite tensor_split. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. rewrite !assoc'. apply maponpaths. rewrite !assoc. exact (presheaf_enrichment_naturality G H f). } etrans. { rewrite !assoc. rewrite <- tensor_comp_id_l. rewrite <- tensor_split. rewrite tensor_split'. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_id_l. apply maponpaths_2. apply maponpaths. rewrite tensor_split. rewrite !assoc'. apply maponpaths. rewrite !assoc. exact (presheaf_enrichment_naturality F G f). } rewrite !assoc. apply maponpaths_2. rewrite <- !tensor_split. 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.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.