Using Prop conjuction on Props lowers the universes.

SigT instead of ExT

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index 09b9a6c67fb189d61070b5adf27f5f131bf5a547..f9de36d1fa4a33fef91473d4f11d43bc86c0c7fd 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -62,6 +62,26 @@ interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t).
 inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.
 
+record sigT (A:Type) (P:A→CProp) : Type ≝ {
+  fstT:A;
+  sndT:P fstT
+}.
+  
+interpretation "sigT \fst" 'pi1 = (fstT _ _).
+interpretation "sigT \fst" 'pi1a x = (fstT _ _ x).
+interpretation "sigT \fst" 'pi1b x y = (fstT _ _ x y).
+interpretation "sigT \snd" 'pi2 = (sndT _ _).
+interpretation "sigT \snd" 'pi2a x = (sndT _ _ x).
+interpretation "sigT \snd" 'pi2b x y = (sndT _ _ x y).
+
+notation "\ll term 19 a, break term 19 b \gg" 
+with precedence 90 for @{'dependent_pair $a $b}.
+interpretation "dependent pair" 'dependent_pair a b = 
+  (ex_introT _ _ a b).
+
+interpretation "dependent set" 'dependent_pair a b = 
+  (mk_sigT _ _ a b).
+
 interpretation "CProp exists" 'exists \eta.x = (exT _ x).
 
 notation "\ll term 19 a, break term 19 b \gg" 

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index e1fbd0a5a75cac9f840d207833e3319214680224..6daebfa0cde944051d1b03fe7d2ddd35cd415d3e 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -38,7 +38,7 @@ cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7;
 intro H2; cases (H10 ? H2);
 cases (H (w1+j)); apply (H11 H7);
 qed.   
-     
+          
 (* Theorem 3.10 *)
 theorem lebesgue_oc:
   ∀C:ordered_uniform_space.
@@ -65,10 +65,10 @@ split;
     [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
     |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
 |2: intros 3 (h);
-    letin Xi ≝ (⌊n,≪xi n,Hxi n≫⌋);
-    letin Yi ≝ (⌊n,≪yi n,Hyi n≫⌋);
-    letin Ai ≝ (⌊n,≪a n,H1 n≫⌋);
-    apply (sandwich {[l,u]} ≪?,h≫ Xi Yi Ai); try assumption;
+    letin Xi ≝ (⌊n,mk_sigT ?? (xi n) (Hxi n)⌋);
+    letin Yi ≝ (⌊n,mk_sigT ?? (yi n) (Hyi n)⌋);
+    letin Ai ≝ (⌊n,mk_sigT ?? (a n) (H1 n)⌋);
+    apply (sandwich {[l,u]} (mk_sigT ?? x h) Xi Yi Ai); try assumption;
     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
         [apply (H5 0);|apply (H7 0)]
     |2: cases (H l u Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
@@ -108,10 +108,10 @@ split;
 |2: intros 3;
     lapply (uparrow_upperlocated ? xi x Hx)as Ux;
     lapply (downarrow_lowerlocated ? yi x Hy)as Uy;
-    letin Xi ≝ (⌊n,≪xi n,Hxi n≫⌋);
-    letin Yi ≝ (⌊n,≪yi n,Hyi n≫⌋);
-    letin Ai ≝ (⌊n,≪a n,H1 n≫⌋);
-    apply (sandwich {[l,u]} ≪x,h≫ Xi Yi Ai); try assumption;
+    letin Xi ≝ (⌊n,mk_sigT ?? (xi n) (Hxi n)⌋);
+    letin Yi ≝ (⌊n,mk_sigT ?? (yi n) (Hyi n)⌋);
+    letin Ai ≝ (⌊n,mk_sigT ?? (a n) (H1 n)⌋);
+    apply (sandwich {[l,u]} (mk_sigT ?? x h) Xi Yi Ai); try assumption;
     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
         [apply (H5 0);|apply (H7 0)]
     |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx);

diff --git a/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma b/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma
index 412b5407dd0e6816c7b7c5d78f9e41725898c61b..01890a416346c9afa546d5c9d7020fa4569f1234 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma
+++ b/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma
@@ -21,7 +21,7 @@ intro C; apply (mk_uniform_space C);
     alias symbol "pi2" = "pair pi2".
     alias symbol "pi1" = "pair pi1".
     alias symbol "and" = "logical and".
-    apply (∃_:unit.∀n:C square.(\fst n ≈ \snd n → P n) ∧ (P n → \fst n ≈ \snd n)); 
+    apply (∃d:unit.∀n:C square.(\fst n ≈ \snd n → P n) ∧ (P n → \fst n ≈ \snd n)); 
 |2: intros 4 (U H x Hx); simplify in Hx;
     cases H (_ H1); cases (H1 x); apply H2; apply Hx;
 |3: intros; cases H (_ PU); cases H1 (_ PV); 

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index bf0260a510ac775fede207a1760f26e371e36daf..2ffda533ac61a612f850eb103d3b2e6e81b1473d 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -53,8 +53,8 @@ qed.
 
 coercion cic:/matita/dama/ordered_uniform/segment_square_of_ordered_set_square.con 0 2.
 
-alias symbol "pi1" (instance 4) = "exT \fst".
-alias symbol "pi1" (instance 2) = "exT \fst".
+alias symbol "pi1" (instance 4) = "sigT \fst".
+alias symbol "pi1" (instance 2) = "sigT \fst".
 lemma ordered_set_square_of_segment_square : 
  ∀O:ordered_set.∀u,v:O.{[u,v]} square → O square ≝ 
   λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈\fst(\fst b),\fst(\snd b)〉.
@@ -100,6 +100,8 @@ notation < "x \sub \neq" with precedence 91 for @{'bsss $x}.
 interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
 
 alias symbol "square" (instance 7) = "ordered set square".
+alias symbol "square" (instance 13) = "ordered set square".
+alias symbol "dependent_pair" = "dependent set".
 lemma ss_of_bs: 
  ∀O:ordered_set.∀u,v:O.
   ∀b:O square.\fst b ∈ [u,v] → \snd b ∈ [u,v] → {[u,v]} square ≝ 
@@ -159,7 +161,7 @@ interpretation "Ordered uniform space segment" 'segment_set a b =
  (segment_ordered_uniform_space _ a b).
 
 (* Lemma 3.2 *)
-alias symbol "pi1" = "exT \fst".
+alias symbol "pi1" = "sigT \fst".
 lemma restric_uniform_convergence:
  ∀O:ordered_uniform_space.∀l,u:O.
   ∀x:{[l,u]}.

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index a492c8f3299e8255c0b86be2605972da857b3310..b4430d6edff7d4daaa16eaa9a899786a4dea2498 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -227,7 +227,6 @@ notation > "a 'order_converges' x" non associative with precedence 45
 interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).   
     
 (* Definition 2.8 *)
-alias symbol "and" = "constructive and".
 definition segment ≝ λO:ordered_set.λa,b:O.λx:O.(x ≤ b) ∧ (a ≤ x).
 
 notation "[a,b]" left associative with precedence 70 for @{'segment $a $b}.
@@ -239,7 +238,7 @@ interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).
 
 lemma segment_ordered_set: 
   ∀O:ordered_set.∀u,v:O.ordered_set.
-intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
+intros (O u v); apply (mk_ordered_set (sigT ? (λx.x ∈ [u,v])));
 [1: intros (x y); apply (\fst x ≰ \fst y);
 |2: intro x; cases x; simplify; apply os_coreflexive;
 |3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]