{A B : pType} (n : nat) (f : A ->* B) : pfiber (fmap (iterated_loops n) f) <~>* iterated_loops n (pfiber f). Proof. induction n. 1: reflexivity. refine (_ o*E pfiber_fmap_loops _ ). rapply (emap loops). exact IHn. Defined.
Require Import Basics Types WildCat. Require Import HFiber. Require Import Pointed.Core. Require Import Pointed.pEquiv. Require Import Pointed.Loops.