Definition em_comnd_cone_to_op2_em_cone {B : bicat} {m : mnd (op2_bicat B)} (e : em_comnd_cone m) : em_cone m. Proof. use make_em_cone. - exact e. - exact (mor_of_em_comnd_cone _ e). - exact (lunitor _ • cell_of_em_comnd_cone _ e). - abstract (cbn ; rewrite !vassocr ; use vcomp_move_L_Mp ; [ is_iso | ] ; cbn ; rewrite !vassocl ; apply maponpaths ; exact (!(em_comnd_cone_counit _ e))). - abstract (cbn ; rewrite !vassocl ; apply maponpaths ; refine (_ @ em_comnd_cone_comult _ e) ; rewrite !vassocl ; apply maponpaths ; rewrite !vassocr ; rewrite rwhisker_vcomp ; rewrite !vassocr ; rewrite linvunitor_lunitor ; rewrite id2_left ; apply idpath). Defined.
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.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.CommaObjects. Require Import UniMath.Bicategories.Limits.EilenbergMooreObjects. Require Import UniMath.Bicategories.Limits.EilenbergMooreComonad. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion.