Theorem isweqtotaltoforall {X : UU} (P : X -> UU) (PP : ∏ x, P x -> UU) : isweq (totaltoforall P PP). Proof. intros. simple refine (isweq_iso (totaltoforall P PP) (foralltototal P PP) _ _). - apply idpath. - apply idpath. Defined.