Definition enriched_whiskered_bifunctor_laws {V : sym_monoidal_cat} {C₁ C₂ C₃ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} {E₃ : enrichment C₃ V} (F : enriched_whiskered_bifunctor_data E₁ E₂ E₃) : UU := (∏ (x : C₁) (y : C₂), enriched_id E₁ x · enriched_whiskered_bifunctor_left F x x y = enriched_id E₃ (F x y)) × (∏ (x : C₁) (y : C₂), enriched_id E₂ y · enriched_whiskered_bifunctor_right F x y y = enriched_id E₃ (F x y)) × (∏ (x₁ x₂ x₃ : C₁) (y : C₂), enriched_comp E₁ x₁ x₂ x₃ · enriched_whiskered_bifunctor_left F x₁ x₃ y = (enriched_whiskered_bifunctor_left F x₂ x₃ y #⊗ enriched_whiskered_bifunctor_left F x₁ x₂ y) · enriched_comp E₃ (F x₁ y) (F x₂ y) (F x₃ y)) × (∏ (x : C₁) (y₁ y₂ y₃ : C₂), enriched_comp E₂ y₁ y₂ y₃ · enriched_whiskered_bifunctor_right F x y₁ y₃ = (enriched_whiskered_bifunctor_right F x y₂ y₃ #⊗ enriched_whiskered_bifunctor_right F x y₁ y₂) · enriched_comp E₃ (F x y₁) (F x y₂) (F x y₃)) × (∏ (x₁ x₂ : C₁) (y₁ y₂ : C₂), enriched_whiskered_bifunctor_left F x₁ x₂ y₂ #⊗ enriched_whiskered_bifunctor_right F x₁ y₁ y₂ · enriched_comp _ _ _ _ = sym_mon_braiding V _ _ · (enriched_whiskered_bifunctor_right F _ _ _ #⊗ enriched_whiskered_bifunctor_left F _ _ _) · enriched_comp _ _ _ _).
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.