Theorem isweqfibtototal' {X : UU} (P Q : X -> UU) (f : ∏ x : X, P x ≃ Q x) : isweq (totalfun _ _ f). Proof. use isweq_iso. - use totalfun. intro x. apply (invmap (f x)). - intro xp. use total2_paths_f. + apply idpath. + apply homotinvweqweq. - intro xp. use total2_paths_f. + apply idpath. + apply homotweqinvweq. Defined.