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