X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fproperties%2Frelations.ma;h=581208d9afb8fcf567a4f931b8fe16f6899edeb2;hb=6678a28314d8878bb46d5de7b1060628f4930242;hp=619ab7807719d48a788b3cda5bed1fcdb500f1aa;hpb=5bc1672a263663a241ba8b0efde692b246761b6a;p=helm.git

diff --git a/helm/software/matita/nlibrary/properties/relations.ma b/helm/software/matita/nlibrary/properties/relations.ma
index 619ab7807..581208d9a 100644
--- a/helm/software/matita/nlibrary/properties/relations.ma
+++ b/helm/software/matita/nlibrary/properties/relations.ma
@@ -14,6 +14,13 @@
 
 include "logic/pts.ma".
 
-ndefinition reflexive ≝ λT:Type.λP:T → T → CProp. ∀x.P x x.
-ndefinition symmetric ≝ λT:Type.λP:T → T → CProp. ∀x,y.P x y → P y x.
-ndefinition transitive ≝ λT:Type.λP:T → T → CProp. ∀z,x,y. P x z → P z y → P x y.
+ndefinition reflexive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x.P x x.
+ndefinition symmetric ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x,y.P x y → P y x.
+ndefinition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z → P z y → P x y.
+
+nrecord equivalence_relation (A:Type[0]) : Type[1] ≝
+ { eq_rel:2> A → A → CProp[0];
+   refl: reflexive ? eq_rel;
+   sym: symmetric ? eq_rel;
+   trans: transitive ? eq_rel
+ }.