{A : Type} {P Q : A -> Type} {a a' : A} (p : a = a') (z : P a * Q a) : transport (fun a => P a * Q a) p z = (p # (fst z), p # (snd z)) := match p with idpath => 1 end.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.