Theorem isweqhfibertoforall {X : UU} (P Q : X -> UU) (f : ∏ x, P x -> Q x) (s : ∏ x, Q x) : isweq (hfibertoforall P Q f s). Proof. use twooutof3c. - exact (isweqfibtototal _ _ (λ pointover, weqtoforallpaths _ _ _)). - apply isweqtotaltoforall. Defined.