{X} (Y : X -> Type) {x1 x2 : X} (p : x1 = x2) {y1 y2 : Y x2} (q : y1 = y2) : ap (transport Y p) (ap (transport Y p^) q) = transport_pV Y p y1 @ q @ (transport_pV Y p y2)^. Proof. destruct p, q; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.