Theorem weqtotal2overunit (P : unit -> UU) : (∑ u, P u) ≃ P tt. Proof. set (f := fromtotal2overunit P). set (g := tototal2overunit P). split with f. assert (egf : ∏ a : _ , (g (f a)) = a). intro a. induction a as [ t p ]. induction t. apply idpath. assert (efg : ∏ a : _ , (f (g a)) = a). intro a. apply idpath. apply (isweq_iso _ _ egf efg). Defined.