n X : Pi n.+1 X <~>* Pi n (loops X). Proof. destruct n. 1: reflexivity. rapply (emap (pTr 0 o loops)). apply unfold_iterated_loops'. Defined.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.