agda - OTT 中可证明的一致性

Question

我正在玩observational type theory .

这里是 π 类型的相等性(π 是小写的 Π，即 π 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

因此，我们不是“相等的函数将相等的输入映射到相等的输出”，而是“相等的函数将定义上相等的输入映射到相等的输出”。

在此设置中连贯性

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 需要一个 friend _≟_ : ∀ {α} {A : 设定 α} (x y : A) -> 也许 (x ≡ y))。

我们仍然需要假设一些东西来定义 subst 和其他东西。

我是不是错过了什么？我们会失去任何无关紧要的东西吗？在函数相等的定义中提及类型相等似乎很可疑。通过限制相等函数的输入在定义上相等，我们会损失很多吗？强规范化相干性有什么好处吗？或者没关系，因为它在计算上无论如何都是无关的？

The code (我完全忽略了积极性、终止性和累积性问题)。

Answer 1

首先，感谢您询问观察类型理论。其次，你在这里所做的似乎确实是连在一起的，尽管它的内容与托尔斯滕·阿尔滕基希、沃特·斯威斯特拉和我在我们的故事版本中放置的地方不同。第三，连贯性是可推导的，这并不奇怪(至少对我来说)，而自反性是唯一的假设。我们的 OTT 也是如此，当我们撰写那篇论文时，Wouter 在 Agda 1 中进行了证明。证明的无关性和生命周期的短暂意味着我没有将他的证明移植到 Agda 2。

如果您遗漏了什么，它就隐藏在您的评论中

We still need to postulate something to define subst and other stuff.

如果你有一些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 的定义有多懒是(这就是你如何获得无关性证明)，你只需要一个假设。

根据您的特定公式，您甚至可能会得到同质值相等。如果您使用强制而不是方程来修复类型间隙，则可能会为自己省去一些麻烦(并且可能会在函数相等中消除域类型上的方程)。当然，在这种情况下，您需要考虑如何替换连贯性声明。

我们非常努力地尝试将强制转换排除在平等的定义之外，以保留某种对称性，并将类型方程排除在值方程之外，主要是为了一次性减少考虑。有趣的是，通过“一个事物及其强制”取代“两个相等的事物”，至少构造的某些部分可能会变得更容易。