Yoneda is CPS

[sassa_nf]

https://bartoszmilewski.com/2015/09/01/the-yoneda-lemma/

forall r . (a -> r) -> r ≅ a

Is it forall a or not? Yoneda says yes. Does this mean type system is boolean?

Comments

[sassa-nf.livejournal.com]

Actially, it is just me getting confused.

Here we are not talking about an isomorphism ((A→⊥)→⊥)→A (from which booleanness would follow). Here we are talking about a _family_ of functions. That is, the type is also an input:

CPS transform is an isomorphism: ((X : Type)→(A→X)→X)→A

(Note it isn't a value of type X as the first argument, but the type X)