{A B : Type} (f : A -> B) `{O_inverts O' f} (P : A -> Type) {P_inO : forall x, In O (P x)} : B -> Type. Proof. intros b. pose (Q := OO_descend O' O P). exact (Q ((O_functor O' f)^-1 (to O' B b))). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.