Definition mixed_distr_law_laws (τ : mixed_distr_law_data) : UU := ((ε ▹ f) • lunitor f = τ • (f ◃ ε) • runitor f) × ((δ ▹ f) • rassociator e e f • (e ◃ τ) • lassociator e f e • (τ ▹ e) • rassociator f e e = τ • (f ◃ δ)) × ((e ◃ η) • τ = runitor e • linvunitor e • (η ▹ e)) × ((e ◃ μ) • τ = lassociator e f f • (τ ▹ f) • rassociator f e f • (f ◃ τ) • lassociator f f e • (μ ▹ e)).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.Monads.Examples.MonadsInOp2Bicat. Section FromBicatToMixedDistrLaw. End FromBicatToMixedDistrLaw.