Definition is_monadic_connecting_functor_fiber : eilenberg_moore_cat M'. Proof. use make_ob_eilenberg_moore. - exact (ob_of_eilenberg_moore_ob z). - cbn. exact (lassociator _ _ _ • mor_of_eilenberg_moore_ob z). - abstract (refine (_ @ eilenberg_moore_ob_unit z) ; cbn ; rewrite !vassocl ; apply idpath). - abstract (cbn ; rewrite <- !rwhisker_vcomp ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite <- rwhisker_rwhisker ; rewrite !vassocl ; pose (eilenberg_moore_ob_mult z) as p ; cbn in p ; rewrite !id2_left, !id2_right in p ; rewrite <- p ; rewrite !vassocr ; apply maponpaths_2 ; rewrite !vassocl ; use vcomp_move_L_pM ; [ is_iso | ] ; cbn ; rewrite <- !lwhisker_vcomp ; rewrite !vassocr ; rewrite rassociator_rassociator ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)) ; rewrite !lwhisker_vcomp ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite lwhisker_lwhisker_rassociator ; rewrite !vassocl ; rewrite rassociator_lassociator ; rewrite id2_right ; use vcomp_move_L_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; rewrite <- rassociator_rassociator ; rewrite !vassocl ; rewrite lwhisker_vcomp ; rewrite !vassocr ; rewrite rassociator_lassociator ; rewrite id2_left ; rewrite <- !rwhisker_vcomp ; rewrite !vassocl ; apply maponpaths ; rewrite <- !lwhisker_vcomp ; rewrite !vassocr ; rewrite rwhisker_lwhisker_rassociator ; rewrite !vassocl ; apply maponpaths ; rewrite lunitor_lwhisker ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.EilenbergMoore. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.CategoryTheory.Monads.Monads. 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.AdjointUnique. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Properties.AdjunctionsRepresentable. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.Monads.Examples.AdjunctionToMonad. Require Import UniMath.Bicategories.Monads.Examples.ToMonadInCat. Require Import UniMath.Bicategories.Monads.Examples.MonadsInBicatOfUnivCats. Require Import UniMath.Bicategories.Limits.EilenbergMooreObjects. Require Import UniMath.Bicategories.Limits.Examples.BicatOfUnivCatsLimits.