Gabriel Scherer: Universe subtyping in Martin-Löf Type Theory
Universe subtyping in Martin-Löf Type Theory
In this talk, I will present the current state of our work -- with Andreas Abel -- on the metatheory of dependent type systems with a universe hierarchy.
Our not-yet-reached goal is universe polymorphism, as a potential extension of the Agda system. This means that we have to develop both:
- a suitable formalization of universe subtyping and its metatheory
- a practical type checking algorithm, along with proofs that the algorithms are faithful to the declarative type system