Proof assistants based on dependent type theory—such as Agda, Lean, and Rocq—employ
different universes to classify types, typically combining a predicative tower for
computationally relevant types with a possibly impredicative universe for proof-irrelevant
propositions. Several other universes with specific logical and computational principles
have been explored in the literature. In general, a universe is characterized by its sort
(e.g., Type, Prop, or SProp) and, in the predicative case, by its level. To improve
modularity and better avoid code duplication, sort polymorphism has recently been
introduced and integrated in the Rocq prover.

However, we observe that, due to its unbounded formulation, sort polymorphism is currently
insufficiently expressive to abstract over valid definitions with a single polymorphic
schema. Indeed, to ensure soundness of a multi-sorted type theory, the interaction between
different sorts must be carefully controlled, as exemplified by the forbidden elimination
of irrelevant terms to produce relevant ones. As a result, generic functions that
eliminate values of inductive types from one sort to another cannot be made polymorphic;
dually, polymorphic records that encapsulate attributes of different sorts cannot be
defined. This lack of expressiveness also breaks the possibility to infer principal
types, which is highly desirable for both metatheoretical and practical reasons. To
address these issues, we extend sort polymorphism with bounds that reflect the required
elimination constraints on sort variables. We present the metatheory of bounded sort
polymorphism, paying particular attention to the consistency of the resulting constraint
graph. We implement bounded sort polymorphism in Rocq and illustrate its benefits
through concrete examples. Bounded sort polymorphism with elimination constraints is a
natural and general solution that effectively addresses current limitations and fosters
the development of, and practical experimentation with, multi-sorted type theories.