fact: Definition diagonal_plus_functor {A B : Type} (f : A -> B) : diagonal (plus_functor L O f) == equiv_plus_pullback f f o plus_functor L O (diagonal f).
imports: HoTT.Basics HoTT.Types Extensions HFiber Truncations NullHomotopy Limits.Pullback Descent Lex Separated