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