∀ {B : Type u_3} [inst : CategoryTheory.Bicategory B] {B' : Type u_5} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B] (F : CategoryTheory.OplaxFunctor B' B) {a : B'},
  (CategoryTheory.asIso (F.mapId a)).hom = F.mapId a