{A : pType} (P Q : pFam A) : (pForall A P * pForall A Q) <~> (pForall A (Build_pFam (fun a => prod (P a) (Q a)) (dpoint P, dpoint Q))). Proof. transitivity {p : prod (forall a:A, P a) (forall a:A, Q a) & prod (fst p _ = dpoint P) (snd p _ = dpoint Q)}. 1: make_equiv. refine (issig_pforall _ _ oE _). srapply equiv_functor_sigma'. 1: apply equiv_prod_coind. intro f; cbn. unfold prod_coind_uncurried. exact (equiv_path_prod (fst f _, snd f _) (dpoint P, dpoint Q)). Defined.
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.