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