Sheng-Yi Jiang

Contravariant Universe Subtyping, Formalized, Mechanized

In a type theory with a cumulative universe hierarchy, \emph{subtyping} is often incorporated to lift lower universe levels to higher ones. In practice, kernels of proof assistants typically implement universe subtyping conservatively: subtyping only propagates covariantly into the output types of $\Pi$ types, while in...