问题标签 [homotopy-type-theory]

我正在尝试在 Agda 中为类型理论和同伦类型理论介绍中给出的练习构建解决方案。

鉴于我在 Agda 中定义的相等E ⁼ (aka J ) 和K的依赖消除器，如下所示：

练习 16（第 13 页）将仅使用消除器推导出等式/身份证明 (UEP) 的唯一性。

我知道 UEP 可以通过模式匹配在 Agda 中证明，这要归功于公理 K，如下所示：

但是文章似乎暗示应该可以在没有模式匹配的情况下推导出一个证明，就像sym, trans，并且resp可以仅使用递归 R ⁼来证明：

鉴于 UEP 是 K 的直接结果，我的直觉是这肯定是可能的，但到目前为止我还没有成功。用 J 和 K 的某种组合可以证明以下内容吗？：

我注意到 Cubical 标准库定义Fin为依赖对而不是索引归纳类型。原因是 Cubical Agda 不完全支持索引归纳类型：https ://github.com/agda/cubical/pull/104#discussion_r268476220

一个链接的问题指出模式匹配不适用于归纳系列，因为hcomp并且transp尚未在它们上定义：https ://github.com/agda/cubical/pull/57#issuecomment-461174095

我定义Fin并Vec编写了一个模式匹配函数，它似乎工作正常：

然而这个问题仍然存在：https ://github.com/agda/agda/issues/3733

我想使用 Cubical Agda 以防我需要更高的归纳类型或函数扩展性，但我不想放弃Vec或Fin. 我对立方类型理论的细节不熟悉，所以我不知道在哪里hcomp以及transp会被调用。Cubical Agda 中归纳家庭的现状如何？如果我避免某些操作，我还能使用它们吗？

我正在使用 Agda 2.5.3 和HoTT Agda库来学习一些同伦类型理论。我定义了一个简单的 S¹：

现在我正在尝试为作为类型 A 的循环递归原理的函数定义记录类型：

但我得到这个错误：

我尝试过提高记录的宇宙级别，但没有运气。任何有关此消息含义的提示将不胜感激。

Cubical Agda 库定义了Modulo这样的类型：

这是一套吗？

挥手，我可以看到任何路径都是refls 和pre-steps 的组合，采用embed n ≡ embed (m * k + n); 并且由于_+_是关联的 and 0 +_ ≡ id，所以refls 和pre-steps 如何组合的结构无关紧要；但这将如何正式化？

我试图在 Coq 中用归纳原则明确证明命题同一性的对称性，但不能像在 agda 中那样用归纳原则来做到这一点。我不知道如何在 Coq 中本地声明一个变量，也不知道如何展开定义，如下所示。如何获得类似于下面的 agda 的证明？

这失败了，我怎样才能展开 D 以便我可以断言自反性？

我如何适用于正确的论点？如何通过策略在本地断言 D 和 d（是否有 where 或（让 a = b in）策略？）应用（Id_ind A x（forall a : A, Id A xa -> Prop））。

这是我试图模仿的 agda 代码

尽管 coq 和 agda J 不相等，但它们可能是可互派的。

我试图复制 HoTT 书（第 70 页）中的主要引理以证明 Eckmann Hilton 定理，仅使用 J（无模式匹配）。

它说：“但是，一般来说，定义水平合成的两种方法是一致的，α ⋆ β = α ⋆' β，正如我们可以通过对 α 和 β 以及剩余的两条 1 路径进行归纳，将所有内容简化为反身性……”

我很困惑E类型签名是否正确 - 应该r'并且s有不同的路径？ d不会改进，所以我认为有什么问题E？我也不太明白我应该采用哪两条路径来完成证明，它们是r'和s？如果是这样，我不明白这些最终动机应该是什么？不是减少“β”以r消除对 1 路径进一步归纳的需要吗？

欢迎任何答案/解决方案，更重要的是，欢迎思考问题的方式。

下面是到达这里的其余代码。

我正在使用立方标准库中定义的有限多重集类型： https ://github.com/agda/cubical/blob/0d272ccbf6f3b142d1b723cead28209444bc896f/Cubical/HITs/FiniteMultiset/Base.agda#L15

我能够重现计数可扩展性的证明，并且我的一个引理表明你可以从等式的两边删除一个元素并保持等式。

它类似于这个：https ://github.com/agda/cubical/blob/0d272ccbf6f3b142d1b723cead28209444bc896f/Cubical/HITs/FiniteMultiset/Properties.agda#L183

我的证明没有使用相同的语法，但在核心库语法中它是

其中证明使用remove1-≡-lemma由路径两侧组成的路径，该路径是在功能上由 组成的参数路径remove1 x。

这要求值的类型具有可判定的相等性，因为没有它 remove1 没有意义。但是引理本身并没有提到可判定的相等性，所以我想我会在没有假设的情况下尝试证明它。现在是一周后，我不知所措，因为这看起来很“明显”，但很难证明。

我认为我对这一点可证明的直觉可能来自我的经典数学背景，因此它并没有建设性地/持续地遵循。

所以我的问题是：在没有元素类型假设的情况下，这是否可以证明？如果是这样，证明的一般结构会是什么样子，我很难获得想要同时在两个 FMSets 上进行感应的证明（因为我主要是在尝试根据需要排列路径时猜测）。如果没有假设就无法证明，是否有可能证明它在某种形式上与必要的假设等价？

我试图证明 ap 在依赖产品类型下的功能性，类似于在 Agda 的 HoTT 书中的定理 2.6.5，并且对于如何在存在的情况下如何呈现功能性条件的类型感到困惑依赖类型，因为它需要传输。本书在第 2.7 节的末尾建议将此作为练习。

上面是尝试的定义，下面有一个独立的文件，可以从中找到支持材料。洞中的目标是：

在下面看到的上下文中。我不了解 patternInTele* 业务，因为我不知道它会在哪里声明，并且非常感谢任何详细说明。此外，我的想法是实现一个具有两个等式的依赖应用程序函数，ap2d第二个等式是由前者的传输引起的。

但是，我什至无法让它工作。似乎有人会执行双重传输以获得所需的结果，但我在最终相等的 lhs 上所做的任何事情似乎都没有改变目标，这总是C x y而不是所需的C x' y'. 这是考虑定义我所追求的正确方法吗，这是否有助于解决产生正确函子定理陈述的原始问题？什么是在这种情况下实现两者的正确方法，functorDProdEq以便ap2d它们节省空间，因为类型签名往往会变得多毛？

最后，这是代码。

我需要在 Coq 中证明对于任何类型 X 和任何命题 P（尽管我认为即使 P 是一种类型它也应该有效）存在

截断实现：|| P-> X || -> (P-> ||X||)

在哪里 ||_|| 是HoTT书中用来表示命题截断的符号。

我证明了类型论中的陈述：一个人通过使用命题截断的归纳原理得到论文，假设从 H ：|| P-> X || 和 ap: P 即 H=|H'|，其中 H': P->X ，然后定义 trunc_impl(p):= |H'(p)|。（|-| 表示 trucation 的构造函数，即 |_| : A -> ||A||）。

顺便说一句，我不能用 Coq 写它！任何帮助将不胜感激。

我正在使用 GitHub 上提供的 HoTT 库。