(O : ReflectiveSubuniverse) (H : forall {A B : Type} (f : A -> B) (b : B), IsEquiv (O_functor_hfiber O f b)) : IsModality O. Proof. intros A'; rapply reflectsD_from_inO_sigma. intros B B_inO. pose (A := O A'). pose (g := O_rec pr1 : O {x : A & B x} -> A). transparent assert (p : (forall x, g (to O _ x) = x.1)). { intros x; subst g; apply O_rec_beta. } apply inO_isequiv_to_O. apply isequiv_contr_map; intros x. snrefine (contr_equiv' _ (hfiber_hfiber_compose_map _ g x)). apply contr_map_isequiv. unfold hfiber_compose_map. transparent assert (h : (hfiber (@pr1 A B) (g x) <~> hfiber g (g x))). { refine (_ oE equiv_to_O O _). refine (_ oE Build_Equiv _ _ (O_functor_hfiber O (@pr1 A B) (g x)) _). unfold hfiber. apply equiv_functor_sigma_id. intros y; cbn. refine (_ oE (equiv_moveR_equiv_V _ _)). apply equiv_concat_l. apply moveL_equiv_V. unfold g, O_functor. revert y; apply O_indpaths; intros [a q]; cbn. refine (_ @ (O_rec_beta _ _)^). apply ap, O_rec_beta. } refine (isequiv_homotopic (h oE equiv_hfiber_homotopic _ _ p (g x)) _). intros [[a b] q]; cbn. clear h. unfold O_functor_hfiber. rewrite O_rec_beta. unfold functor_sigma; cbn. refine (path_sigma' _ 1 _). rewrite O_indpaths_beta; cbn. unfold moveL_equiv_V, moveR_equiv_V. Open Scope long_path_scope. Local Opaque eissect. rewrite !ap_pp, !concat_p_pp, !ap_V. unfold to_O_natural. rewrite concat_pV_p. subst p. rewrite concat_pp_V. rewrite concat_pp_p; apply moveR_Vp. rewrite <- !(ap_compose (to O A) (to O A)^-1). rapply @concat_A1p. Local Transparent eissect. Close Scope long_path_scope. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.