fact: Definition lex_gen `{Univalence} (O : Modality) `{IsAccModality O} (lexgen : forall (i : ngen_indices (acc_ngen O)) (x y : ngen_type (acc_ngen O) i), IsConnected O (x = y)) : Lex O.
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Factorization Truncations.Core Modality Accessible Localization Descent Separated