Definition foralltohfiber {X : UU} (P Q : X -> UU) (f : ∏ x, P x -> Q x) (s : ∏ x, Q x) : (∏ x, hfiber (f x) (s x)) -> hfiber (maponsec _ _ f) s. Proof. unfold hfiber. set (map2inv := foralltototal P (λ x pointover, f x pointover = s x)). set (map1inv := totalfun (λ pointover, ∏ x, f x (pointover x) = s x) (λ pointover, (λ x, f x (pointover x)) = s) (λ pointover, funextsec _ (λ x, f x (pointover x)) s)). exact (λ a, map1inv (map2inv a)). Defined.