From e04c5d0fc1ef38f6df0091474cddd5e2d69b7cbd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 1 Mar 2017 15:32:35 -0500 Subject: Add η principles for sigma types MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Util/Sigma.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'src/Util/Sigma.v') diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index 96a59e705..9d710a039 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -16,7 +16,7 @@ Local Arguments f_equal {_ _} _ {_ _} _. (** ** Equality for [sigT] *) Section sigT. - + (** *** Projecting an equality of a pair to equality of the first components *) Definition pr1_path {A} {P : A -> Type} {u v : sigT P} (p : u = v) : projT1 u = projT1 v @@ -96,6 +96,11 @@ Section sigT. Proof. destruct H, u; reflexivity. Defined. + + (** *** η Principle for [sigT] *) + Definition sigT_eta {A P} (p : { a : A & P a }) + : p = existT _ (projT1 p) (projT2 p). + Proof. destruct p; reflexivity. Defined. End sigT. (** ** Equality for [sig] *) @@ -161,6 +166,11 @@ Section sig. Proof. destruct H, u; reflexivity. Defined. + + (** *** η Principle for [sig] *) + Definition sig_eta {A P} (p : { a : A | P a }) + : p = exist _ (proj1_sig p) (proj2_sig p). + Proof. destruct p; reflexivity. Defined. End sig. (** ** Equality for [ex] *) -- cgit v1.2.3