Definition op2_mnd_mor_weq_comnd_mor {B : bicat} (m₁ m₂ : mnd (op2_bicat B)) : m₁ --> m₂ ≃ comnd_mor (op2_mnd_to_comnd m₁) (op2_mnd_to_comnd m₂). Proof. use make_weq. - exact op2_mnd_mor_to_comnd_mor. - use isweq_iso. + exact comnd_mor_to_op2_mnd_mor. + exact op2_mnd_mor_weq_comnd_mor_inv₁. + exact op2_mnd_mor_weq_comnd_mor_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.