§ Predicative v/s Impredicative: On Universes in Type Theory

§ Tarski formulation of univereses

U type

a ∈ U
T(a) type
Q. Given a definition, give me an algorithm that says when the definition needs predicativity A. perform type + universe inference on the definition. If we get a constraint of the form Type lower = Type higher where lower < higher, then the definition needs impredicativity.