proposition: Corollary isweqfromcompltodisjoint (X : UU) : isweq (fromcompltodisjoint X).
proof: Proof. intros. apply (isweqinvmap (weqtocompltodisjoint X)). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom