Yoneda is CPS, think again
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 - the isomorphism is between a fixed A and a dependently typed function:
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 a type X)
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 - the isomorphism is between a fixed A and a dependently typed function:
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 a type X)