fact: Definition hfibertosec { X : UU } (P:X -> UU): (hfiber (λ f x, pr1 (f x)) (λ x:X, x)) -> (∏ x:X, P x) := λ se , λ x:X, match se as se' return P x with tpair _ s e => (transportf P (toforallpaths _ (λ x:X, pr1 (s x)) (λ x:X, x) e x) (pr2 (s x))) end.
imports: UniMath.Foundations.PartB