`{O' <= Sep O} {X : Type@{i}} (x y : X) : O (x = y) <~> (to O' X x = to O' X y) := Build_Equiv _ _ (path_OO x y) _. Global Instance OO_inverts_functor_hfiber {A B C D : Type} {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D} (p : k o f == g o h) (b : B) `{O_inverts O' h, O_inverts O' k} : O_inverts O (functor_hfiber p b). Proof. unfold functor_hfiber. snrefine (OO_inverts_functor_sigma _ _). 1:exact _. intros a; cbn. refine (isequiv_homotopic (O_functor O (concat (p a)^) o O_functor O (@ap _ _ k (f a) b)) _). symmetry; apply O_functor_compose. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.