From 583977e3d9e646efcaf5b8e956f0407fd3777236 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 13 Dec 2011 11:12:02 +0000
Subject: [PATCH] Sig in Prop

---
 matita/matita/lib/basics/types.ma | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index bfcf7731f..a6749bb39 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -123,6 +123,12 @@ notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
 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) ⇒
-- 
2.39.2