{A B : Type} (f : A -> B) `{O_inverts O' f} (P : A -> Type) {P_inO : forall x, In O (P x)} (a : A) : (OO_descend_O_inverts f P (f a)) <~> P a. Proof. unfold OO_descend_O_inverts. refine (OO_descend_beta O' O P a oE _). assert (p := (to_O_natural O' f a)^). apply moveR_equiv_V in p. exact (equiv_transport _ p). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.