Church编码平等的递归

【问题标题】：Recursion for Church encoding of equalityChurch编码平等的递归
【发布时间】：2019-03-10 15:25:05
【问题描述】：

对于正整数的Church编码N，可以定义一个递归原理nat_rec：

Definition N : Type :=
forall (X:Type), X->(X->X)->X.

Definition nat_rec (z:N)(s:N->N)(n:N) : N :=
n N z s.

以下 Church 编码 equal 的递归原理是什么 equal_rec 相等？

Definition equal (x:A) : A->Type :=
fun x' => forall (P:A->Type), P x -> P x'.

Definition equal_rec (* ... *)

【问题讨论】：

标签： recursion coq equality church-encoding

【解决方案1】：

与自然数的情况一样，递归原理只是一个 eta 扩展：

Definition equal (A:Type) (x:A) : A->Type :=
  fun x' => forall (P:A->Type), P x -> P x'.

Definition equal_rec (A:Type) (x y : A) (e : equal x y) (P : A -> Type) : P x -> P y :=
  e P.

【讨论】：

这看起来没什么用，不是吗？它可以用来证明等式的对称性、传递性或同余性吗？
它不能，因为宇宙问题。但是您可以在任何地方用Prop 替换Type，它应该可以工作。