proposition: Theorem isaninvpropneg (X : UU) : isaninvprop (neg X).
proof: 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.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom