Definition tensor_enriched_precat_data : enriched_precat_data V. Proof. use make_enriched_precat_data. - exact (C₁ × C₂). - exact (λ x y, E₁ ⦃ pr1 x , pr1 y ⦄ ⊗ (E₂ ⦃ pr2 x , pr2 y ⦄)). - exact (λ x, mon_linvunitor _ · (enriched_id E₁ _ #⊗ enriched_id E₂ _)). - exact (λ x y z, inner_swap _ _ _ _ _ · (enriched_comp E₁ _ _ _ #⊗ enriched_comp E₂ _ _ _)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Enriched.Enriched. Require Import UniMath.CategoryTheory.EnrichedCats.Enriched.EnrichmentEquiv. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal. Import MonoidalNotations.