Definition op2_mnd_to_comnd (m : mnd (op2_bicat B)) : comnd B. Proof. use make_comnd. - use make_comnd_data. + exact (ob_of_mnd m). + exact (endo_of_mnd m). + exact (unit_of_mnd m). + exact (mult_of_mnd m). - repeat split. + abstract (unfold comnd_counit_left_law ; rewrite !vassocl ; exact (mnd_unit_left m)). + abstract (unfold comnd_counit_right_law ; rewrite !vassocl ; exact (mnd_unit_right m)). + abstract (unfold comnd_comult_assoc_law ; rewrite !vassocl ; exact (mnd_mult_assoc m)). 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.