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