tlt_defs: notation updated

ac_defs : PREDICATIVE TOPOLOGY: firs attempt

diff --git a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
index 1d5f73f17b01283028da43a233572ae7e6c6bb46..390c067cc15823721e09fdf7f81653f2f1e2a9c1 100644 (file)
--- a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
+++ b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
@@ -44,6 +44,10 @@ let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T A N) on t : nat \def
       | (TGRef y n)     \Rightarrow O
   ].
 
-definition weight : \forall A,N. T A N \to nat \def \lambda A,N.(weight_map A N (\lambda _.O)).
+definition weight: \forall A,N. T A N \to nat \def 
+   \lambda A,N. 
+   (weight_map A N (\lambda _.O)).
 
-definition tlt : \forall A,N. T A N \to T A N \to Prop \def \lambda A,N. \lambda t1,t2. weight A N t1 < weight A N t2.
+definition tlt: \forall A,N. T A N \to T A N \to Prop \def 
+   \lambda A,N,t1,t2. 
+   weight A N t1 < weight A N t2.

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
new file mode 100644 (file)
index 0000000..89e67c2
--- /dev/null
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ac_defs".
+
+(* Project started Wed Oct 12, 2005 ***************************************)
+
+
+
+(* ACZEL CATEGORIES:                                                      *)
+(* 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     *)
+(* domain of a propositional function (ie a subset in the predicative     *)
+(* setting) as a quantification domain and therefore as a category, but   *)
+(* there is no type in CIC representing the domain of a propositional     *)
+(* function                                                               *)
+
+record AC: Type \def {
+   ac: Type;
+   acin: ac \to Prop;
+   aceq: ac \to ac \to Prop
+}.
+
+definition a \def \lambda A. ac A.
+
+coercion a. 
+
+inductive eq (A:AC) : ac A \to ac A \to Prop \def
+   | eq_refl: \forall a. acin ? a \to eq A a a.