∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F : CategoryTheory.LaxFunctor B C} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (mapIdIso : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a))
  (mapCompIso :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g))
  (mapIdIso_inv :
    autoParam (∀ {a : B}, (mapIdIso a).inv = F.mapId a) CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv._autoParam)
  (mapCompIso_inv :
    autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso f g).inv = F.mapComp f g)
      CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv._autoParam),
  sizeOf
      { mapIdIso := mapIdIso, mapCompIso := mapCompIso, mapIdIso_inv := mapIdIso_inv,
        mapCompIso_inv := mapCompIso_inv } =
    1