{A B : pType} (n : nat) (f : A ->* B) : (unfold_iterated_loops' n B) o* (fmap (iterated_loops n.+1) f) ==* (fmap (iterated_loops n) (fmap loops f)) o* (unfold_iterated_loops' n A). Proof. induction n. - srefine (Build_pHomotopy _ _). + reflexivity. + cbn. apply moveL_pV. refine (concat_1p _ @ _). refine (concat_1p _ @ _). refine (_ @ (concat_p1 _)^). exact ((ap_idmap _)^). - refine ((fmap_comp loops _ _)^* @* _). refine (_ @* (fmap_comp loops _ _)). rapply (fmap2 loops). apply IHn. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Factorization Truncations.Core Truncations.Connectedness HProp. Require Import Pointed.Core Pointed.pEquiv. Require Import WildCat. Require Import Spaces.Nat.Core.