Definition op2_mnd_mor_to_comnd_mor (f : m₁ --> m₂) : comnd_mor (op2_mnd_to_comnd m₁) (op2_mnd_to_comnd m₂). Proof. use make_comnd_mor. - use make_comnd_mor_data. + exact (mor_of_mnd_mor f). + exact (mnd_mor_endo f). - split. + abstract (unfold comnd_mor_counit_law ; cbn ; rewrite !vassocl ; exact (mnd_mor_unit f)). + abstract (unfold comnd_mor_comult_law ; cbn ; rewrite !vassocl ; exact (mnd_mor_mu 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.