n X : Pi n.+1 X $<~> Pi 1 (iterated_loops n X) := grp_iso_id. Module PiUtf8. Notation "'π'" := Pi. End PiUtf8. Global Instance ishset_pi {n : nat} {X : pType} : IsHSet (Pi n X) := ltac:(destruct n; exact _). Global Instance isabgroup_pi (n : nat) (X : pType) : IsAbGroup (Pi n.+2 X). Proof. nrapply Build_IsAbGroup. 1: exact _. intros x y. strip_truncations. cbn; apply (ap tr). apply eckmann_hilton. Defined.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.