notation "\ll term 19 a, break term 19 b \gg"
with precedence 90 for @{'dependent_pair (λx:?.? x) $a $b}.
-interpretation "dependent pair" 'dependent_pair \eta.c a b = (sigma_intro _ c a b).
+interpretation "dependent pair" 'dependent_pair \eta.c a b = (sigma_intro ? c a b).
-interpretation "sigma" 'Sigma \eta.x = (sigma _ x).
+interpretation "sigma" 'Sigma \eta.x = (sigma ? x).
definition sigmaFst ≝
λT:Type.λf:T → Type.λs:sigma T f.match s with [ sigma_intro x _ ⇒ x ].