Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Church encoding of identity types, courtesy of Ben Delaware
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))).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment