proposition: Lemma pconst_factor {A B : pType} {f : pUnit ->* B} {g : A ->* pUnit} : f o* g ==* pconst.
proof: Proof. refine (_ @* precompose_pconst f). apply pmap_postwhisker. symmetry. apply pmap_punit_pconst. Defined.
imports: Basics Types Pointed.Core