(H : forall (A : Type) (Ac : IsConnected O A) (x y : A), IsConnected O (x = y)) : Lex O. Proof. apply lex_from_conn_map_lex. intros A B f Ac Bc c. rapply isconnected_sigma. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.