Definition op2_mnd_cell_to_comnd_cell (α : f₁ ==> f₂) : comnd_cell (op2_mnd_mor_to_comnd_mor f₁) (op2_mnd_mor_to_comnd_mor f₂). Proof. use make_comnd_cell. - exact (cell_of_mnd_cell α). - exact (mnd_cell_endo α). 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.