{A B : Type} (z z' z'' : A * B) (p : fst z = fst z') (p' : fst z' = fst z'') (q : snd z = snd z') (q' : snd z' = snd z'') : path_prod z z'' (p @ p') (q @ q') = path_prod z z' p q @ path_prod z' z'' p' q'. Proof. destruct z, z', z''; simpl in *; destruct p, p', q, q'. reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.