{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {F : CategoryTheory.Functor C (Type v)} →
      {X : C} →
        {P : Sort u} →
          {homEquiv : {Y : C} → (X ⟶ Y) ≃ F.obj Y} →
            {homEquiv_comp :
                autoParam
                  (∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
                    homEquiv (CategoryTheory.CategoryStruct.comp f g) = F.map g (homEquiv f))
                  CategoryTheory.Functor.CorepresentableBy.homEquiv_comp._autoParam} →
              {homEquiv' : {Y : C} → (X ⟶ Y) ≃ F.obj Y} →
                {homEquiv_comp' :
                    autoParam
                      (∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
                        homEquiv' (CategoryTheory.CategoryStruct.comp f g) = F.map g (homEquiv' f))
                      CategoryTheory.Functor.CorepresentableBy.homEquiv_comp._autoParam} →
                  { homEquiv := homEquiv, homEquiv_comp := homEquiv_comp } =
                      { homEquiv := homEquiv', homEquiv_comp := homEquiv_comp' } →
                    (homEquiv ≍ homEquiv' → P) → P