fact: 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))).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Limits.EilenbergMooreObjects UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax UniMath.Bicategories.Monads.Examples.AdjunctionToMonad UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion