∀ {B : Type u_3} [inst : CategoryTheory.Bicategory B] {B' : Type u_5} [inst_1 : CategoryTheory.Bicategory B']
  [CategoryTheory.Bicategory.IsLocallyGroupoid B] (F : CategoryTheory.LaxFunctor B' B) {a b c : B'} (f : a ⟶ b)
  (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)