{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {motive : CategoryTheory.Pseudofunctor B C → Sort u} →
          (t : CategoryTheory.Pseudofunctor B C) →
            ((toPrelaxFunctor : CategoryTheory.PrelaxFunctor B C) →
                (mapId :
                    (a : B) →
                      toPrelaxFunctor.map (CategoryTheory.CategoryStruct.id a) ≅
                        CategoryTheory.CategoryStruct.id (toPrelaxFunctor.obj a)) →
                  (mapComp :
                      {a b c : B} →
                        (f : a ⟶ b) →
                          (g : b ⟶ c) →
                            toPrelaxFunctor.map (CategoryTheory.CategoryStruct.comp f g) ≅
                              CategoryTheory.CategoryStruct.comp (toPrelaxFunctor.map f) (toPrelaxFunctor.map g)) →
                    (map₂_whisker_left :
                        ∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
                          toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
                            CategoryTheory.CategoryStruct.comp (mapComp f g).hom
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f) (toPrelaxFunctor.map₂ η))
                                (mapComp f h).inv)) →
                      (map₂_whisker_right :
                          ∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
                            toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerRight η h) =
                              CategoryTheory.CategoryStruct.comp (mapComp f h).hom
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.whiskerRight (toPrelaxFunctor.map₂ η)
                                    (toPrelaxFunctor.map h))
                                  (mapComp g h).inv)) →
                        (map₂_associator :
                            ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
                              toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.associator f g h).hom =
                                CategoryTheory.CategoryStruct.comp
                                  (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (toPrelaxFunctor.map h))
                                    (CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.Bicategory.associator (toPrelaxFunctor.map f)
                                          (toPrelaxFunctor.map g) (toPrelaxFunctor.map h)).hom
                                      (CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f)
                                          (mapComp g h).inv)
                                        (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv)))) →
                          (map₂_left_unitor :
                              ∀ {a b : B} (f : a ⟶ b),
                                toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
                                  CategoryTheory.CategoryStruct.comp
                                    (mapComp (CategoryTheory.CategoryStruct.id a) f).hom
                                    (CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.Bicategory.whiskerRight (mapId a).hom (toPrelaxFunctor.map f))
                                      (CategoryTheory.Bicategory.leftUnitor (toPrelaxFunctor.map f)).hom)) →
                            (map₂_right_unitor :
                                ∀ {a b : B} (f : a ⟶ b),
                                  toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
                                    CategoryTheory.CategoryStruct.comp
                                      (mapComp f (CategoryTheory.CategoryStruct.id b)).hom
                                      (CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f) (mapId b).hom)
                                        (CategoryTheory.Bicategory.rightUnitor (toPrelaxFunctor.map f)).hom)) →
                              motive
                                { toPrelaxFunctor := toPrelaxFunctor, mapId := mapId, mapComp := mapComp,
                                  map₂_whisker_left := map₂_whisker_left, map₂_whisker_right := map₂_whisker_right,
                                  map₂_associator := map₂_associator, map₂_left_unitor := map₂_left_unitor,
                                  map₂_right_unitor := map₂_right_unitor }) →
              motive t