coq - HoTT 的 Coq：证明 || P-> X || -> (P-> ||X||)

Question

我需要在 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 库。

Answer 1

您需要这样做，Require Import Basics.因为 coq 不知道 Trunc.TruncType 可以强制转换为 Type 否则。您要了解的策略是apply Trunc_ind针对诸如forall (x : Tr _ _), _.

intros x y并将revert x派上用场将目标转化为您要申请的表格trunc_ind。

您还具有（自定义）策略strip_truncations，它将在上下文中搜索任何被截断的术语，并尝试对它们进行归纳以删除它们。这要求目标被截断，但这在这里不应该是一个问题。

最后，截断的构造函数是tr，所以你可以apply在那里使用。