Definition op2_mnd_weq_comnd (B : bicat) : mnd (op2_bicat B) ≃ comnd B. Proof. use make_weq. - exact op2_mnd_to_comnd. - use isweq_iso. + exact comnd_to_op2_mnd. + exact op2_mnd_weq_comnd_inv₁. + exact op2_mnd_weq_comnd_inv₂. 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.