{Y X : Type} `{IsConnected O Y, IsConnected O X} (f : Y -> X) : IsConnMap O f := OO_conn_map_isconnected O O f.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.