proposition: Lemma postcompose_pconst {A B C : pType} (f : A ->* B) : pconst o* f ==* @pconst A C.
proof: Proof. srapply Build_pHomotopy. 1: reflexivity. exact (concat_p1 _ @ concat_p1 _ @ ap_const _ _)^. Defined.
imports: Basics Types Pointed.Core