fact: Definition transport_prod {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.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Decidable Types.Empty