Definition hfibertoforall {X : UU} (P Q : X -> UU) (f : ∏ x, P x -> Q x) (s : ∏ x, Q x) : hfiber (maponsec _ _ f) s -> ∏ x, hfiber (f x) (s x). Proof. unfold hfiber. set (map1 := totalfun (λ (pointover : ∏ x, P x), (λ x, f x (pointover x)) = s) (λ (pointover : ∏ x, P x), ∏ x, (f x) (pointover x) = s x) (λ (pointover : ∏ x, P x), toforallpaths _ (λ x, f x (pointover x)) s)). set (map2 := totaltoforall P (λ x pointover, f x pointover = s x)). exact (map2 ∘ map1). Defined.