OTT中可证明的连贯性

Question

我正在玩观察型理论.

这里是强制相互定义的?-types(?是小写?,即? A B代码(x : A) -> B x)的相等性:

? A? B? ? ? A? B? = ? (A? ? A?) ? P -> ? _ ? x -> B? (coerce P x) ? B? x

和相应定义的函数相等(?是小写?):

_?_ {A = ? A? B?} {? A? B?} f? f? = ? (A? ? A?) ? P -> ? _ ? x -> f? (coerce P x) ? f? x

因此,不是"相等的函数将相等的输入映射到相等的输出",而是"相等的函数映射定义相等的输入到相等的输出".

在此设置中 coherence

coerce : ? {? ?} {A : Univ ?} {B : Univ ?} -> ? A ? B ?? -> ? A ?? -> ? B ??
coherence : ? {? ?} {A : Univ ?} {B : Univ ?}
          -> (P : ? A ? B ??) -> (x : ? A ??) -> ? x ? coerce P x ??

(Univ 0是Prop,Univ (suc ?)是Type ?)

是可证明的.我唯一需要假设的是

postulate ?-refl : ? {?} -> (A : Univ ?) -> ? A ? A ??

但我们可以调整平等处理A ? A作为一个特例(我认为,trustMe需要一个朋友_?_ : ? {?} {A : Set ?} (x y : A) -> Maybe (x ? y)).

我们仍然需要假定要定义的subst东西和其他东西.

我错过了什么？我们是否会失去任何不相干性？在函数相等的定义中提到类型相等似乎是可疑的.通过限制相等函数的输入在定义上相等,我们是否会损失很多？强烈正常化是否有任何好处,coherence或者无关紧要,因为它在计算上无关紧要？

代码(我完全忽略了积极性,终止和累积性问题).

Answer 1

首先,感谢您询问观测类型理论.其次,你在这里所做的事情确实似乎在一起,即使它有不同的地方,Thorsten Altenkirch,Wouter Swierstra和我把它们放在我们的故事版本中.第三,毫不奇怪(至少对我而言)一致性是可推导的,只有反身性才是唯一的假设.我们的OTT也是如此,当我们写这篇论文时,Wouter在Agda 1中做了证明.证明不相关和生命的短暂意味着我没有将他的证据移植到Agda 2.

如果你错过了任何东西,它就会潜伏在你的评论中

我们仍然需要假定要定义的subst东西和其他东西.

如果你有一些P : X -> Set,一些a, b : X和一些q : a = b,你期望得到一个功能P a -> P b."相等的功能对平等输出采取相同的输入"的表述为您提供了refl P : P = P,因此q,我们可以推导出P a = P b.你的"相同的功能需要一个给定的输入到相等的输出"的公式不允许你让q差距缩小a到b.

在存在refl和的情况下subst,"两个相等的输入"与"两个地方使用的一个输入"相同.在我看来,你已经将工作转移到了你需要的任何其他东西上subst.根据你的定义coerce是多么懒惰(这就是你如何得到证据不相关),你只需要一个假设.

使用您的特定配方,您甚至可以获得同质的价值平等.如果你用强制而不是方程来修正类型间隙,你可能会省去一些麻烦(并且可能在函数相等的情况下摆脱域类型上的那个等式).当然,在这种情况下,你需要考虑如何取代连贯性陈述.

我们非常努力地将强制排除在平等的定义之外,保留某种对称性,并将类型方程式保持在价值方程之外,主要是为了不必一次考虑.有趣的是,至少有一部分建筑可能会变得更容易,"一件事和它的强制"取代"两件平等的事情".