{A B : Type} {f : A -> B} {x1 x2 : A} {y : B} (p : x1 = x2) (q : f x1 = y) : transport (fun x => f x = y) p q = (ap f p)^ @ q. Proof. destruct p, q; reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.