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]

Does this mean Hask type system is boolean then?

[zeit-raffer.livejournal.com]

no. it means that expression of cps with a quantifier is a good approximation for Yoneda.

[sassa-nf.livejournal.com]

да, я забыл, это же fast and loose reasoning, а не полная правда.

А как Йонеда в Set выглядит? Вот у нас есть Hom(A,-), тогда Hom(A,⊥) - пустое множество для непустых A. Не наврал? И вот множество стрелок из пустого множества (естественные преобразования) изоморфно множеству, отображающему A?..

[sassa-nf.livejournal.com]

а, тьфу, это же стрелка из пустого множества - одно из значений множества естественных преобразований.

[zeit-raffer.livejournal.com]

also we cannot prove the isomorphism in the underlying type system.