Theorem isweqii2withneg {X : UU} (Y : UU) (nf : X -> empty) : isweq (@ii2 X Y). Proof. intros. set (f:= @ii2 X Y). set (g:= λ xy : X ⨿ Y, match xy with | ii1 x => fromempty (nf x) | ii2 y => y end). assert (egf : ∏ y : Y, (g (f y)) = y). intro. apply idpath. assert (efg : ∏ xy : X ⨿ Y, (f (g xy)) = xy). intro. induction xy as [ x | y ]. apply (fromempty (nf x)). apply idpath. apply (isweq_iso f g egf efg). Defined.