Proposition presheaf_enrichment_to_arr_laws : is_nat_trans F G presheaf_enrichment_to_arr_data. 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.
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.