Definition lax_monoidal_functor_laws {V₁ V₂ : monoidal_cat} (F : V₁ ⟶ V₂) (μ : ∏ (x y : V₁), F x ⊗ F y --> F(x ⊗ y)) (η : I_{V₂} --> F(I_{V₁})) : UU := (∏ (x₁ x₂ y₁ y₂ : V₁) (f : x₁ --> x₂) (g : y₁ --> y₂), #F f #⊗ #F g · μ x₂ y₂ = μ x₁ y₁ · #F(f #⊗ g)) × (∏ (x : V₁), η #⊗ identity _ · μ (I_{V₁}) x · #F (mon_lunitor x) = mon_lunitor (F x)) × (∏ (x : V₁), identity _ #⊗ η · μ x (I_{V₁}) · #F (mon_runitor x) = mon_runitor (F x)) × (∏ (x y z : V₁), (μ x y #⊗ identity _) · μ (x ⊗ y) z · #F(mon_lassociator x y z) = mon_lassociator (F x) (F y) (F z) · (identity _ #⊗ μ y z) · μ x (y ⊗ z)).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import BifunctorNotations. Import MonoidalNotations.