Lemma compl_weq_compl_ne (X : UU) (x : X) (neq_x : neqPred x) : compl_ne X x neq_x ≃ compl X x. Proof. intros. apply weqfibtototal; intro y. apply weqiff. - apply issymm_logeq. apply negProp_to_iff. - apply negProp_to_isaprop. - apply isapropneg. Defined.