4

我想学习 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也被使用，但它们在这里不起作用。我在哪里可以找到教程开始？

4

3 回答 3

3

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

于 2015-05-13T13:36:22.690 回答
1

我不熟悉启用 HoTT 的 Coq 变体，但是当您定义一个归纳类型时，您的circle所有构造函数都必须实际构造该类型的元素。你不能写例如

Inductive mytype : Type :=
  | foo1 : mytype        (* ok *)
  | foo2 : nat -> mytype (* ok *)
  | foo3 : nat -> False  (* urk! Not ok. *)
  | foo3 : nat -> 0 = 1  (* urk! Not ok. *)
  .

否则逻辑会很快变得不一致。现在，您可能认为 sinceZERO = ZERO是一个定理，假设存在的证明是无害的，但 Coq 无法自动意识到这一点。此外，这样的证明肯定不是 的构造函数ZERO。可能更好的选择是使用例如

Variable foo3 : ZERO = ZERO .

或类似的命令之一 ( Axiom,Hypothesis,...)。

于 2015-05-15T19:01:40.860 回答
1

Bruno Barras 的 Coq 分支有一个旧分支，它允许大致类似的语法。例如，参见示例文件 hit-hoh.v：

Inductive circle : U :=
   base
// loop : base=base.

唉，这个版本的 Coq 从 2015 年底就没有更新过，而且当前版本的 Coq 也没有这样的原生支持。

HoTT 库编码高级归纳类型的方式是扩展私有归纳。例如，在旧版本的圆文件中（后来被通过 coequaliziers 的定义替换），我们可以看到：

Module Export Circle.

Private Inductive S1 : Type1 :=
| base : S1.

Axiom loop : base = base.

Definition S1_ind (P : S1 -> Type) (b : P base) (l : loop # b = b)
  : forall (x:S1), P x
  := fun x => match x with base => fun _ => b end l.

Axiom S1_ind_beta_loop
  : forall (P : S1 -> Type) (b : P base) (l : loop # b = b),
  apD (S1_ind P b l) loop = l.

End Circle.

关键字告诉 Coq在Private Inductive当前模块之外禁用模式匹配；这允许我们强制用户仅使用给定模块中定义的消除/归纳原则。然后我们公理化路径构造函数，公理化它们的计算规则，并定义消除器。请注意，消除器必须l : loop # b = b在其主体中使用路径参数 ( )，否则 Coq 将假定您作为该参数传递的内容无关紧要。

~~~~~

我在哪里可以找到教程开始？

目前我不知道有任何此类教程，但我可能会建议查看contrib/HoTTBook.v其中contrib/HoTTBookExercises.v包含 HoTT 书籍/练习和 HoTT/HoTT 库之间的许多链接。看看这些定理和练习是如何陈述和证明的可能是有用的（并随时为尚未与任何东西相关联的问题/定理贡献您自己的解决方案/证明！）。

于 2018-12-03T21:11:51.310 回答