Definition weqoncompl {X Y : UU} (w : X ≃ Y) x : compl X x ≃ compl Y (w x). Proof. intros. intermediate_weq (∑ x', w x != w x'). - apply weqfibtototal; intro x'. apply weqiff. {apply logeqnegs. apply weq_to_iff. apply weqonpaths. } {apply isapropneg. } {apply isapropneg. } - refine (weqfp _ _). Defined.