Definition comnd_to_op2_mnd (C : comnd B) : mnd (op2_bicat B). Proof. use make_mnd. - use make_mnd_data. + exact (ob_of_comnd C). + exact (endo_of_comnd C). + exact (counit_of_comnd C). + exact (comult_of_comnd C). - repeat split. + abstract (cbn ; rewrite !vassocr ; exact (comnd_counit_left C)). + abstract (cbn ; rewrite !vassocr ; exact (comnd_counit_right C)). + abstract (cbn ; rewrite !vassocr ; exact (comnd_comult_assoc C)). 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.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax.