{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). Proof. refine (equiv_O_functor_hfiber L (O_functor O f) (to O Y y) oE _). apply equiv_O_functor. rapply equiv_O_functor_hfiber. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.