A Metatheoretic Analysis of Subtype Universes

Subtype universes were initially introduced as an expressive mechanisation of bounded quantification extending a modern type theory. In this paper, we consider a dependent type theory equipped with coercive subtyping and a generalised, more expressive model of subtype universes. We prove results regarding the metatheoretic properties of subtype universes, such as consistency and strong normalisation. We analyse the causes of undecidability in bounded quantification, and we discuss how coherency impacts the metatheoretic properties of theories implementing bounded quantification. We discuss the effects of certain natural choices of subtyping inference rules on the expressiveness of a type theory. We describe applications in natural language semantics, programming languages, and mathematics formalisation.