fact: Definition OO_inverts_conn_map_isconnected_domain (O' O : ReflectiveSubuniverse) `{O << O', O <<< O', O' <= Sep O} {Y X : Type} (f : Y -> X) `{IsConnected O' Y} `{IsConnMap O _ _ f} : O_inverts O' f.
imports: HoTT.Basics HoTT.Types HFiber Extensions Limits.Pullback Modality Accessible Localization