{A B C} (f : B <~>* C) (g : A ->* B) (h : A ->* C) (p : f^-1* o* h ==* g) : (h ==* f o* g). Proof. refine (_ @* pmap_postwhisker f p). refine (_ @* (pmap_compose_assoc _ _ _)). refine ((pmap_postcompose_idmap _)^* @* _). apply pmap_prewhisker. symmetry; apply peisretr. Defined.
Require Import Basics. Require Import Types. Require Import WildCat. Require Import Pointed.Core.