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