Corollary isweqinvmap {X Y : UU} (w : X ≃ Y) : isweq (invmap w). Proof. intros. assert (efg : ∏ (y : Y), w (invmap w y) = y). apply homotweqinvweq. assert (egf : ∏ (x : X), invmap w (w x) = x). apply homotinvweqweq. apply (isweq_iso _ _ efg egf). Defined.