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