From 9009ddf4261bbf489874c4619a8c0397eb3f989d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 3 Apr 2017 15:14:17 -0400 Subject: Split off liftn_sig, add lift{3,4}_sig --- src/Util/Sigma.v | 19 ------------------- 1 file changed, 19 deletions(-) (limited to 'src/Util/Sigma.v') diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index 693b8ef00..1c30219b7 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -211,25 +211,6 @@ Section ex. Defined. End ex. -(* Lift foralls out of sig proofs *) -Definition lift1_sig {A C} (P:A->C->Prop) - (op_sig : forall (a:A), {c | P a c}) : - { op : A -> C | forall (a:A), P a (op a) } - := exist - (fun op => forall a, P a (op a)) - (fun a => proj1_sig (op_sig a)) - (fun a => proj2_sig (op_sig a)) -. - -(* Lift foralls out of sig proofs *) -Definition lift2_sig {A B C} (P:A->B->C->Prop) - (op_sig : forall (a:A) (b:B), {c | P a b c}) : - { op : A -> B -> C | forall (a:A) (b:B), P a b (op a b) } - := exist - (fun op => forall a b, P a b (op a b)) - (fun a b => proj1_sig (op_sig a b)) - (fun a b => proj2_sig (op_sig a b)). - Definition projT2_map {A P Q} (f : forall a, P a -> Q a) (x : @sigT A P) : @sigT A Q := let 'existT a p := x in existT Q a (f a p). Definition proj2_sig_map {A} {P Q : A -> Prop} (f : forall a, P a -> Q a) (x : @sig A P) : @sig A Q -- cgit v1.2.3