From f47aced0c78747920afe3d32cbc0aeed1045d8ce Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 1 Mar 2017 15:27:48 -0500 Subject: Add η principles for sigma types MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- theories/Init/Specif.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'theories/Init') diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index e94b2e346..2cc2ecbc2 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -190,6 +190,23 @@ Definition sig2_of_sigT2 (A : Type) (P Q : A -> Prop) (X : sigT2 P Q) : sig2 P Q Definition sigT2_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sigT2 P Q := existT2 P Q (proj1_sig (sig_of_sig2 X)) (proj2_sig (sig_of_sig2 X)) (proj3_sig X). +(** η Principles *) +Definition sigT_eta {A P} (p : { a : A & P a }) + : p = existT _ (projT1 p) (projT2 p). +Proof. destruct p; reflexivity. Defined. + +Definition sig_eta {A P} (p : { a : A | P a }) + : p = exist _ (proj1_sig p) (proj2_sig p). +Proof. destruct p; reflexivity. Defined. + +Definition sigT2_eta {A P Q} (p : { a : A & P a & Q a }) + : p = existT2 _ _ (projT1 (sigT_of_sigT2 p)) (projT2 (sigT_of_sigT2 p)) (projT3 p). +Proof. destruct p; reflexivity. Defined. + +Definition sig2_eta {A P Q} (p : { a : A | P a & Q a }) + : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p). +Proof. destruct p; reflexivity. Defined. + (** [sumbool] is a boolean type equipped with the justification of their value *) -- cgit v1.2.3