types - Coq 的 HoTT 变体语法教程

Question

我想学习 Coq 的同伦类型理论 (HoTT) 变体。我正在浏览网站http://homotopytypetheory.org/ , 我已经安装了 Coq 的变种，我想用它玩一点，写下书中的例子，等等......但是我找不到解释基本语法的 pdf/html 文件。当我尝试使用 hoqide(coqide 的 HoTT 变体)时，这段代码

Require Import HoTT.
Inductive circle:Type1 := | ZERO : circle | loop : ZERO = ZERO.

我收到错误“错误:在当前环境中找不到引用零”。我想我没有加载足够的库，或者可能是 ZERO = ZERO不是从零到自身的路径类型的正确表示法。
在博客中，符号 ZERO ~~> ZERO和 Paths ZERO ZERO也被使用，但它们在这里不起作用。我在哪里可以找到教程开始？

Answer 1

我不知道您正在寻找的风格的任何教程，但据我所知，HoTT 并没有真正改变 Coq 中归纳类型的语法。相反，除了公理之外，他们还使用称为私有(private)归纳类型的特性来定义更高的归纳类型，同时保持一致性。例如，看看如何 the circle is defined在 HoTT 库本身中。