`{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. Proof. srapply lex_from_inO_typeO; [ exact _ | intros i ]. rapply ooextendable_TypeO_from_extension; intros P; srefine (_;_). 1:intros; exists (forall x, P x); exact _. assert (wc : forall y z, P y <~> P z). { intros y z. refine (pr1 (isconnected_elim O _ (@equiv_transport _ P y z))). } intros x; apply path_TypeO, path_universe_uncurried. refine (equiv_adjointify (fun f => f x) (fun u y => wc x y ((wc x x)^-1 u)) _ _). - intros u; apply eisretr. - intros f; apply path_forall; intros y; apply moveR_equiv_M. destruct (isconnected_elim O _ (fun y => (wc x y)^-1 (f y))) as [z p]. exact (p x @ (p y)^). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.