Theorem isweqforalltohfiber {X : UU} (P Q : X -> UU) (f : ∏ x, P x -> Q x) (s : ∏ x, Q x) : isweq (foralltohfiber _ _ f s). Proof. use (twooutof3c (Y := @total2 (forall x, P x) (λ (s0 : forall x, P x), forall x, (λ x0 (pointover : P x0), f x0 pointover = s x0) x (s0 x)))). - exact (isweqforalltototal P (λ x, (λ pointover, f x pointover = s x))). - exact (isweqfibtototal _ _ (λ pointover, weqfunextsec _ _ _)). Defined.