Representing objects are unique up to isomorphism?

Stream: Is there code for X?

[Robert Maxton]

If a functor F : Cᵒᵖ ⥤ Type _ is representable by two objects X, X', then X ≅ X'.

[Michał Mrugała]

I couldn't find it myself. Would be helpful to have it if you'd be willing to PR it!

[Edward van de Meent]

i might be forgetting how this works, but i think this isn't true?

[Michał Mrugała]

I'm pretty sure it's true by Yoneda. The images of X and X' under the Yoneda embedding are naturally isomorphic. Since the Yoneda embedding is fully faithful there is an isomorphism between X and X'.

[Robert Maxton]

Yeah, Yoneda gives you a unique morphism from X to X' and back, plus X to itself, and is functorial, so taking the unique arrow to X' and back gets you the identity.

[Robert Maxton]

Or that

[Edward van de Meent]

yea, i was forgetting how this works

[Robert Maxton]

Michał Mrugała said:

I couldn't find it myself. Would be helpful to have it if you'd be willing to PR it!

#24059