{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} →
            (homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) →
              autoParam
                  (∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
                    (homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
                      CategoryTheory.CategoryStruct.comp (F.map f) ((homEquiv X Y).symm g))
                  CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm._autoParam →
                autoParam
                    (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
                      (homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) =
                        CategoryTheory.CategoryStruct.comp ((homEquiv X Y) f) (G.map g))
                    CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right._autoParam →
                  CategoryTheory.Adjunction.CoreHomEquiv F G