-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory 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)) →
              autoParam
                  (∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
                    CategoryTheory.CategoryStruct.comp
                        (toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) (mapComp f' g) =
                      CategoryTheory.CategoryStruct.comp (mapComp f g)
                        (CategoryTheory.Bicategory.whiskerRight (toPrelaxFunctor.map₂ η) (toPrelaxFunctor.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
                          (toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) (mapComp f g') =
                        CategoryTheory.CategoryStruct.comp (mapComp f g)
                          (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f) (toPrelaxFunctor.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
                            (toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.associator f g h).hom)
                            (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h))
                              (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f) (mapComp g h))) =
                          CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h)
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (toPrelaxFunctor.map h))
                              (CategoryTheory.Bicategory.associator (toPrelaxFunctor.map f) (toPrelaxFunctor.map g)
                                  (toPrelaxFunctor.map h)).hom))
                      CategoryTheory.OplaxFunctor.map₂_associator._autoParam →
                    autoParam
                        (∀ {a b : B} (f : a ⟶ b),
                          toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
                            CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id a) f)
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerRight (mapId a) (toPrelaxFunctor.map f))
                                (CategoryTheory.Bicategory.leftUnitor (toPrelaxFunctor.map f)).hom))
                        CategoryTheory.OplaxFunctor.map₂_leftUnitor._autoParam →
                      autoParam
                          (∀ {a b : B} (f : a ⟶ b),
                            toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
                              CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b))
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f) (mapId b))
                                  (CategoryTheory.Bicategory.rightUnitor (toPrelaxFunctor.map f)).hom))
                          CategoryTheory.OplaxFunctor.map₂_rightUnitor._autoParam →
                        CategoryTheory.OplaxFunctor B C