∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y Y' : C}
  (e : F.RepresentableBy Y) (e' : F.RepresentableBy Y'),
  (e.uniqueUpToIso e').hom =
    CategoryTheory.Yoneda.fullyFaithful.preimage
      (CategoryTheory.NatIso.ofComponents
          (fun Z =>
            { hom := ⇑e'.homEquiv.symm ∘ ⇑e.homEquiv, inv := ⇑(e.homEquiv.trans e'.homEquiv.symm).symm, hom_inv_id := ⋯,
              inv_hom_id := ⋯ })
          ⋯).hom