{A B : Type} (f : A -> B) : diagonal (O_functor O f) == equiv_O_pullback f f o O_functor O (diagonal f). Proof. apply O_indpaths; intros x. refine (_ @ (ap _ (to_O_natural _ _ _))^). cbn. refine (_ @ (O_rec_beta _ _)^). unfold diagonal, functor_pullback, functor_sigma; cbn. apply ap, ap. apply moveL_pV; exact (concat_1p_p1 _). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.