fact: Definition pequiv_pi_connmap `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y) `{!IsConnMap n f} : Pi n X <~>* Pi n Y := Build_pEquiv _ _ (fmap (pPi n) f) _.
imports: Basics Types Pointed HSet Modalities.Modality Truncations.Core Truncations.SeparatedTrunc Algebra.AbGroups WildCat