{A B A' B'} (P : A -> B -> Type) (f : A' -> A) (g : B' -> B) {x1 x2 : A'} {y1 y2 : B'} (p : x1 = x2) (q : y1 = y2) (z : P (f x1) (g y1)) : transport011 (fun x y => P (f x) (g y)) p q z = transport011 P (ap f p) (ap g q) z. Proof. destruct p, q; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.