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