To exploit the expressivity of being able to refer to the type of types, such as for large elimination, dependent type systems will either employ a universe hierarchy or else contend with an inconsistent type-in-type rule. However, these are not be the only possible options. Taking inspiration from Stratified System F, we introduce Stratified Type Theory (StraTT), where rather than stratifying universes by levels, we stratify typing judgements and restrict the domain of dependent function types to some fixed level strictly lower than that of the overall type. Even in the presence of type-in-type, this restriction suffices to enforce consistency of the system. We explore the expressivity of several extensions atop this design. First, the subsystem subStraTT employs McBride's crude-but-effective stratification (also known as displacement) as a simple form of level polymorphism where top-level definitions can be displaced uniformly to any higher level as needed, which is valid due to level cumulativity and plays well with stratified judgements. Second, to recover some expressivity lost due to the restriction on dependent function domains, the full StraTT system includes a separate nondependent function type with floating domains, whose level instead matches that of the overall type. Finally, we have implemented a prototype type checker for StraTT extended with datatypes along with a small type checked core library. While it's possible to show that the subsystem is consistent, showing consistency for the full system with floating nondependent functions remains open. Nevertheless, we believe that the full system is also consistent and have mechanized a syntactic proof of subject reduction. Furthermore, we use our implementation to investigate various well-known type-theoretic type-in-type paradoxes. These examples all fail to type check in expected ways as evidence towards consistency.

翻译：为利用可引用类型之类型（例如用于大消除）的表达能力，依赖类型系统要么采用宇宙层级结构，要么需要处理不一致的类型即类型规则。然而，这些并非唯一可能的选择。受分层系统F的启发，我们引入了分层类型理论（StraTT），其中并非按层级对宇宙进行分层，而是对类型判断进行分层，并将依赖函数类型的定义域限制为严格低于整体类型的某个固定层级。即使存在类型即类型规则，这一限制也足以保证系统的一致性。我们探索了在此设计基础上若干扩展的表达能力。首先，子系统subStraTT采用麦克布莱德的粗糙但有效的分层（亦称位移）作为简单的层级多态形式，其中顶层定义可按需统一位移至任何更高层级——这凭借层级累积性得以成立，且与分层判断良好配合。其次，为恢复因依赖函数定义域限制而损失的部分表达能力，完整StraTT系统包含一个独立的非依赖函数类型及浮动定义域，其层级与整体类型相匹配。最后，我们实现了扩展了数据类型的StraTT原型类型检查器，以及一个经类型检查的小型核心库。虽然能够证明子系统的一致性，但包含浮动非依赖函数的完整系统的一致性证明仍悬而未决。尽管如此，我们相信完整系统也是一致的，并通过机械化手段完成了主题归约的语法证明。此外，我们利用实现探究了若干著名的类型论类型即类型悖论。这些示例均以预期方式未能通过类型检查，作为一致性的佐证。