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

首先，感谢您对观察型理论的提问。第二，你们在这里所做的事情似乎是紧密联系在一起的，尽管在不同的地方有不同的东西，从托尔斯滕·奥尔滕基奇，沃特·斯威勒斯特拉和我把它们放在我们的故事版本中。第三，毫不奇怪(至少对我而言)，连贯是可以衍生的，而反身性则是唯一的假设。我们的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的定义有多懒(这就是您如何获得无关性的证据)，您只需要一个假设。

使用您的特定公式，您甚至可以避免使用齐次值相等。如果你用矫顽力子而不是方程来修正类型间隙，你可能会省去一些麻烦(并且可能在函数相等的域类型上去掉这个方程)。当然，在这种情况下，您需要考虑如何替换一致性语句。

我们非常努力地将强制排除在平等的定义之外，保持某种对称性，并将类型方程排除在价值方程之外，大多数情况下一次就可以少考虑一些问题。有趣的是，通过“一件事和它的强制”代替“两个平等的东西”，结构的某些部分可能会变得更容易。