fact: Definition lex_from_modal_over_connected_isconst (H : forall (A : Type) (A_isC : IsConnected O A) (P : A -> Type) (P_inO : forall x, In O (P x)), {Q : Type & In O Q * forall x, Q <~> P x}) : Lex O.
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Factorization Truncations.Core Modality Accessible Localization Descent Separated