Yoneda Lemma doesn't imply that. But their paper uses weird notation and handwavy explanations (at least in the key moment where they transition from parametricity to functors), so all I am wondering is how they don't end up with isomorphism like that. :)
The weird notation is:
C(A,B) ≅ ∀ X . C(B,X) → C(A,X)
The _→_ is not just a function from a set to a set here. What does ∀ X mean? They mean many more unsaid things. Because it really should be a Hom-set for a category of functors from C to Set - eg commutativity implied (for C(B,X)→C(A,X) and C(B,Y)→C(A,Y) for all functions f : X→Y).
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2020-05-14 03:04 pm (UTC)The weird notation is:
C(A,B) ≅ ∀ X . C(B,X) → C(A,X)
The _→_ is not just a function from a set to a set here. What does ∀ X mean? They mean many more unsaid things. Because it really should be a Hom-set for a category of functors from C to Set - eg commutativity implied (for C(B,X)→C(A,X) and C(B,Y)→C(A,Y) for all functions f : X→Y).