fact: Definition OO_isconnected_hfiber {Y X : Type} `{IsConnected O' Y, IsConnected O' X} (f : Y -> X) (x : X) : IsConnected O (hfiber f x) := OO_conn_map_isconnected f x.
imports: HoTT.Basics HoTT.Types HFiber Extensions Limits.Pullback Modality Accessible Localization