proposition: Lemma fmap_iterated_loops_pp {X Y : pType} (f : X ->* Y) n (x y : iterated_loops n.+1 X) : fmap (iterated_loops n.+1) f (x @ y) = fmap (iterated_loops n.+1) f x @ fmap (iterated_loops n.+1) f y.
proof: Proof. apply fmap_loops_pp. Defined.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core