{X Y : Type} (f : X -> Y) : Plus X -> Plus Y := O_functor L (O_functor O f).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.