{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} →
            {P : Sort u} →
              {homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)} →
                {homEquiv_naturality_left_symm :
                    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} →
                  {homEquiv_naturality_right :
                      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} →
                    {homEquiv' : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)} →
                      {homEquiv_naturality_left_symm' :
                          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} →
                        {homEquiv_naturality_right' :
                            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} →
                          { homEquiv := homEquiv, homEquiv_naturality_left_symm := homEquiv_naturality_left_symm,
                                homEquiv_naturality_right := homEquiv_naturality_right } =
                              { homEquiv := homEquiv', homEquiv_naturality_left_symm := homEquiv_naturality_left_symm',
                                homEquiv_naturality_right := homEquiv_naturality_right' } →
                            (homEquiv ≍ homEquiv' → P) → P