Definition isinjinvmap' {X Y} (v w:X->Y) (v' w':Y->X) : w ∘ w' ~ idfun Y -> v' ∘ v ~ idfun X -> v' ~ w' -> v ~ w. Proof. intros p q h x . intermediate_path (w (w' (v x))). { apply pathsinv0. apply p. } apply maponpaths. rewrite <- h. apply q. Defined.