+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).
+