Subtype Universes

Subtype universes - a collection of subtypes of a given type - were proposed as a rich extension of modern type theories and as a potential solution to the undecidability of bounded quantification in some type systems. This project analyses a more expressive version of subtype universes and the role they play in type systems without type universes, with a key focus on desirable metatheoretic properties such as logical consistency, strong normalisation, and the decidability of type checking and the subtype relation.

In our analysis, the monotonic property of subtyping relations - in layman's terms, that more complex types cannot be subtypes of simpler types - was found to be key. When a system has subtype universes monotonic coercive subtyping, we were able to produce a reduction of that system down to the well-studied UTT[C], Luo's Unifying Theory of Dependent Types equipped with coercive subtyping. As a result, logical consistency, strong normalisation, and the decidability of type checking and the subtype relation hold.

In the case where a system does not have monotonic subtyping, it is possible to define a reduction of that system down to a version of the system without the non-monotonic subtyping relation, and thus these systems also preserve these metatheoretic properties. This means that the logical properties of a system with coercive subtyping and subtype universes is independent of the choice of subtyping relations, so long as the subtyping relations are coherent.

It was also found that coercive subtyping and subtype universes have interesting relationships to that of homotopy type theory: one can think of subtyping as describing continuous embeddings of one space into another, and subtype universes as describing a kind of path space between these spaces. Further analysis of this was outside the scope of this paper, however.