Corollary remakeweqinv {X Y : UU} {f:X≃Y} {h:Y->X} : invmap f ~ h -> X≃Y. Proof. intros e. exists f. intro y. assert (p : hfiber f y). { exists (h y). apply pathsweq1', pathsinv0. apply e. } exact (iscontr_move_point p (weqproperty f y)). Defined.