∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} [inst_2 : SizeOf C] [inst_3 : SizeOf D]
  (homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (unit : CategoryTheory.Functor.id C ⟶ F.comp G)
  (counit : G.comp F ⟶ CategoryTheory.Functor.id D)
  (homEquiv_unit :
    autoParam
      (∀ {X : C} {Y : D} {f : F.obj X ⟶ Y},
        (homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (unit.app X) (G.map f))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit._autoParam)
  (homEquiv_counit :
    autoParam
      (∀ {X : C} {Y : D} {g : X ⟶ G.obj Y},
        (homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (counit.app Y))
      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_counit._autoParam),
  sizeOf
      { homEquiv := homEquiv, unit := unit, counit := counit, homEquiv_unit := homEquiv_unit,
        homEquiv_counit := homEquiv_counit } =
    1 + sizeOf unit + sizeOf counit