Definition wequnittocontr {X : UU} (is : iscontr X) : unit ≃ X. Proof. intros. set (f := λ (_ : unit), pr1 is). set (g := λ (_ : X), tt). split with f. assert (egf : ∏ t : unit, g (f t) = t). { intro. induction t. apply idpath. } assert (efg : ∏ x : X, f (g x) = x). { intro. apply (! (pr2 is x)). } apply (isweq_iso _ _ egf efg). Defined.