fact: Definition pequiv_ppi_ptr_iterated_loops (n : nat) (X : pType) : pPi n X <~>* pTr 0 (iterated_loops n X) := ltac:(destruct n; exact pequiv_pmap_idmap).
imports: Basics Types Pointed HSet Modalities.Modality Truncations.Core Truncations.SeparatedTrunc Algebra.AbGroups WildCat