Recursion for Church encoding of equality

Question

For the Church encoding N of positive integers, one can define a recursion principle 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.
In environment
z : N
s : N -> N
n : N
The term "N" has type "Type@{N.u0}"
while it is expected to have type "Type@{N.u1}"
(universe inconsistency: Cannot enforce N.u0 <=
N.u1 because N.u1 < N.u0).

What is the recursion principle equal_rec for the following Church encoding equal of equality?

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

Definition equal_rec (* ... *)

Answer

Like the case of natural numbers, the recursion principle is simply an eta expansion:

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.

Q: This looks pretty useless, isn't it? Can it be used to prove symmetry, transitivity or congruence of equality?

A: It cannot, because of universe issues. But you can replace Type by Prop everywhere, and it should work.