Рекурсия для церковного кодирования равенства

Question

Для Церкви, кодирующей 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.

Каков принцип рекурсии equal_rec для следующей церковной кодировки equal равенства?

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

Definition equal_rec (* ... *)

Answer 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.