Theorem isweqfibtototal {X : UU} (P Q : X -> UU) (f : ∏ x : X, P x ≃ Q x) : isweq (totalfun _ _ f). Proof. set (fpq := totalfun P Q f). set (pr1p := λ z : total2 P, pr1 z). set (pr1q := λ z : total2 Q, pr1 z). unfold isweq. intro xq. set (x:= pr1q xq). set (xqe:= make_hfiber pr1q xq (idpath _)). set (hfpqx:= hfibersgftog fpq pr1q x). assert (isint : iscontr (hfiber hfpqx xqe)). assert (isint1 : isweq hfpqx). set (ipx := ezmappr1 P x). set (iqx := ezmappr1 Q x). set (diag := λ p : P x, (iqx ((f x) p))). assert (is2: isweq diag). apply (twooutof3c (f x) iqx (pr2 (f x)) (isweqezmappr1 Q x)). apply (twooutof3b ipx hfpqx (isweqezmappr1 P x) is2). unfold isweq in isint1. apply (isint1 xqe). set (intmap := invezmaphf fpq pr1q x xqe). apply (iscontrweqf (make_weq intmap (isweqinvezmaphf fpq pr1q x xqe)) isint). Defined.