Add η principles for sigma types

1 files changed, 17 insertions, 0 deletions

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 *)