{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. Proof. apply ispullback_isequiv_functor_hfiber; intros b. apply (isequiv_O_inverts O). apply OO_inverts_functor_hfiber; exact _. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.