Theorem isaninvpropneg (X : UU) : isaninvprop (neg X). Proof. intros. set (f := todneg (neg X)). set (g := negf (todneg X)). set (is1 := isapropneg X). set (is2 := isapropneg (dneg X)). apply (isweqimplimpl f g is1 is2). Defined.