diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-29 11:16:37 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-29 11:16:37 -0700 |
| commit | 332b9f0644305a5cde01f2744b9eeb5dbb66614b (patch) | |
| tree | bf85279837a6b9549236eba05e7153490c020ec2 | |
| parent | f03423799be521432f0550ba3498e912b3489731 (diff) | |
Rename path_sig{,T}{ => _uncurried}_iff
| -rw-r--r-- | src/Util/Sigma.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index 0867c8a34..a3d37d133 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -39,7 +39,7 @@ 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) + Definition path_sigT_uncurried_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. @@ -101,7 +101,7 @@ 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) + Definition path_sig_uncurried_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. |