(H : forall A B (f : A -> B), (IsConnected O A) -> (IsConnected O B) -> (MapIn O f) -> IsEquiv f) : Lex O. Proof. apply lex_from_conn_map_lex. intros A B f AC BC. apply (conn_map_homotopic O _ _ (fact_factors (image O f))). apply conn_map_compose; [ exact _ | ]. apply conn_map_isequiv. apply H; [ | exact _ | exact _ ]. apply isconnected_conn_map_to_unit. apply (cancelR_conn_map O (factor1 (image O f)) (const_tt _)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.