n X : Pi n.+2 X $<~> Pi n.+1 (loops X). Proof. snrapply (groupiso_pi_functor 0). 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.