Using Prop conjuction on Props lowers the universes.

[helm.git] / helm / software / matita / contribs / dama / dama / cprop_connectives.ma

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"