`{Univalence} {m n : trunc_index} (X : pType@{u}) {iscX : IsConnected m.+1 X} (Y : pFam@{u v} X) {istY : forall x, IsTrunc (n +2+ m) (Y x)} : IsTrunc@{w} n (pForall X Y). Proof. nrapply (istrunc_equiv_istrunc _ (equiv_extension_along_pforall@{v w u} Y)). rapply (istrunc_extension_along_conn (n:=m) _ Y (HP:=istY)). Defined.
Require Import Basics Types WildCat Truncations