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