Coq 中独占命题的析取与 sumbool

Question

同伦类型论中存在一个函数：

|| P + ~P || -> P + ~P,

对于任何单纯的命题

P

（

||_||

表示命题截断）。该函数是通过证明

P + ~P

只是一个命题并使用命题截断消除原理来定义的。

Coq 中的等效项（没有 HoTT 库）是：

Conjecture or_to_sumbool : forall P : Prop, P \/ ~P -> { P } + { ~P }.

它不能以直接的方式证明，因为当目标有排序时，禁止对析取进行案例分析

Set

。有没有办法在 Coq 中证明这个说法还是不可能？

Answer 1

我知道这些名字对于新手来说有点混乱，但 Prop 并不是 Coq 中 HoTT 的 hprop 的对应项。 Prop 对应于提取时可以擦除的内容。因此，如果您可以消除

P \/ ~P

到

{P} + {~P}

，您将从将要删除的内容中提取计算内容，因此它不起作用。

要在 Coq 中进行 HoTT，您需要公理，只要保持一致就可以。有一些库可以做到这一点，例如 Coq-Hott 库 或 Unimath 库。