Definition op2_mnd_cell_weq_comnd_cell {B : bicat} {m₁ m₂ : mnd (op2_bicat B)} (f₁ f₂ : m₁ --> m₂) : f₁ ==> f₂ ≃ comnd_cell (op2_mnd_mor_to_comnd_mor f₁) (op2_mnd_mor_to_comnd_mor f₂). Proof. use make_weq. - exact op2_mnd_cell_to_comnd_cell. - use isweq_iso. + exact comnd_cell_to_op2_mnd_cell. + abstract (intro ; use eq_mnd_cell ; apply idpath). + abstract (intro ; use subtypePath ; [ intro ; apply cellset_property | ] ; apply idpath). 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.