next up previous contents
Next: Altenkirch-Streicher Elimination Rule Up: Equality Previous: Paulin-Mohring's Inductive Equality

Martin-Löf's Inductive Equality


This library file gives the definition and rules for Martin-Löf's inductive equality. We cannot use LEGO's inductive type mechanism for this definition because the type of the constructor Eqr does not conform to Luo's schema for inductive types, so the definition is done by hand. Loading this file causes the LEGO tactic Qrepl to be configured for this inductive equality.

     ** Mark "lib_ML_eq" **

Eq : {t|SET}t->t->Prop
Eqr : {t|SET}{x:t}Eq x x
Eq_elim : {t|SET}{P:{x,y:t}(Eq x y)->TYPE}
     ({x:t}P x x (Eqr x))->{x,y:t}{p:Eq x y}P x y p
Eq_refl = ... : {t|SET}refl (Eq|t)
Eq_subst = ... : {t|SET}{m,n|t}(Eq m n)->{P:t->TYPE_minus1}(P m)->P n
Eq_sym = ... : {t|SET}sym (Eq|t)
Eq_trans = ... : {t|SET}trans (Eq|t)
Eq_resp = ... : {A,B|SET}{f:A->B}respect f Eq
Eq_resp2 = ... : {A,B,C|SET}{r:A->B->C}respect2 r Eq

Fri May 24 19:01:27 BST 1996