agda - 如何在 Agda 中使用来自 UTT 的 Prop

Question

在Ulf Norell 的论文中，他提到Agda 是基于Luo 的UTT。但是，我找不到在那里使用 Prop 的方法。有什么办法吗？

Answer 1

Prop Universe 在 Agda 的早期版本中可用，但此后已被删除。事实上，Prop仍然是 Agda 中的关键字，但使用它会出现错误 Prop is no longer supported .根据您想要实现的目标，您有几个选择:

您可能想看看 Agda 的 proof irrelevance特征。

我看到有些人使用同义词 Prop = Set .如果你想在命题和更一般的集合之间做出逻辑上的区别，这很有用，但当然它不会给你任何 Prop 的额外公理。 .

最后，还有来自 HoTT 的(同伦)命题类型，它可以在 Agda 中由 hProp = Σ[ X ∈ Set ] ((x y : X) → x ≡ y) 定义。 .这保证了命题至多有一个证明，但会导致相当多的开销。