From 3d9e7f3def594f5a07b3db934ecfac7ec2a64996 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 2 Apr 2017 17:28:07 -0400 Subject: Add ap_transport to Equality.v --- src/Util/Equality.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/Util/Equality.v') 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 -- cgit v1.2.3