| #a #H #p normalize @p @refl
] qed.
+(* dependent pair *)
+record DPair (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
+ dpi1:> A
+ ; dpi2: f dpi1
+ }.
+
+interpretation "DPair" 'dpair x = (DPair ? x).
+
+interpretation "mk_DPair" 'mk_DPair x y = (mk_DPair ?? x y).
+
(* sigma *)
-record Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
+record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
pi1: A
; pi2: f pi1
}.
interpretation "Sigma" 'sigma x = (Sig ? x).
-notation "hvbox(« term 19 a, break term 19 b»)"
-with precedence 90 for @{ 'dp $a $b }.
-
interpretation "mk_Sig" 'dp x y = (mk_Sig ?? x y).
+lemma sub_pi2 : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' (pi1 … x).
+#A #P #P' #H1 * #x #H2 @H1 @H2
+qed.
+
(* Prod *)
record Prod (A,B:Type[0]) : Type[0] ≝ {
for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
λ${ident E}.$s ] (refl ? $t) }.
-(* Prop sigma *)
-record PSig (A:Type[0]) (P:A→Prop) : Type[0] ≝
- {elem:>A; eproof: P elem}.
-
-interpretation "subset type" 'sigma x = (PSig ? x).
-
notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp 'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
with precedence 10
for @{ match $t return λ${ident k}:$X.$eq $T $k $t → ? with [ mk_Prod (${ident x}:$U) (${ident y}:$W) ⇒