{B : Type u₁} →
  {inst : CategoryTheory.Bicategory B} →
    {C : Type u₂} →
      {inst_1 : CategoryTheory.Bicategory C} →
        {F : CategoryTheory.LaxFunctor B C} →
          {P : Sort u} →
            {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} →
                    {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} →
                            { mapIdIso := mapIdIso, mapCompIso := mapCompIso, mapIdIso_inv := mapIdIso_inv,
                                  mapCompIso_inv := mapCompIso_inv } =
                                { mapIdIso := mapIdIso', mapCompIso := mapCompIso', mapIdIso_inv := mapIdIso_inv',
                                  mapCompIso_inv := mapCompIso_inv' } →
                              (mapIdIso ≍ mapIdIso' → mapCompIso ≍ mapCompIso' → P) → P