§ 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.