Definition weqsecovercontr {X : UU} (P : X -> UU) (is : iscontr X) : (∏ x, P x) ≃ (P (pr1 is)). Proof. intros. set (w1 := weqonsecbase P (wequnittocontr is)). apply (weqcomp w1 (weqsecoverunit _)). Defined.