{X Y : pType} (f : X ->* Y) (x y : loops X) : fmap loops f (x @ y) = fmap loops f x @ fmap loops f y. Proof. pointed_reduce_rewrite. apply ap_pp. 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.