{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (obj : B → C) →
          (map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)) →
            (map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (map f))
                  CategoryTheory.PrelaxFunctor.map₂_id._autoParam →
                autoParam
                    (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
                      map₂ (CategoryTheory.CategoryStruct.comp η θ) =
                        CategoryTheory.CategoryStruct.comp (map₂ η) (map₂ θ))
                    CategoryTheory.PrelaxFunctor.map₂_comp._autoParam →
                  (mapId :
                      (a : B) → map (CategoryTheory.CategoryStruct.id a) ⟶ CategoryTheory.CategoryStruct.id (obj a)) →
                    (mapComp :
                        {a b c : B} →
                          (f : a ⟶ b) →
                            (g : b ⟶ c) →
                              map (CategoryTheory.CategoryStruct.comp f g) ⟶
                                CategoryTheory.CategoryStruct.comp (map f) (map g)) →
                      autoParam
                          (∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
                            CategoryTheory.CategoryStruct.comp (map₂ (CategoryTheory.Bicategory.whiskerRight η g))
                                (mapComp f' g) =
                              CategoryTheory.CategoryStruct.comp (mapComp f g)
                                (CategoryTheory.Bicategory.whiskerRight (map₂ η) (map g)))
                          CategoryTheory.OplaxFunctor.mapComp_naturality_left._autoParam →
                        autoParam
                            (∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
                              CategoryTheory.CategoryStruct.comp (map₂ (CategoryTheory.Bicategory.whiskerLeft f η))
                                  (mapComp f g') =
                                CategoryTheory.CategoryStruct.comp (mapComp f g)
                                  (CategoryTheory.Bicategory.whiskerLeft (map f) (map₂ η)))
                            CategoryTheory.OplaxFunctor.mapComp_naturality_right._autoParam →
                          autoParam
                              (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
                                CategoryTheory.CategoryStruct.comp
                                    (map₂ (CategoryTheory.Bicategory.associator f g h).hom)
                                    (CategoryTheory.CategoryStruct.comp
                                      (mapComp f (CategoryTheory.CategoryStruct.comp g h))
                                      (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) =
                                  CategoryTheory.CategoryStruct.comp
                                    (mapComp (CategoryTheory.CategoryStruct.comp f g) h)
                                    (CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h))
                                      (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom))
                              CategoryTheory.OplaxFunctor.map₂_associator._autoParam →
                            autoParam
                                (∀ {a b : B} (f : a ⟶ b),
                                  map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
                                    CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id a) f)
                                      (CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.Bicategory.whiskerRight (mapId a) (map f))
                                        (CategoryTheory.Bicategory.leftUnitor (map f)).hom))
                                CategoryTheory.OplaxFunctor.map₂_leftUnitor._autoParam →
                              autoParam
                                  (∀ {a b : B} (f : a ⟶ b),
                                    map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
                                      CategoryTheory.CategoryStruct.comp
                                        (mapComp f (CategoryTheory.CategoryStruct.id b))
                                        (CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b))
                                          (CategoryTheory.Bicategory.rightUnitor (map f)).hom))
                                  CategoryTheory.OplaxFunctor.map₂_rightUnitor._autoParam →
                                CategoryTheory.OplaxFunctor B C