{A B : Type} {P : A -> Type} {Q : B -> Type} (f : A -> B) (g : forall a, P a -> Q (f a)) `{O_inverts O' f} `{forall a, O_inverts O (g a)} : O_inverts O (functor_sigma f g). Proof. srapply isequiv_homotopic'. - refine (equiv_O_sigma_O O _ oE _ oE (equiv_O_sigma_O O _)^-1). refine (Build_Equiv _ _ (O_functor O (functor_sigma f (fun x => O_functor O (g x)))) _). - apply O_indpaths. intros [x u]; cbn. rewrite !to_O_natural, O_rec_beta; cbn. rewrite !to_O_natural, O_rec_beta. reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.