{A A' B B' : Type} (f : A <-> A') (g : B <-> B') : A * B <-> A' * B' := (functor_prod (fst f) (fst g) , functor_prod (snd f) (snd g)).
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.