From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 15 Dec 2008 13:50:17 +0000 (+0000)
Subject: use named types to force some constraints asap
X-Git-Tag: make_still_working~4393
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e7cbfc078d4738277cf4a730c9407fc140bc029b;p=helm.git

use named types to force some constraints asap
---

diff --git a/helm/software/matita/library/datatypes/categories.ma b/helm/software/matita/library/datatypes/categories.ma
index 692f977df..6dac9b044 100644
--- a/helm/software/matita/library/datatypes/categories.ma
+++ b/helm/software/matita/library/datatypes/categories.ma
@@ -14,6 +14,12 @@
 
 include "logic/cprop_connectives.ma".
 
+definition Type0 := Type.
+definition Type1 := Type.
+definition Type2 := Type.
+definition Type0_lt_Type1 := (Type0 : Type1).
+definition Type1_lt_Type2 := (Type1 : Type2).
+
 record equivalence_relation (A:Type) : Type ≝
  { eq_rel:2> A → A → CProp;
    refl: reflexive ? eq_rel;
@@ -21,7 +27,7 @@ record equivalence_relation (A:Type) : Type ≝
    trans: transitive ? eq_rel
  }.
 
-record setoid : Type ≝
+record setoid : Type1 ≝
  { carr:> Type;
    eq: equivalence_relation carr
  }.
@@ -30,7 +36,7 @@ definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
 definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
 definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
 
-record equivalence_relation1 (A:Type) : Type ≝
+record equivalence_relation1 (A:Type) : Type2 ≝
  { eq_rel1:2> A → A → CProp;
    refl1: reflexive1 ? eq_rel1;
    sym1: symmetric1 ? eq_rel1;
@@ -82,17 +88,24 @@ notation ".= r" with precedence 50 for @{'trans $r}.
 interpretation "trans1" 'trans r = (trans1 _____ r).
 interpretation "trans" 'trans r = (trans _____ r).
 
-record unary_morphism (A,B: setoid1) : Type ≝
+(*
+record unary_morphism0 (A,B: setoid) : Type0 ≝
+ { fun_0:1> A → B;
+   prop_0: ∀a,a'. eq ? a a' → eq ? (fun_0 a) (fun_0 a')
+ }.
+*)
+
+record unary_morphism (A,B: setoid1) : Type0 ≝
  { fun_1:1> A → B;
    prop_1: ∀a,a'. eq1 ? a a' → eq1 ? (fun_1 a) (fun_1 a')
  }.
 
-record binary_morphism (A,B,C:setoid) : Type ≝
+record binary_morphism (A,B,C:setoid) : Type0 ≝
  { fun:2> A → B → C;
    prop: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun a b) (fun a' b')
  }.
 
-record binary_morphism1 (A,B,C:setoid1) : Type ≝
+record binary_morphism1 (A,B,C:setoid1) : Type0 ≝
  { fun1:2> A → B → C;
    prop1: ∀a,a',b,b'. eq1 ? a a' → eq1 ? b b' → eq1 ? (fun1 a b) (fun1 a' b')
  }.
@@ -104,6 +117,7 @@ notation "† c" with precedence 90 for @{'prop1 $c }.
 notation "l ‡ r" with precedence 90 for @{'prop $l $r }.
 notation "#" with precedence 90 for @{'refl}.
 interpretation "prop_1" 'prop1 c = (prop_1 _____ c).
+(* interpretation "prop_0" 'prop1 c = (prop_0 _____ c). *)
 interpretation "prop1" 'prop l r = (prop1 ________ l r).
 interpretation "prop" 'prop l r = (prop ________ l r).
 interpretation "refl1" 'refl = (refl1 ___).
@@ -174,7 +188,7 @@ definition eq_morphism: ∀S:setoid. binary_morphism S S CPROP.
 qed.
 *)
 
-record category : Type ≝
+record category : Type1 ≝
  { objs:> Type;
    arrows: objs → objs → setoid;
    id: ∀o:objs. arrows o o;
@@ -185,7 +199,7 @@ record category : Type ≝
    id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
  }.
 
-record category1 : Type ≝
+record category1 : Type2 ≝
  { objs1:> Type;
    arrows1: objs1 → objs1 → setoid1;
    id1: ∀o:objs1. arrows1 o o;
diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index 3e3d2d343..c06799274 100644
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -16,7 +16,7 @@ technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic
 nat/div_and_mod_diseq.ma nat/lt_arith.ma
 logic/cprop_connectives.ma logic/connectives.ma
 algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma
-formal_topology/saturations_reductions.ma datatypes/subsets.ma
+formal_topology/saturations_reductions.ma datatypes/subsets.ma formal_topology/relations.ma
 nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
 Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma
 nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma
@@ -35,6 +35,7 @@ didactic/exercises/duality.ma nat/minus.ma
 nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma
 dama/supremum.ma dama/nat_ordered_set.ma dama/sequence.ma datatypes/constructors.ma nat/plus.ma
 nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
+didactic/exercises/natural_deduction1.ma didactic/support/natural_deduction.ma
 nat/times.ma nat/plus.ma
 nat/chebyshev_thm.ma nat/neper.ma
 Z/z.ma datatypes/bool.ma nat/nat.ma
@@ -120,6 +121,7 @@ higher_order_defs/functions.ma logic/equality.ma
 Q/fraction/numerator_denominator.ma Q/fraction/finv.ma
 datatypes/constructors.ma logic/equality.ma
 nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma
+didactic/exercises/natural_deduction_theories.ma didactic/support/natural_deduction.ma nat/plus.ma
 nat/plus.ma nat/nat.ma
 Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma
 dama/sequence.ma nat/nat.ma
diff --git a/helm/software/matita/library/formal_topology/saturations_reductions.ma b/helm/software/matita/library/formal_topology/saturations_reductions.ma
index d87ea9e1f..0582bf0b1 100644
--- a/helm/software/matita/library/formal_topology/saturations_reductions.ma
+++ b/helm/software/matita/library/formal_topology/saturations_reductions.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "datatypes/subsets.ma".
+include "formal_topology/relations.ma".
 
 definition is_saturation ≝
  λC:REL.λA:unary_morphism (Ω \sup C) (Ω \sup C).