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