∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : SizeOf B] [inst_3 : SizeOf C] (toPrelaxFunctorStruct : CategoryTheory.PrelaxFunctorStruct B C)
  (map₂_id :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.id f) =
          CategoryTheory.CategoryStruct.id (toPrelaxFunctorStruct.map f))
      CategoryTheory.PrelaxFunctor.map₂_id._autoParam)
  (map₂_comp :
    autoParam
      (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
        toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.comp η θ) =
          CategoryTheory.CategoryStruct.comp (toPrelaxFunctorStruct.map₂ η) (toPrelaxFunctorStruct.map₂ θ))
      CategoryTheory.PrelaxFunctor.map₂_comp._autoParam),
  sizeOf { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp } =
    1 + sizeOf toPrelaxFunctorStruct