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