(O' O : ReflectiveSubuniverse) `{O << O', O <<< O', O' <= Sep O} {Y X Z : Type} (f : Y -> X) (g : X -> Z) `{IsConnMap O' _ _ (g o f)} `{IsConnMap O _ _ f} : O_inverts O' f. Proof. nrapply (cancelL_isequiv (O_functor O' g)). - apply O_inverts_conn_map. apply (OO_cancelR_conn_map O' O f g). - rapply (isequiv_homotopic _ (O_functor_compose O' f g)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.