[TYPES] Y-combinator in Type:Type?

Thomas Streicher streicher at mathematik.tu-darmstadt.de
Fri May 16 11:41:42 EDT 2008


But if you have Type:Type together with extensional identity types then
every type X is equal to X->X and thus provides a model for untyped
lambda calculus and thus allows one to write down an Y-combinator of type X.

So the problem is open because of intensional identity types, isn't it?

Thomas


More information about the Types-list mailing list