proposition: Lemma isaninv1 (X : UU) : isdecprop X -> isaninvprop X.
proof: Proof. intros is1. unfold isaninvprop. assert (is2 := pr1 is1); simpl in is2. assert (adjevinv: dneg X -> X). { intro X0. induction is2 as [ a | b ]. - assumption. - contradicts X0 b. } assert (is3: isaprop (dneg X)). { apply (isapropneg (X -> empty)). } apply (isweqimplimpl (todneg X) adjevinv is1 is3). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom