(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. Proof. intros A; unshelve econstructor; intros P P_inO. all:pose (Q := fun z:O A => H (hfiber (to O A) z) _ (P o pr1) _). - exact (fun z => (Q z).1). - exact (fun z => fst (Q z).2). - intros x; cbn. exact (snd (Q (to O A x)).2 (x;1)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.