{Y X Z : Type} (f : Y -> X) (g : X -> Z) `{IsConnMap O' _ _ (g o f)} `{IsConnMap O' _ _ g} : IsConnMap O f. Proof. apply conn_map_OO_inverts. nrapply (cancelL_isequiv (O_functor O' g)). 1:exact _. 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.