{A B C D : Type} {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D} (p : k o f == g o h) `{O_inverts O h, O_inverts O k, MapIn O _ _ f, MapIn O _ _ g} : IsPullback p := OO_ispullback_connmap_mapino O O p. Global Instance conn_map_functor_hfiber_to_O {Y X : Type} (f : Y -> X) (x : X) : IsConnMap O (functor_hfiber (fun y => (to_O_natural O f y)^) x) := OO_conn_map_functor_hfiber_to_O O O f x. Global Instance isequiv_O_functor_hfiber {A B} (f : A -> B) (b : B) : IsEquiv (O_functor_hfiber O f b). Proof. apply (isequiv_O_rec_O_inverts O). apply O_inverts_conn_map. refine (conn_map_homotopic O (functor_hfiber (fun x => (to_O_natural O f x)^) b) _ _ _). intros [a p]. unfold functor_hfiber, functor_sigma. apply ap. apply whiskerR, inv_V. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.