X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcontribs%2FPREDICATIVE-TOPOLOGY%2Fclass_defs.ma;h=ba119561956e16c043898fe57df069a1530385a6;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;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..ba1195619 100644
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
@@ -27,60 +27,26 @@ 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
 *) 
 
+definition true_f \def \lambda (X:Type). \lambda (_:X). True.
+
+definition false_f \def \lambda (X:Type). \lambda (_:X). False.
+
 record Class: Type \def {
    class: Type;
    cin  : class \to Prop;
-   csub1: class \to class \to Prop
+   cle1 : 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.
-
-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.
-
-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.
-
-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.
-
-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): C \to Prop \def
+   | ceq_refl:   cin ? c1 \to ceq ? c1 c1
+   | ceq_sing_r: \forall c2,c3. 
+                ceq ? c1 c2 \to cin ? c3 \to cle1 ? c2 c3 \to ceq ? c1 c3
+   | ceq_sing_l: \forall c2,c3. 
+                ceq ? c1 c2 \to cin ? c3 \to cle1 ? c3 c2 \to ceq ? c1 c3.