proposition: Proposition presheaf_enrichment_to_arr_laws : is_nat_trans F G presheaf_enrichment_to_arr_data.
proof: Proof. intros x y f ; cbn. unfold internal_to_arr. rewrite !assoc. rewrite tensor_linvunitor. rewrite !assoc'. apply maponpaths. refine (!_). etrans. { rewrite tensor_comp_id_r. rewrite !assoc'. apply maponpaths. rewrite !assoc. exact (presheaf_enrichment_naturality F G f). } rewrite !assoc. apply maponpaths_2. refine (!_). etrans. { rewrite <- tensor_split. rewrite tensor_split'. apply idpath. } rewrite <- !tensor_comp_id_r. rewrite !assoc. 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