\ / GNU General Public License Version 2
V_______________________________________________________________ *)
+include "basics/core_notation/pair_2.ma".
include "basics/logic.ma".
(* void *)
(* sigma *)
record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
- pi1: A
+ pi1: A (* not a coercion due to problems with Cerco *)
; pi2: f pi1
}.
#A #P #P' #H1 * #x #H2 @H1 @H2
qed.
+lemma inj_mk_Sig: ∀A,P.∀x. x = mk_Sig A P (pi1 A P x) (pi2 A P x).
+#A #P #x cases x //
+qed-.
(* Prod *)
record Prod (A,B:Type[0]) : Type[0] ≝ {
match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
λ${ident E}.$s ] ] (refl ? $t) }.
-notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp 'as' \nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
with precedence 10
-for @{ match $t return λ${ident x}.$eq $T $x $t → $U with [ mk_Prod (${fresh xy}:$V) (${ident z}:$Z) ⇒
- match ${fresh xy} return λ${ident y}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
+for @{ match $t return λ${ident k}:$X.$eq $T $k $t → $U with [ mk_Prod (${ident xy}:$V) (${ident z}:$Z) ⇒
+ match $xy return λ${ident a}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
λ${ident E}:$J.$s ] ] ($refl $A $t) }.
notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"