Cool: only 8 universes in use.

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 3ee3915074dd3db68941cbe032c9b4bcb8f3fa40..75ca005c64b9ce03d24b487c22d103ee97499492 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -26,9 +26,9 @@ record setoid : Type1 ≝
    eq: equivalence_relation carr
  }.
 
-definition reflexive1 ≝ λA:Type1.λR:A→A→CProp1.∀x:A.R x x.
-definition symmetric1 ≝ λC:Type1.λlt:C→C→CProp1. ∀x,y:C.lt x y → lt y x.
-definition transitive1 ≝ λA:Type1.λR:A→A→CProp1.∀x,y,z:A.R x y → R y z → R x z.
+definition reflexive1: ∀A:Type1.∀R:A→A→CProp1.CProp1 ≝ λA:Type1.λR:A→A→CProp1.∀x:A.R x x.
+definition symmetric1: ∀A:Type1.∀R:A→A→CProp1.CProp1 ≝ λC:Type1.λlt:C→C→CProp1. ∀x,y:C.lt x y → lt y x.
+definition transitive1: ∀A:Type1.∀R:A→A→CProp1.CProp1 ≝ λA:Type1.λR:A→A→CProp1.∀x,y,z:A.R x y → R y z → R x z.
 
 record equivalence_relation1 (A:Type1) : Type2 ≝
  { eq_rel1:2> A → A → CProp1;
@@ -57,9 +57,9 @@ qed.
 (* questa coercion e' necessaria per problemi di unificazione *)
 coercion setoid1_of_setoid.
 
-definition reflexive2 ≝ λA:Type2.λR:A→A→CProp2.∀x:A.R x x.
-definition symmetric2 ≝ λC:Type2.λlt:C→C→CProp2. ∀x,y:C.lt x y → lt y x.
-definition transitive2 ≝ λA:Type2.λR:A→A→CProp2.∀x,y,z:A.R x y → R y z → R x z.
+definition reflexive2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λA:Type2.λR:A→A→CProp2.∀x:A.R x x.
+definition symmetric2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λC:Type2.λlt:C→C→CProp2. ∀x,y:C.lt x y → lt y x.
+definition transitive2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λA:Type2.λR:A→A→CProp2.∀x,y,z:A.R x y → R y z → R x z.
 
 record equivalence_relation2 (A:Type2) : Type3 ≝
  { eq_rel2:2> A → A → CProp2;

diff --git a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
index 36616b2f8fc74dc10a8f53170abe94b4b1915229..4855bf658cb6403081a39c4f04b2f23de5ba7ab9 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
@@ -140,16 +140,18 @@ definition Not : CProp0 → Prop ≝ λx:CProp.x → False.
 
 interpretation "constructive not" 'not x = (Not x).
   
-definition cotransitive ≝
+definition cotransitive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝
  λC:Type0.λlt:C→C→CProp0.∀x,y,z:C. lt x y → lt x z ∨ lt z y. 
 
-definition coreflexive ≝ λC:Type0.λlt:C→C→CProp0. ∀x:C. ¬ (lt x x).
+definition coreflexive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝
+ λC:Type0.λlt:C→C→CProp0. ∀x:C. ¬ (lt x x).
 
-definition symmetric ≝ λC:Type0.λlt:C→C→CProp0. ∀x,y:C.lt x y → lt y x.
+definition symmetric: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝
+ λC:Type0.λlt:C→C→CProp0. ∀x,y:C.lt x y → lt y x.
 
-definition antisymmetric ≝ λA:Type0.λR:A→A→CProp0.λeq:A→A→Prop.∀x:A.∀y:A.R x y→R y x→eq x y.
+definition antisymmetric: ∀A:Type0. ∀R:A→A→CProp0. ∀eq:A→A→Prop.CProp0 ≝
+ λA:Type0.λR:A→A→CProp0.λeq:A→A→Prop.∀x:A.∀y:A.R x y→R y x→eq x y.
 
-definition reflexive ≝ λA:Type0.λR:A→A→CProp0.∀x:A.R x x.
+definition reflexive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x:A.R x x.
 
-definition transitive ≝ λA:Type0.λR:A→A→CProp0.∀x,y,z:A.R x y → R y z → R x z.
- 
+definition transitive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x,y,z:A.R x y → R y z → R x z.
\ No newline at end of file

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index 6be19d92c31ac4518d402650c362e85dc4b3fd9b..10f50358103e04fce97ba83db0c3340c6de9f63f 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -168,7 +168,7 @@ definition hint5: OAlgebra → objs2 SET1.
 qed.
 coercion hint5.
 
-record ORelation (P,Q : OAlgebra) : Type ≝ {
+record ORelation (P,Q : OAlgebra) : Type2 ≝ {
   or_f_ : P ⇒ Q;
   or_f_minus_star_ : P ⇒ Q;
   or_f_star_ : Q ⇒ P;