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