proposition: Lemma pmap_punit_pconst {A : pType} (f : A ->* pUnit) : pconst ==* f.
proof: Proof. srapply Build_pHomotopy. 1: intro; apply path_unit. apply path_contr. Defined.
imports: Basics Types PathAny WildCat Truncations.Core ReflectiveSubuniverse Extensions