>Lean doesn't allow you to refer to `id` as an object, just an application of it to a known universe. That's true, but I don't think you necessarily need a typ

>Lean doesn't allow you to refer to `id` as an object, just an application of it to a known universe. That's true, but I don't think you necessarily need a type for all universes (excluding itself), just some other way to denote that type is supposed to be universe polymorphic. >Does that require forbidding full recursion, or can you still introduce non-computable objects? I'm not sure what you mean exactly. The core type theory assumes that all functions are terminating. You can 'cheat in' full recursion by providing a non-computational termination proof, but the type checker would still be assuming that its actually terminating. I think if that wasn't the case, it'd need to be restricted (unless you did something really weird like introducing infinite negative universe levels).