next up previous contents
Next: Setoids Up: Equality Previous: Altenkirch-Streicher Elimination Rule

Theorems about Equality

All of the above notions of equality are reflexive and substitutive. We can thus derive symmetry and transitivity. Furthermore, equality respects function applications i.e.,

\frac{a=b}{{f(a)}={f(b)}} \tag{\tt Eq\_resp}\\ \frac{a_1=b_1\quad a_2=b_2}{{f(a_1)(a_2)}={f(b_1)(b_2)}}\tag{\tt Eq\_resp2}\end{gather*}

 ** Module lib_eq_basics Imports lib_eq
  injective = ... : {S|Type}{T|Type}(S->T)->Prop
  Eq_sym = ... : {t|Type}sym (Eq|t)
  Eq_trans = ... : {t|Type}trans (Eq|t)
  Eq_resp = ... : {A|Type}{B|Type}{f:A->B}respect f Eq
 ** Config Equality Eq Eq_refl Eq_subst
 ** Config Qrepl Eq Eq_subst Eq_sym
 ** Config Qrepl Eq Eq_subst Eq_sym
  Eq_resp2 = ... : {A|Type}{B|Type}{C|Type}{r:A->B->C}respect2 r Eq

Conor McBride