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