§ Predicative v/s Impredicative: On Universes in Type Theory
§ Tarski formulation of univereses

U
is a code for types.  We have a decoding function
T: U → Type
.
U type
a ∈ U

T(a) type
 Universes bump up levels when we quantify over them?
 Impredicative universes are closed under quantification over types of that same universe.
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.