Definition weqtodirprodwithunit (X : UU): X ≃ X × unit. Proof. intros. set (f := λ x : X, make_dirprod x tt). split with f. set (g := λ xu : X × unit, pr1 xu). assert (egf : ∏ x : X, (g (f x)) = x). intro. apply idpath. assert (efg : ∏ xu : _, (f (g xu)) = xu). intro. induction xu as [ t x ]. induction x. apply idpath. apply (isweq_iso f g egf efg). Defined.