fact: Definition weqforalltohfiber {X : UU} (P Q : X -> UU) (f : ∏ x, P x -> Q x) (s : ∏ x, Q x) : (∏ x, hfiber (f x) (s x)) ≃ hfiber (maponsec P Q f) s := make_weq _ (isweqforalltohfiber P Q f s).
imports: UniMath.Foundations.PartC