Lemma weqishinhnegtoneg (X : UU) : ∥ ¬ X ∥ ≃ ¬ X. Proof. assert (lg : logeq (ishinh (neg X)) (neg X)). { split. - simpl. apply (@hinhuniv _ (make_hProp _ (isapropneg X))). simpl. intro nx. apply nx. - apply hinhpr. } apply (weqimplimpl (pr1 lg) (pr2 lg) (pr2 (ishinh _)) (isapropneg X)). Defined.