![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Yoneda is CPS, think again
Jul. 4th, 2016 09:52 amActially, 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)
