Church encoding of identity types, courtesy of Ben Delaware

church_eq.v

Inductive eq_fun (A : Type) (x : A) (B : A -> Prop)  : A -> Prop :=
| eq_refl' : eq_fun x B x.

(* Indexed Mendler Algebra *)
Definition iMAlgebra {I : Type} (F : (I -> Prop) -> I -> Prop) (A : I -> Prop) :=
forall i (R : I -> Prop), (forall i, R i -> A i) -> F R i -> A i.

(* Type of initial Mendler Algebra objects *)
Definition iFix {I : Type} (F : (I -> Prop) -> I -> Prop) (i : I) : Prop :=
forall (A : I -> Prop), iMAlgebra F A -> A i.

Definition ifold_malgebra {I : Type} (F : (I -> Prop) -> I -> Prop) :
forall (A : I -> Prop) (f : iMAlgebra F A) (i : I),
  iFix F i -> A i := fun A f i e => e A f.

(* Type of Church Encodings of eq *)
Definition church_eq (A : Type) (a : A) : A -> Prop := iFix (@eq_fun A a).

(* Induction principle for eq *)
Definition church_eq_ind (A : Type) (x : A) (P : A -> Prop)
         (H : P x) (y : A)
: church_eq x y -> P y.
intros; apply ifold_malgebra with (F := @eq_fun A x) (i := y); eauto.
unfold iMAlgebra; intros; destruct H2; simpl in *; eauto.
Qed.

(* Constructors of church-encoded eqs *)
Definition in_ti {I : Type} {F} : forall i : I, F (iFix F) i -> iFix F i :=
fun i F_e A f => f _ _ (ifold_malgebra f) F_e.
Definition eq_refl'' (A : Type) (a : A) : @eq A a a
:= in_ti a (eq_refl' a (iFix (eq_fun a))).