predicative subsets started

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
index e4ee22311e194768818e6e9420dc57c3e0e83067..b375c69ada732dd06bc7926a945f3e59baada69b 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
@@ -30,7 +30,7 @@ include "coq.ma".
      of the aceq 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 AC: Type \def {
    ac: Type;

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
index 2fb07bd64d0d1bfc108100f261c221701943abae..0fd99341142e450e3221635223cd126b60ce0cf4 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
@@ -24,7 +24,7 @@ record QD: Type \def {
 }.
 
 coercion qd.
-
+(*
 inductive iall (D:QD) (P:D \to Prop) : Prop \def
    | iall_intro: (\forall (a:D). acin D a \to P a) \to iall D P.
-   
+*)   

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma
new file mode 100644 (file)
index 0000000..579708e
--- /dev/null
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/subsets_defs".
+
+include "qd_defs.ma".
+
+(* SUBSETS
+   - We use predicative subsets coded as propositional functions
+     according to G.Sambin and S.Valentini "Toolbox" 
+*)
+
+definition Subset \def \forall (D:QD). D \to Prop.
+
+alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
+definition stop \def \lambda (D:QD). \lambda (a:(ac (qd D))). True.