{A B C : Type} (f : A -> B -> C) {z z' : A * B} (p : fst z = fst z') (q : snd z = snd z') : ap (fun z => f (fst z) (snd z)) (path_prod _ _ p q) = ap011 f p q. Proof. destruct z, z'; simpl in *; destruct p, q; reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.