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