proposition: Lemma fmap_loops_pconst {A B : pType} : fmap loops (@pconst A B) ==* pconst.
proof: Proof. rapply fmap_zero_morphism. Defined.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core