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