Definition mnd_to_adjunction_to_mnd_law₂ : lassociator (id₁ _) f f • ((lunitor f • cell_of_mnd_cell ((em_ump_1_inv2cell m He free_alg_1cell_cone) ^-1) • rinvunitor (em_ump_1_mor m He free_alg_1cell_cone · pr1 (mor_of_em_cone m e))) ▹ endo_of_mnd m) • rassociator (free_alg_1cell · l) (id₁ x) f • (free_alg_1cell · l ◃ (lunitor f • cell_of_mnd_cell ((em_ump_1_inv2cell m He free_alg_1cell_cone) ^-1) • rinvunitor (em_ump_1_mor m He free_alg_1cell_cone · pr1 (mor_of_em_cone m e)))) • lassociator (free_alg_1cell · l) (free_alg_1cell · l) (id₁ x) • ((((rassociator free_alg_1cell l (free_alg_1cell · l) • (free_alg_1cell ◃ lassociator l free_alg_1cell l)) • (free_alg_1cell ◃ (mnd_to_counit ▹ l))) • (free_alg_1cell ◃ lunitor l)) ▹ id₁ x) = (id₁ x ◃ μ) • ((lunitor f • cell_of_mnd_cell ((em_ump_1_inv2cell m He free_alg_1cell_cone) ^-1)) • rinvunitor (em_ump_1_mor m He free_alg_1cell_cone · pr1 (mor_of_em_cone m e))).
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.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Limits.EilenbergMooreObjects. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.Monads.Examples.AdjunctionToMonad. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion.