首先,我已经研究了几种相关材料,包括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的定义中在reflJ上对模式进行匹配时,其类型将从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的右侧传递。

09-11 03:26
查看更多