aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Equality.v
diff options
context:
space:
mode:
authorJason Gross <jgross@mit.edu>2017-04-02 17:28:07 -0400
committerJason Gross <jgross@mit.edu>2017-04-02 17:28:07 -0400
commit3d9e7f3def594f5a07b3db934ecfac7ec2a64996 (patch)
tree19172f38e3fd58d4392f0ddd24b5fcad7000343a /src/Util/Equality.v
parentfe0c2f54075c9f5c6805ee165dbf9df8b8058693 (diff)
Add ap_transport to Equality.v
Diffstat (limited to 'src/Util/Equality.v')
-rw-r--r--src/Util/Equality.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index 81c94d871..456c9497a 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -44,6 +44,9 @@ Proof. case p; reflexivity. Defined.
Definition transport_idmap_ap A (P : A -> Type) x y (p : x = y) (u : P x)
: eq_rect _ P u _ p = eq_rect _ (fun T => T) u _ (f_equal P p).
Proof. case p; reflexivity. Defined.
+Definition ap_transport {A} {P Q : A -> Type} {x y : A} (p : x = y) (f : forall x, P x -> Q x) (z : P x)
+ : f _ (@eq_rect A x P z y p) = @eq_rect A x Q (f _ z) y p.
+Proof. case p; reflexivity. Defined.
(** To classify the equalities of a type [A] at a point [a : A], we
must give a "code" that stands in for the type [a = x] for each