fact: Definition equiv_functor_pprod {A A' B B' : pType} (f : A <~>* A') (g : B <~>* B') : A * B <~>* A' * B' := Build_pEquiv _ _ (functor_pprod f g) _.
imports: Basics Types PathAny WildCat Truncations.Core ReflectiveSubuniverse Extensions