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