§ 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.
a ∈ U
- 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.