X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Flimits%2FClass%2Fdefs.ma;h=429a6a17fc128b4371c9fe4b5c379d124eb2122c;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=bbb071b5003435ccf672e4c1ea8e515a698218d2;hpb=bf8fe5331d6e6d2dfe955efa54b1ffdafaae8429;p=helm.git

diff --git a/helm/software/matita/contribs/limits/Class/defs.ma b/helm/software/matita/contribs/limits/Class/defs.ma
index bbb071b50..429a6a17f 100644
--- a/helm/software/matita/contribs/limits/Class/defs.ma
+++ b/helm/software/matita/contribs/limits/Class/defs.ma
@@ -14,7 +14,7 @@
 
 include "preamble.ma".
 
-(* ACZEL CATEGORIES
+(* CLASSES:
    - We use typoids with a compatible membership relation
    - The category is intended to be the domain of the membership relation
    - The membership relation is necessary because we need to regard the
@@ -27,19 +27,43 @@ include "preamble.ma".
 *) 
 
 record Class: Type ≝ {
-   class:> Type;
-   cin: class → Prop;
-   ces: class → class \to Prop
+   class     :> Type;
+   cin       :  class → Prop;
+   ces       :  class → class → Prop;
+   ces_cin_fw:  ∀c1,c2. cin c1 → ces c1 c2 → cin c2;
+   ces_cin_bw:  ∀c1,c2. cin c1 → ces c2 c1 → cin c2
 }.
 
-(* default inhabitance predicates *)
-definition true_f ≝ λ(X:Type). λ(_:X). True.
-definition false_f ≝ λ(X:Type). λ(_:X). False.
+(* equality predicate *******************************************************)
 
-(* equality predicate *)
 inductive ceq (C:Class): class C → class C → Prop ≝
-   | ceq_refl : ∀c. cin ? c → ceq ? c c
-   | ceq_trans: ∀c1,c,c2. cin ? c1 → ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
-   | ceq_conf : ∀c1,c,c2. cin ? c1 → ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
+   | ceq_refl : ∀c. ceq ? c c
+   | ceq_trans: ∀c1,c,c2. ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
+   | ceq_conf : ∀c1,c,c2. ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
 .
 
+(* default inhabitance predicates *******************************************)
+
+definition true_f ≝ λX:Type. λ_:X. True.
+
+definition false_f ≝ λX:Type. λ_:X. False.
+
+(* default foreward compatibilities *****************************************)
+
+theorem const_fw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x1 x2 → A.
+intros; autobatch.
+qed.
+
+definition true_fw ≝ const_fw True.
+
+definition false_fw ≝ const_fw False.
+
+(* default backward compatibilities *****************************************)
+
+theorem const_bw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x2 x1 → A.
+intros; autobatch.
+qed.
+
+definition true_bw ≝ const_bw True.
+
+definition false_bw ≝ const_bw False.