types - 我如何说服 Agda 的宇宙检查器我所做的事情是有根据的？

Question

我有一个函数可以将自然数映射到它们相应的 Agda 宇宙级别。

level : Nat -> Level
level zero = lzero
level (suc l) = lsuc (level l)

Setn : (l : Nat) -> Set (level (suc l))
Setn l = Set (level l)

我以这种方式在归纳数据类型的定义中使用此函数:

data U l : Setn l where
  ...
  Lift : {l' : Nat} -> {l' <= l} -> U l' -> U l

在这里，Agda 提示 Set (level l')不小于或等于 Set (level l) ，这显然是错误的，尽管我知道 Agda 没有能力推导出 Set (level l') <= Set (level l)来自 l' <= l .我如何向 Agda 的 Universe checker 暗示这个定义确实是有根据的？

Answer 1

你没有。
这可能不是您想听到的答案，但 Agda 拒绝这种类型是有充分理由的，即使您使用 Universe 级别的方式似乎是正确的。特别是，如果 Agda 允许这样做，那么强规范化(以及类型检查的可判定性)将丢失:在具有 1 <= 0 证明的开放上下文中。 ，您将能够利用此数据类型(或其变体)来定义不遵守 Universe 层次结构的数据类型，然后可以使用它(通过 Girard 悖论)来定义非终止项。由于 Agda 无法确定假设是否一致，因此它完全排除了这些用户证明的级别不等式，只相信自己的求解器。