`{Funext} {A : Type} (F : A -> pType) (X : pType) (f : forall a, X ->* F a) : X ->* pproduct F. Proof. snrapply Build_pMap. - intros x a. exact (f a x). - cbn. funext a. 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.