{A A' B B' : pType} (f : A ->* A') (g : B ->* B') : A * B ->* A' * B'. Proof. snrapply Build_pMap. - exact (functor_prod f g). - apply path_prod; apply point_eq. Defined.
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.