如何解决为什么在 agda 中没有公理 K 的归纳族和参数化归纳类型之间的宇宙级限制表现不同
在启用 List
的情况下在 agda 中定义 --without-K
时的观察:
接受以下参数化归纳定义:
data List (A : Set) : Set where
[] : List A
_::_ : A → List A → List A
但不是等效的归纳族定义:
data List' : Set → Set where
[]' : {A : Set} → List' A
_::'_ : {A : Set} → A → List' A → List' A
错误消息是 Set₁ is not less or equal than Set
,因此我必须将类型从 List' : Set → Set
更改为 List' : Set → Set₁
以进行类型检查。如果我禁用 --without-K
,那么 agda 也会正确地进行类型检查。
我试图查找为什么会出现这种情况,例如,在页面 https://agda.readthedocs.io/en/latest/language/without-k.html 上它说“启用 --without-K
时,必须在更高的 Universe 级别定义某些索引数据类型。特别是,所有索引的类型都应该符合数据类型的排序。”但它没有说明归纳族(索引数据类型)定义和参数化归纳定义之间存在这种差异的原因。我想这与底层类型理论的同伦模型解释有关。但是,我想知道如果归纳家庭生活在较小的宇宙中(语法和语义),会发生什么样的“坏”事情。参数化归纳定义如何避免此类问题?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。