X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcontribs%2FPREDICATIVE-TOPOLOGY%2Fclass_defs.ma;h=17a53f64f57ec30e013bdb79d514d5002f6b6bef;hb=112afe13b5aef27425d1a0bc9c71a70b491069bf;hp=10a5ae34c8c36ce3618113fe75e8c2024355f83f;hpb=192884dae520029b152a3f69989e51cc8af158ce;p=helm.git

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
index 10a5ae34c..17a53f64f 100644
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
@@ -27,60 +27,25 @@ include "../../library/logic/connectives.ma".
      type in CIC representing the domain of a propositional function
    - We set up a single equality predicate, parametric on the category,
      defined as the reflexive, symmetic, transitive and compatible closure
-     of the csub1 predicate given inside the category. Then we prove the 
+     of the cle1 predicate given inside the category. Then we prove the 
      properties of the equality that usually are axiomatized inside the 
      category structure. This makes categories easier to use
 *) 
 
-record Class: Type \def {
-   class: Type;
-   cin  : class \to Prop;
-   csub1: class \to class \to Prop
-}.
-
-coercion class. 
-
-inductive eq (C:Class) (c1:C): C \to Prop \def
-   | eq_refl:   cin ? c1 \to eq ? c1 c1
-   | eq_sing_r: \forall c2,c3. 
-                eq ? c1 c2 \to cin ? c3 \to csub1 ? c2 c3 \to eq ? c1 c3
-   | eq_sing_l: \forall c2,c3. 
-                eq ? c1 c2 \to cin ? c3 \to csub1 ? c3 c2 \to eq ? c1 c3.
+definition true_f \def \lambda (X:Type). \lambda (_:X). True.
 
-theorem eq_cl: \forall C,c1,c2. eq ? c1 c2 \to cin C c1 \land cin C c2.
-intros; elim H; clear H; clear c2; 
-   [ auto | decompose H2; auto | decompose H2; auto ].
-qed.
+definition false_f \def \lambda (X:Type). \lambda (_:X). False.
 
-theorem eq_trans: \forall C,c2,c1,c3.
-                  eq C c2 c3 \to eq ? c1 c2 \to eq ? c1 c3.
-intros 5; elim H; clear H; clear c3;
-   [ auto 
-   | apply eq_sing_r; [||| apply H4 ]; auto
-   | apply eq_sing_l; [||| apply H4 ]; auto
-   ].
-qed.
-
-theorem eq_conf_rev: \forall C,c2,c1,c3.
-                     eq C c3 c2 \to eq ? c1 c2 \to eq ? c1 c3.
-intros 5; elim H; clear H; clear c2;
-   [ auto 
-   | lapply eq_cl; [ decompose Hletin |||| apply H1 ].
-     apply H2; apply eq_sing_l; [||| apply H4 ]; auto
-   | lapply eq_cl; [ decompose Hletin |||| apply H1 ].
-     apply H2; apply eq_sing_r; [||| apply H4 ]; auto
-   ].
-qed.
+record Class: Type \def {
+   class:> Type;
+   cin: class \to Prop;
+   cle1: class \to class \to Prop
+}.
 
-theorem eq_sym: \forall C,c1,c2. eq C c1 c2 \to eq C c2 c1.
-intros;
-lapply eq_cl; [ decompose Hletin |||| apply H ].
-auto.
-qed.
+inductive cle (C:Class) (c1:C): C \to Prop \def
+   | cle_refl: cin ? c1 \to cle ? c1 c1
+   | ceq_sing: \forall c2,c3. 
+               cle ? c1 c2 \to cin ? c3 \to cle1 ? c2 c3 \to cle ? c1 c3.
 
-theorem eq_conf: \forall C,c2,c1,c3.
-                 eq C c1 c2 \to eq ? c1 c3 \to eq ? c2 c3.
-intros.
-lapply eq_sym; [|||| apply H ].
-apply eq_trans; [| auto | auto ].
-qed.
+inductive ceq (C:Class) (c1:C) (c2:C): Prop \def
+   | ceq_intro: cle ? c1 c2 \to cle ? c2 c1 \to ceq ? c1 c2.