在 Arend 中相等道具的元素是否相等？

【问题标题】：Are elements of equal Props equal in Arend?在 Arend 中相等道具的元素是否相等？
【发布时间】：2021-06-09 09:47:52
【问题描述】：

我能证明相等的 Props 的两个元素相等吗？这似乎是合乎逻辑的，因为一个 Prop 中的所有元素都是相等的，所以每个 Prop 都有一个唯一的元素，如果两个 Prop 也相等，那么它们的元素是相同的。但是我不明白，如何在 arend 中表达这个想法。

更准确地说，我想要这样的功能：

\func eqProp
  {A B : \Prop} 
  (A=B : A = B)
  (a : A) (b : B)
  : a = b

我已阅读有关相等性的文档，但它对我没有帮助，我无法从 Props 相等性转移到元素相等性。

【问题讨论】：

标签： proof

【解决方案1】：

是的，你可以证明它，但是你的函数有一个错误：相等（=）只支持一种类型的对象（它被定义为\func \infix 1 = {A : \Type} (a a' : A) => Path (\lam _ => A) a a'）。虽然A 等于B，但您需要Path (\lam i => A=B @ i) a b 而不是a = b，然后您可以使用arend 库中的函数，这正是您想要的：

\func eqProp
{A B : \Prop}
(A=B : A = B)
(a : A) (b : B)
: Path (\lam i => A=B @ i) a b
=> pathInProp (\lam i => A=B @ i) a b

【讨论】：