Definition is_comnd_cell {B : bicat} {C₁ C₂ : comnd B} {f₁ f₂ : comnd_mor C₁ C₂} (α : f₂ ==> f₁) : UU := (_ ◃ α) • comnd_mor_endo f₁ = comnd_mor_endo f₂ • (α ▹ _).
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.