为什么J公理在给x,y签名时取2 x？

Question

首先，我已经查阅了一些相关资料，包括 HoTT 书和 this question。

但我仍然很困惑，我希望能从 Agda 中得到一个解释，但直接从它的数学公式中得到解释。去掉点符号后，J公理是这样说的，其类型签名与我上面提到的问题的答案完全相同：

J : forall {A : Set} {C : (x y : A) → (x ≡ y) → Set} →
                 (c : ∀ x → C x x refl) →
                 (x y : A) → (p : x ≡ y) → C x y p

，注意到最后一行要求我们提供 x、y 和 p。那为什么

J c x x refl = c x

，（唯一的区别是我去掉了点符号）？或者说，为什么第二个x写的是x而不是y？

这个问题其实我也想过，也有我的解释，但是我不能确定我说的对不对。 J 的类型签名在命题世界，但它的定义在判断世界。我们正在逐步构建命题相等 class 但是所有判断相等的变量可以立即相互重写，当我们使用 J 时我们应该已经判断 x 等于 y（因为我们要提供一个路径）。但是，如果我的推理是完美的，那么回顾那个问题，我们为什么要写

cong : ∀ { a b} { A : Set a }  { B : Set b }
   (f : A → B ) {m  n}  → m ≡ n → f m ≡ f n
cong f {x} {y} p = J {C = \x y p → f x ≡ f y}
                     (\_ → refl)
                     x y p

同样，最后一行提供了 x、y、p 而不是 x、x、p？

Answer 1

当您在 J 的定义 refl 处对 p 进行模式匹配时，其类型从 x ≡ y 细化为 x ≡ x（因为构造函数 refl 的类型是 ∀ {x} -> x ≡ x，即将两个索引设置为 x），这意味着我们可以通过 x ~ y 优化左侧和右侧，这就是为什么模式中的 y 变成 x（或者 .x in Agda to make it explicit that it is an inaccessable pattern），也是为什么 c x : C x x refl 在结果的右侧传递输入 C x y p.

Answer 2

J是归纳公理。因为是公理，所以不需要证明。该公理表示，如果您可以提供 C x x refl 类型的见证，则可以为任何 x 和 y 构造 C x y p，因为 p 是x ≡ y.

的证明

Agda 中的证明并不是真正的 "full" 证明 - 没有可见的步骤为任何 x、y 和 [ 构建 C x y p 的证明=15=]。可见部分仅建立了 C x x refl 可以构造的事实。不可见的部分是 Agda 类型检查器内置的归纳公理，它得出的结论是这就是所需要的。

为什么J公理在给x,y签名时取2 x？

Why J axiom takes 2 x when giving signature of x, y?

equality

agda

type-theory