{A B : Type} (f : A -> B) : diagonal (plus_functor L O f) == equiv_plus_pullback f f o plus_functor L O (diagonal f). Proof. intros x. refine (diagonal_O_functor L (O_functor O f) x @ _). apply (ap (equiv_O_pullback L (O_functor O f) (O_functor O f))). refine (O_functor_homotopy L _ _ (diagonal_O_functor O f) x @ _). unfold plus_functor. exact (O_functor_compose L _ _ x). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.