问题标签 [homotopy-type-theory]

I am reading the article about extensional type theory on n-lab and it mentions two ways to make intensional type theory extensional.

1. Definitional: Add rule p:Id(x,y) => x===y
2. Propositional: Add one of the following to the type theory
   • axiom UIP
   • axiom K
   • axiom stating Id((a,b_1),(a,b_2)) => Id(b_1,b_2) where (a,b_1) and (a,b_2) are both dependent pairs
   • add unconstrained pattern matching as in original Agda

My question is are these two ways equivalent?

Specifically, if so, can one derive p:Id(x,y) => x===y from axiom K or UIP?

我有一个天真的问题：

我们为什么不将这个公理添加到 Coq：

好的，它允许诸如 (nat->Prop)=(nat->bool) 和 (A\/B)->(A+B) 之类的非构造定理（证明在这里）。但是 Coq 的标准库已经有很多非建设性的公理。

它会导致矛盾吗？（如果是这样，我在哪里可以阅读证明？）或者只是还没有证明公理不会导致矛盾？也许它只是没用？

也许这就是 HoTT 库在https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v中重新定义路径类型的原因。这个“type_extensionality”公理不如单价公理强。如果存在 ProofIrrelevance、PropositionExtensionality，最后一个将失败。（bool 以两种不同的方式等效于自身，而 bool=bool 类型仅包含一个元素）。

我在 Agda 中有一个 Conats 的定义（实际上它是立方体库中的那个）。我试图证明相关的 F 代数是（同伦）终端。

我已经设法将 F-Coalgebra Homomorphsim 的存在证明到 Conat 余代数中，但我正在努力解决它的独特性方面。

具体而言，函子F是：

Conat/Base.agda

Conat/Properties.agda（修改为删除不相关的东西。这是我的代码所在的位置）

我遇到问题的特定位置在第二个文件的末尾标有一个洞。的定义isContr是

因为我使用的是立方体模式，所以可以证明相等（实际上是路径）与双模拟一致。我认为这以某种方式使我产生了共同作用，但我不知道如何。

还有Conat一个 hSet 的证明，它可能对证明有用，也可能没用。

我正在尝试为具有 HIT 域的函数的结果中的相等性编写证明。因为函数是在 HIT 上定义的，所以相等性证明也必须处理路径情况。在这些情况下，Agda 报告了我需要构建的高维路径的大量限制；例如：

然而，有问题的 HIT 恰好是一个集合（在isSet某种意义上）。因此，我能想到的任何具有正确端点的路径都与解决给定约束的路径无法区分。因此，更具体地说，假设我在范围内再引入两个术语：

我如何使用这两个定义来填补这个漏洞？

这是这个问题的延续，基于这个答案。使用 Saizan 解释的技术，并稍微考虑我的fromList-toList证明以避免有问题的递归，我设法填写了除了一个案例之外的所有fromList-toList. 我认为如果我只展示我所拥有的一切是最简单的：

集合是群，所以我想我可以尝试在最后一种情况下做和以前一样的事情，只是高一维。但这就是我开始失败的地方：由于某种原因，六个面中的两个不能使用FreeMonoid集合的事实来构造。更具体地说，在下面代码中缺少的两个面中，如果我只是尝试通过放入isSet→isSet' squash孔来进行细化（没有指定更多参数），我已经得到“无法细化”。

这是我设法填写的四个面孔的代码：

报告的两个缺失面的类型是：

和

当然，我并没有声称现有的四个面孔是正确的。

所以我想我的问题是，两个缺失的面孔是什么，或者，正确的 6 个面孔是什么？

我正在 Agda 中试验同伦类型理论。我使用 HIT 来定义整数：

现在，我想在整数上定义加法：

但是，编译器给出了一个错误，因为我还需要对等式构造函数进行模式匹配：

所以，我最终得到了这个：

Agda 的类型孔无济于事：

Agda 文档给出了 HIT 用法的示例，它在对环面和命题截断进行操作时在等式构造函数上进行模式匹配。但是，作为没有拓扑学背景的人，我并不完全了解正在发生的事情。

i[0, 1] 区间的and的目的是什么j，为什么它们会出现在我的相等构造函数模式中？如何使用i和j？我如何处理较高归纳的情况？

我从 github 存储库编译了 Lean 2。然后，按照 scr/emacs/README.md 中的说明，我修改了我的 .emacs 文件，打开一个文件，单击“创建新项目”，单击“打开”，输入“hott”并按 Enter。

然后我输入

我收到了一条消息

我也尝试lean-hott-mode了相同结果的命令。

我究竟做错了什么？

在 Cubical Agda 的标准库中，有一些有限的多重集，我在下面重现了它们的优雅定义：

[]作为右中性元素的证明使用了FMSetElimProp.f我不理解的抽象引理。因此，我试图直接证明，但我被卡住了。这是我的尝试：

我在正确的轨道上吗？我怎样才能完成这个证明？

假设我有一些代数结构的记录类型；例如对于幺半群：

然后我可以手动为幺半群同态创建一个类型：

但是有没有一种方法可以在Hom 不说明同态定律的情况下进行定义？M : Monoid A因此，作为从见证人到的某种映射N : Monoid B，但这对我来说没有多大意义，因为它是一个“映射”，我们已经知道它应该映射M到N......

我想把我对幺半群的定义分成多个部分：

• 幺半群的签名
• 幺半群定律，作为关系
• 此关系中元素的相等见证

我目前的想法是这样做：

现在，我想为自由幺半群创建一个数据类型，作为由幺半群法则商的原始语法的商类型。但我还没有想出如何摆脱RawFreeMonoid下面的定义，并以MonoidSig某种方式实现它：

所以这是我的问题：有没有办法以FreeMonoid这种方式定义，而无需手动写出RawFreeMonoidandrawFreeMonoid定义？