fact: Definition ppi_ptr_iterated_loops (n : nat) : pPi n = pTr 0 o iterated_loops n := ltac:(destruct n; reflexivity).
imports: Basics Types Pointed HSet Modalities.Modality Truncations.Core Truncations.SeparatedTrunc Algebra.AbGroups WildCat