fact: Definition groupiso_pi_functor (n : nat) {X Y : pType} (e : X <~>* Y) : Pi n.+1 X $<~> Pi n.+1 Y := emap (Pi n.+1) e.
imports: Basics Types Pointed HSet Modalities.Modality Truncations.Core Truncations.SeparatedTrunc Algebra.AbGroups WildCat