{A B C : Type} (f : B -> A) (g : C -> A) : IsPullback (O_functor_square O _ _ _ _ (pullback_commsq f g)). Proof. unfold IsPullback. nrapply (isequiv_homotopic (O_rec (functor_pullback _ _ _ _ _ _ _ (to_O_natural O f) (to_O_natural O g)))). 1: apply isequiv_O_rec_O_inverts; exact _. apply O_indpaths. etransitivity. 1: intro x; apply O_rec_beta. symmetry. snrapply pullback_homotopic; intros [b [c e]]; cbn. all: change (to (modality_subuniv O)) with (to O). - nrapply (to_O_natural O). - nrapply (to_O_natural O). - Open Scope long_path_scope. lhs nrapply concat_p_pp. lhs nrapply (concat_p_pp _ _ _ @@ 1). rewrite to_O_natural_compose. unfold O_functor_square. rewrite O_functor_homotopy_beta. rewrite 6 concat_pp_p. do 3 apply whiskerL. rhs_V nrapply concat_pp_p. apply moveL_pM. lhs_V nrapply inv_pp. rhs_V nrapply inv_Vp. apply (ap inverse). nrapply to_O_natural_compose. Close Scope long_path_scope. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.