{X Y : pType} (f : X $-> Y) (n : nat) : fmap (Pi n.+1) f $== fmap (Pi 1) (fmap (iterated_loops n) f). Proof. reflexivity. Defined.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.