proposition: Theorem isequiv_sigma_fibration `{Univalence} {Y : Type} : IsEquiv (@sigma_fibration Y).
proof: Proof. srapply isequiv_adjointify. - exact sigma_fibration_inverse. - intros [X p]. srapply path_sigma; cbn. + exact (path_universe (equiv_fibration_replacement _)^-1%equiv). + apply transport_arrow_toconst_path_universe. - intro P. funext y; cbn. exact ((path_universe (@hfiber_fibration _ y P))^). Defined.
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations