Kon*_*tov 5 agda dependent-type
在Ulf Norell的论文中,他提到Agda是基于罗的UTT.但是,我找不到在那里使用Prop的方法.有没有办法这样做？
Prop宇宙在早期版本的Agda中可用,但它已被删除.实际上,Prop仍然是Agda中的关键字,但使用它会产生错误Prop is no longer supported.根据您想要实现的目标,您有以下几种选择:
您可能想看看Agda的证明无关性功能.
我见过有些人使用同义词Prop = Set.如果你想在命题和更一般的集合之间做出逻辑差异,这很有用,但当然它并没有给你任何额外的公理Prop.
最后,有来自HoTT的(同伦)命题的类型,可以在Agda中定义hProp = ?[ X ? Set ] ((x y : X) ? x ? y).这保证了命题最多有一个证明,但可能会导致相当大的开销.