From: Ferruccio Guidi Date: Thu, 13 Oct 2005 14:22:08 +0000 (+0000) Subject: more comments added X-Git-Tag: V_0_7_2_3~213 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a6378eaf623f898f8cbea4381a1ea7132146c8c2;p=helm.git more comments added --- diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma index 89e67c2f9..f2cd4860f 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma @@ -18,14 +18,19 @@ set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/ac_defs". -(* 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 *) +(* 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 predicative subset) as a + quantification domain and therefore as a category, but there is no + 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 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; @@ -33,9 +38,7 @@ record AC: Type \def { aceq: ac \to ac \to Prop }. -definition a \def \lambda A. ac A. +coercion ac. -coercion a. - -inductive eq (A:AC) : ac A \to ac A \to Prop \def +inductive eq (A:AC) : A \to A \to Prop \def | eq_refl: \forall a. acin ? a \to eq A a a.