`{IsEquiv A A' f} `{IsEquiv B B' g} : A * B <~> A' * B'. Proof. exists (functor_prod f g). exact _. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.