{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.LaxFunctor B C} →
          {motive : F.PseudoCore → 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 : ∀ {a : B}, (mapIdIso a).inv = F.mapId a) →
                    (mapCompIso_inv : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso f g).inv = F.mapComp f g) →
                      motive
                        { mapIdIso := mapIdIso, mapCompIso := mapCompIso, mapIdIso_inv := mapIdIso_inv,
                          mapCompIso_inv := mapCompIso_inv }) →
              (t : F.PseudoCore) → motive t