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

在乌尔夫·诺雷尔(Ulf Norell)的论文中，他提到 Agda (Agda)基于罗的UTT。但是，我在那里找不到使用Prop的方法。有什么办法吗？

最佳答案

Prop宇宙在Agda的早期版本中可用，但此后已被删除。实际上，Prop仍然是Agda中的关键字，但是使用它会导致错误Prop is no longer supported。根据要实现的目标，您可以选择以下几种:

您可能想看看Agda的proof irrelevance功能。

我见过有人使用Prop = Set的同义词。如果您想在命题和更一般的集合之间进行逻辑上的区别，这很有用，但是当然，它不会给您Prop的任何其他公理。

最后，存在来自HoTT的(同伦)命题类型，可以在Agda中通过hProp = Σ[ X ∈ Set ] ((x y : X) → x ≡ y)进行定义。这保证了命题最多具有一个证明，但是会造成相当大的开销。

关于agda - 如何在Agda中使用UTT的Prop，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/22750429/