问题标签 [homotopy-type-theory]

高级归纳类型是同伦类型理论中非常重要的工具。我正在尝试使用 Z3-SMT-LIB 定义一些更高的归纳类型。一个例子是圆，它是由一个点base和一条路径自由生成的loop，从base到它自己。我正在使用代码

输出是

问题是：我真的在定义更高的归纳类型，叫做圆？

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

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

这是同伦类型理论书中的一个练习。这是我所拥有的：

我不知道如何证明这一点recℕ z f (succ n) ≡ f n (recℕ z f n)。我需要证明：

在英语中，给定一个自然数n和归纳假设证明了结果。

中缀运算符_∘_是正常的函数组合。和数据类型定义为_≡_：_×_

我一直在想一个解决方案，但我不知道如何解决这个问题。

在 HOTT 和 COQ 中，无法证明 UIP，即
\Prod_{p:a=a} p = refl a

但可以证明：
\Prod_{p:a=a} (a,p) = (a, refl a)

为什么这样定义？是不是因为想要一个好的同伦解释？或者这个定义有什么自然的、更深层的原因？

我最近在阅读 Álvaro Pelayo、Michael A. Warren 的文章同伦类型理论和 Voevodsky 的单价基础。有一个配套文件http://mawarren.net/papers/tutorial.v。我用最新的 coq 版本 8.8.0 编译它，但遇到了错误。谁能帮我？提前致谢。

根据同伦类型理论（第 49 页），这是相等的完整归纳原理：

我对HoTT不太了解，但我确实看到路径归纳比eq_rect：

相反，我未能path_induction从eq_rect. 可能吗 ？如果不是，平等的正确归纳原则是什么？Inductive我认为这些原则是从类型定义中机械地派生出来的。

编辑

多亏了下面的答案，关于相等的完整归纳原则可以由

然后我们得到相反的，

使用该cubical-demo库，我认为以下证明将是微不足道的：

但是，唉，它并没有定义：尝试使用refl失败

我不知道从哪里开始。

单价公理是可逆的（模路径）吗？是否可以使用Agda 的 Cubical 库来证明以下内容：

我怀疑上述内容应该成立，因为在HoTT book的示例 3.19 中，证明中有一个步骤使用两个等价之间的等价来证明它们的功能之间的等价：

[...]f等价物也是如此。因此，通过一元性，f产生了一条路径p : A ≡ A。

如果p等于refl A，那么（再次通过单价）f将等于 的恒等函数A。

我在 CS SE 上问了以下问题：

例如，在 HoTT 书中引理 6.4.1 的证明中，在函数上归纳定义的函数简单地应用于路径loop 和refl，然后使用和之间的路径loop（refl可能是通过同余通过f）来构造和之间的f loop路径f refl：

假设loop = refl base. [...] 与x : Aand p : x = x，有一个由and f : S1 → A定义的函数，我们有f(base) :≡ xf(loop) := p

但在立体环境中，事情就不是那么清晰了。f(loop)不是很好的类型，只是f(loop i)，对于某些i : I. 但是上面的证明变成了

但这不需要在中间步骤中进行某种“区间扩展”吗？立方体类型理论中的中间步骤的正当性究竟是什么？我可以看到如何证明∀ i → f (loop i) = f (refl base i)，但是如何将其“提升”到<i> f (loop i) = <i> f (refl base i)？

我在那里没有收到回复，所以我要在这里尝试，用具体的 Agda 代码来支持它。

我正在尝试将上述证明转换为 Cubical Agda，如下所示。首先，给定p的定义f很简单：

我们可以逐点loop证明f (loop i) ≡ f (refl i)：

（要了解原因，这里有更详细的说明：

)

但如果我试图证明整个事情：

它失败了，我想是因为我试图使用的“区间扩展性”：

无法将元变量实例化为_342解决方案f (loop i) ≡ f base，因为它包含不在元变量i范围内或在元变量中不相关但在解决方案中相关的变量

检查表达式proofAt i是否具有类型时_A_342

尝试将其 eta 转换为 justproofAt_也失败了，但出于不同的原因（我认为通常没有路径的 eta 转换）：

((i : I) → f (loop i) ≡ f base)!=<_344 ≡ _y_345类型 ;Agda.Primitive.Setω

那么，上述HoTT证明的正确CTT音译是什么？