Definition comnd_mor_to_op2_mnd_mor (f : comnd_mor (op2_mnd_to_comnd m₁) (op2_mnd_to_comnd m₂)) : m₁ --> m₂. Proof. use make_mnd_mor. - use make_mnd_mor_data. + exact f. + exact (comnd_mor_endo f). - split. + abstract (cbn ; rewrite !vassocr ; exact (comnd_mor_counit f)). + abstract (cbn ; rewrite !vassocr ; exact (comnd_mor_comult f)). 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.