fact: Definition plus_hfiber {X Y : Type} (f : X -> Y) (y : Y) : Plus L O (hfiber f y) <~> hfiber (plus_functor L O f) (to_plus L O Y y).
imports: HoTT.Basics HoTT.Types Extensions HFiber Truncations NullHomotopy Limits.Pullback Descent Lex Separated