Arend 中相等 Props 的元素是否相等？

问题描述

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

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

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

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

解决方法

是的，你可以证明它，但是你的函数有一个错误：等式（=）只支持一种类型的对象（它被定义为\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