-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctorCore.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : SizeOf B] [inst_3 : SizeOf C] (obj : B → C) (map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y))
  (map_id :
    autoParam (∀ (X : B), map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj X))
      CategoryTheory.StrictlyUnitaryLaxFunctorCore.map_id._autoParam)
  (map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g))
  (map₂_id :
    autoParam
      (∀ {a b : B} (f : a ⟶ b), map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (map f))
      CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_id._autoParam)
  (map₂_comp :
    autoParam
      (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
        map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (map₂ η) (map₂ θ))
      CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_comp._autoParam)
  (mapComp :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) → CategoryTheory.CategoryStruct.comp (map f) (map g) ⟶ map (CategoryTheory.CategoryStruct.comp f g))
  (mapComp_naturality_left :
    autoParam
      (∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
        CategoryTheory.CategoryStruct.comp (mapComp f g) (map₂ (CategoryTheory.Bicategory.whiskerRight η g)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (map₂ η) (map g)) (mapComp f' g))
      CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapComp_naturality_left._autoParam)
  (mapComp_naturality_right :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
        CategoryTheory.CategoryStruct.comp (mapComp f g) (map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (map₂ η)) (mapComp f g'))
      CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapComp_naturality_right._autoParam)
  (map₂_leftUnitor :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        map₂ (CategoryTheory.Bicategory.leftUnitor f).inv =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (map f)).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
              (mapComp (CategoryTheory.CategoryStruct.id a) f)))
      CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_leftUnitor._autoParam)
  (map₂_rightUnitor :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        map₂ (CategoryTheory.Bicategory.rightUnitor f).inv =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (map f)).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
              (mapComp f (CategoryTheory.CategoryStruct.id b))))
      CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_rightUnitor._autoParam)
  (map₂_associator :
    autoParam
      (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h))
            (CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h)
              (map₂ (CategoryTheory.Bicategory.associator f g h).hom)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))
              (mapComp f (CategoryTheory.CategoryStruct.comp g h))))
      CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_associator._autoParam),
  sizeOf
      { obj := obj, map := map, map_id := map_id, map₂ := map₂, map₂_id := map₂_id, map₂_comp := map₂_comp,
        mapComp := mapComp, mapComp_naturality_left := mapComp_naturality_left,
        mapComp_naturality_right := mapComp_naturality_right, map₂_leftUnitor := map₂_leftUnitor,
        map₂_rightUnitor := map₂_rightUnitor, map₂_associator := map₂_associator } =
    1