Lemma isweqtocompltodisjoint (X : UU) : isweq (tocompltodisjoint X). Proof. intros. set (ff := tocompltodisjoint X). set (gg := fromcompltodisjoint X). assert (egf : ∏ x : X, paths (gg (ff x)) x) by (intro; apply idpath). assert (efg : ∏ xx : _, paths (ff (gg xx)) xx). { intro. induction xx as [ t x ]. induction t as [ x0 | u ]. - simpl. unfold ff. unfold tocompltodisjoint. simpl. assert (ee : (negpathsii2ii1 x0 tt) = x) by apply (proofirrelevance _ (isapropneg _)). induction ee. apply idpath. - induction u. simpl. apply (fromempty (x (idpath _))). } apply (isweq_iso ff gg egf efg). Defined.