Definition isinjinvmap {X Y} (v w:X≃Y) : invmap v ~ invmap w -> v ~ w. Proof. intros h x. intermediate_path (w ((invmap w) (v x))). { apply pathsinv0. apply homotweqinvweq. } rewrite <- h. rewrite homotinvweqweq. apply idpath. Defined.