首先,我已经研究了几种相关材料,包括HoTT书和this question。
但是我仍然很困惑,我希望得到一个解释,该解释脱离了Agda,但直接脱离了其数学公式。删除点符号后,J axiom会这样说,其类型签名与我上面提到的问题的答案完全相同:
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的类型签名在命题世界中,但其定义在判断世界中。我们正在逐步构建命题相等类,但是所有判断相等变量都可以立即相互重写,并且当我们使用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?
最佳答案
在p
的定义中在refl
的J
上对模式进行匹配时,其类型将从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
的右侧传递。