{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.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.