Definition weqsecoverunit (P : unit -> UU) : (∏ t : unit, P t) ≃ (P tt). Proof. set (f := λ a : ∏ t : unit, P t, a tt). set (g := tosecoverunit P). split with f. assert (egf : ∏ a, g (f a) = a). { intro. apply funextsec. intro t. induction t. apply idpath. } assert (efg : ∏ a, f (g a) = a) by (intros; apply idpath). apply (isweq_iso _ _ egf efg). Defined.