{A B C : Type} (f : B -> A) (g : C -> A) : Plus L O (Pullback f g) <~> Pullback (plus_functor L O f) (plus_functor L O g). Proof. refine (equiv_O_pullback L (O_functor O f) (O_functor O g) oE _). apply equiv_O_functor. rapply equiv_O_pullback. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.