同伦类型理论和 Voevodsky 的单价基础一文的 coq 代码
coq code of the article Homotopy type theory and Voevodsky's univalent foundations
我正在阅读文章 Homotopy type theory and Voevodsky's univalent foundations by Álvaro Pelayo, Michael A. Warren recently. There is a companion file http://mawarren.net/papers/tutorial.v。我用最新的coc版本8.8.0编译，但是遇到了错误。谁能帮我？提前致谢。
此代码旨在使用自定义补丁版本的 Coq 8.4 或 Coq 8.3 构建，该版本禁用了 universe 检查；我记得当时与 Dan Grayson 或 Vladimir 交谈过，他们提到使用这样一个补丁版本的 Coq。 （另请注意，该文件来自 2012 年 8 月，https://coq.inria.fr/news/ 表示 Coq 8.4 于该月发布。）非常不幸的是，您引用的文章似乎没有在任何地方提及 Coq 的版本。
在任何情况下，您都可以通过将参数 -type-in-type 传递给 coqc 或 coqtop 并添加
在 Coq 8.5 及更新版本中构建此文件
Set Asymmetric Patterns.
在文件的顶部。如果您使用 ProofGeneral，您可以添加
(* -*- coq-prog-args: ("-type-in-type") -*- *)
也添加到文件顶部，这样您就不必手动将 -type-in-type 传递给 coqtop。
我正在阅读文章 Homotopy type theory and Voevodsky's univalent foundations by Álvaro Pelayo, Michael A. Warren recently. There is a companion file http://mawarren.net/papers/tutorial.v。我用最新的coc版本8.8.0编译，但是遇到了错误。谁能帮我？提前致谢。
此代码旨在使用自定义补丁版本的 Coq 8.4 或 Coq 8.3 构建，该版本禁用了 universe 检查；我记得当时与 Dan Grayson 或 Vladimir 交谈过，他们提到使用这样一个补丁版本的 Coq。 （另请注意，该文件来自 2012 年 8 月，https://coq.inria.fr/news/ 表示 Coq 8.4 于该月发布。）非常不幸的是，您引用的文章似乎没有在任何地方提及 Coq 的版本。
在任何情况下，您都可以通过将参数 -type-in-type 传递给 coqc 或 coqtop 并添加
Set Asymmetric Patterns.
在文件的顶部。如果您使用 ProofGeneral，您可以添加
(* -*- coq-prog-args: ("-type-in-type") -*- *)
也添加到文件顶部，这样您就不必手动将 -type-in-type 传递给 coqtop。