Definition enriched_whiskered_bifunctor_data {V : monoidal_cat} {C₁ C₂ C₃ : category} (E₁ : enrichment C₁ V) (E₂ : enrichment C₂ V) (E₃ : enrichment C₃ V) : UU := ∑ (F : C₁ → C₂ → C₃), (∏ (x₁ x₂ : C₁) (y : C₂), E₁ ⦃ x₁ , x₂ ⦄ --> E₃ ⦃ F x₁ y , F x₂ y ⦄) × (∏ (x : C₁) (y₁ y₂ : C₂), E₂ ⦃ y₁ , y₂ ⦄ --> E₃ ⦃ F x y₁ , F x y₂ ⦄).
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.EnrichedCats.Examples.Tensor. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.CurriedBifunctors. 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. Section FromWhiskeredBifunctor. End FromWhiskeredBifunctor.