{Y X : Type} `{IsConnected O' Y, IsConnected O' X} (f : Y -> X) `{MapIn O _ _ f} : IsEquiv f. Proof. apply (isequiv_conn_ino_map O). - apply OO_conn_map_isconnected. - assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.