{A B : pType} : fmap loops (@pconst A B) ==* pconst. Proof. rapply fmap_zero_morphism. 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.