fact: Definition equiv_functor_prod_r {A A' B : Type} (f : A <~> A') : A * B <~> A' * B := f *E 1.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Decidable Types.Empty