proposition: 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: 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.
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.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