Cool: only 8 universes in use.

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / categories.ma

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;