(A : Type) `{IsConnected O A} (P : A -> Type) `{forall x, In O (P x)} : {Q : Type & In O Q * forall x, Q <~> P x}. Proof. pose proof (O_inverts_isconnected O (fun _:A => tt)). exists (OO_descend_O_inverts O O (fun _:A => tt) P tt); split. - apply OO_descend_O_inverts_inO. - intros; nrapply OO_descend_O_inverts_beta. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.