Theorem isweqtotaltofib {X : UU} (P Q : X -> UU) (f : ∏ x : X, P x -> Q x): isweq (totalfun _ _ f) -> ∏ x : X, isweq (f x). Proof. intros X0 x. set (totp := total2 P). set (totq := total2 Q). set (totf := (totalfun _ _ f)). set (pip := λ z: totp, pr1 z). set (piq:= λ z: totq, pr1 z). set (hfx := hfibersgftog totf piq x). simpl in hfx. assert (H : isweq hfx). unfold isweq. intro y. set (int := invezmaphf totf piq x y). assert (X1 : isweq int). apply (isweqinvezmaphf totf piq x y). induction y as [ t e ]. assert (is1 : iscontr (hfiber totf t)). apply (X0 t). apply (iscontrweqb (make_weq int X1) is1). set (ip := ezmappr1 P x). set (iq := ezmappr1 Q x). set (h := λ p: P x, hfx (ip p)). assert (is2 : isweq h). apply (twooutof3c ip hfx (isweqezmappr1 P x) H). set (h':= λ p: P x, iq ((f x) p)). assert (ee : ∏ p:P x, (h p) = (h' p)). intro. apply idpath. assert (X2 : isweq h'). apply (isweqhomot h h' ee is2). apply (twooutof3a (f x) iq X2). apply (isweqezmappr1 Q x). Defined.