Agda开启--without-K时归纳族与参数化归纳类型的宇宙层级限制差异成因

在Agda中开启--without-K编译选项后，可以观测到明显的类型检查行为差异：

• 以下带外部参数的归纳定义可以正常通过类型检查：

data List (A : Set) : Set where
    [] : List A
    _::_ : A → List A → List A

• 语义上等价的全索引归纳族定义会触发Set₁ is not less or equal than Set报错，只有把List'的返回类型从Set修改为Set₁才能通过校验：

data List' : Set → Set where 
    []'  : {A : Set} → List' A
    _::'_ : {A : Set} → A → List' A → List' A

• 如果关闭--without-K选项，两种定义都可以无修改通过类型检查。

当前观测到的差异背后，存在两个待解释的问题：

• 开启--without-K时，将索引归纳族定义在更低的宇宙层级（即与索引同层级），会在语法和语义层面引发哪些具体问题？
• 参数化归纳定义的设计，是从哪些层面规避了这种层级约束的？

首先需要明确Agda对归纳定义中“参数”和“索引”的本质处理逻辑，这是层级校验分歧的来源：

• 写在data关键字后、冒号前的参数，是整个归纳类型生成阶段就固定的外部绑定。以data List (A : Set) : Set为例，定义逻辑是：对任意给定的A : Set，独立生成对应的List A类型的所有构造子，整个构造子的定义过程中A是全局固定的，不需要在构造子签名里重新绑定。这种生成方式产出的List A是无索引的普通归纳类型，不受“带索引归纳族”的特殊校验规则约束。
• 写在data关键字后、整体类型签名里的索引，是构造子定义阶段才临时引入的可变绑定。以data List' : Set → Set为例，整个类型是一个从集合到集合的归纳族，每个构造子都需要在自己的签名里显式声明当前作用的索引值（比如[]'签名里的{A : Set} → List' A），此时A是归纳族的内部索引，直接受带索引归纳族的校验规则约束。

开启--without-K时，Agda针对带索引归纳族新增了一条强制校验规则：归纳族的返回值宇宙层级，必须严格高于其所有索引所在的宇宙层级。
对应到报错场景：List'的索引A位于Set层级（即宇宙0），按照规则它的返回值至少需要是Set₁层级；如果强行把返回值写为Set，就相当于把本来属于Set₁层级的类型嵌入到Set层级，直接触发宇宙层级的不匹配错误。而关闭--without-K时，由于默认开启了恒等类型的证明无关性（即K原理），索引的相等性被默认为是平凡的，不需要额外的层级保护，因此同层级的归纳族可以通过校验。

强制要求索引归纳族抬升宇宙层级，本质是为了在关闭K原理的前提下，保证类型论模型的逻辑一致性，避免两类经典的一致性矛盾：

1. 非平凡路径的坍缩风险：开启--without-K意味着不再默认“同一类型的所有相等证明都是等价的”（即不再承认UIP原理）。如果允许索引归纳族和索引处于同一宇宙层级，就可以构造出利用归纳族递归性定义的小类型，反过来证明“所有相等路径都等于恒等证明”，直接和--without-K的非UIP假设矛盾，破坏整个类型系统的语义一致性。
2. 宇宙良基性破坏：同层级的索引和归纳族会形成类似罗素悖论的循环定义——索引本身是一个宇宙下的集合，而归纳族是从集合映射到集合的函数，如果函数的返回值和索引处于同一宇宙，就可以在定义中构造出“将自身作为元素”的递归循环类型，违反类型论宇宙的良基性要求。

参数化归纳的设计从根源上规避了索引归纳族的约束，核心原因有两点：

• 参数化归纳的本质是“对每个固定参数，生成一个完全独立的无索引普通归纳类型”。比如List A在给定A之后，就是一个没有任何内部索引的普通归纳类型，完全不触发带索引归纳族的特殊层级校验规则。
• 参数是在归纳类型生成之前就固定的外部绑定，不会参与构造子层面的临时绑定，也就不会把索引的宇宙层级带回归纳类型的返回值层级。这种情况下，哪怕开启了--without-K，List A作为无索引的普通归纳类型，完全可以合法定义在Set层级，不需要抬升到更高宇宙。

注：很多开发者会误认为List和List'是完全等价的类型，但在带--without-K的语境下，二者的逻辑属性存在本质差异：List'的索引A是可以参与相等性路径构造的内部索引，而List的参数A是外部固定绑定，不会参与索引层面的路径运算。

内容的提问来源于stack exchange，提问作者Kaa1el