fact: Definition diagonal_O_functor {A B : Type} (f : A -> B) : diagonal (O_functor O f) == equiv_O_pullback f f o O_functor O (diagonal f).
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Factorization Truncations.Core Modality Accessible Localization Descent Separated