diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-02 17:28:07 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-04-02 17:28:07 -0400 |
commit | 3d9e7f3def594f5a07b3db934ecfac7ec2a64996 (patch) | |
tree | 19172f38e3fd58d4392f0ddd24b5fcad7000343a /src | |
parent | fe0c2f54075c9f5c6805ee165dbf9df8b8058693 (diff) |
Add ap_transport to Equality.v
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/Equality.v | 3 |
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 |