diff options
author | Jason Gross <jagro@google.com> | 2016-07-29 11:14:53 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-07-29 11:14:53 -0700 |
commit | f03423799be521432f0550ba3498e912b3489731 (patch) | |
tree | 1608dc1330ce5ae7889d496116189671c20a75eb /src/Util/Sigma.v | |
parent | 11d0b7ad0da0b7aeb37411059150a2baf0bf68fc (diff) |
Add path_sig{,T}_iff
Diffstat (limited to 'src/Util/Sigma.v')
-rw-r--r-- | src/Util/Sigma.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index 901b2f915..0867c8a34 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -39,6 +39,13 @@ Section sigT. : u = v := path_sigT u v p (P_hprop _ _ _). + Definition path_sigT_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q) + (u v : @sigT A P) + : u = v <-> (sigT (fun p : projT1 u = projT1 v => eq_rect _ _ (projT2 u) _ p = projT2 v)). + Proof. + split; [ intro; subst; exists eq_refl; reflexivity | apply path_sigT_uncurried ]. + Defined. + Definition path_sigT_hprop_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : @sigT A P) : u = v <-> (projT1 u = projT1 v) @@ -94,6 +101,13 @@ Section sig. : u = v := path_sig u v p (P_hprop _ _ _). + Definition path_sig_iff {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q) + (u v : @sig A P) + : u = v <-> (sig (fun p : proj1_sig u = proj1_sig v => eq_rect _ _ (proj2_sig u) _ p = proj2_sig v)). + Proof. + split; [ intro; subst; exists eq_refl; reflexivity | apply path_sig_uncurried ]. + Defined. + Definition path_sig_hprop_iff {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : @sig A P) : u = v <-> (proj1_sig u = proj1_sig v) |