{A A' B B' : Type} (f:A->A') (g:B->B') (z z' : A * B) (p : fst z = fst z') (q : snd z = snd z') : ap (functor_prod f g) (path_prod _ _ p q) = path_prod (functor_prod f g z) (functor_prod f g z') (ap f p) (ap g q). Proof. destruct z as [a b]; destruct z' as [a' b']. simpl in p, q. destruct p, q. reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.