fact: Definition istrunc_pmap `{Univalence} {m n : trunc_index} (X Y : pType) `{!IsConnected m.+1 X} `{!IsTrunc (n +2+ m) Y} : IsTrunc n (X ->* Y) := istrunc_pforall X (pfam_const Y).
imports: Basics Types WildCat Truncations Pointed.Core Pointed.pEquiv Pointed.Loops Pointed.pModality