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