{X Y : Type} (f : X -> Y) (y : Y) : plus_hfiber f y o to_plus L O (hfiber f y) == functor_hfiber (fun u => (to_plus_natural L O f u)^) y. Proof. intros [x q]; unfold plus_hfiber, to_plus. cbn. rewrite to_O_natural. rewrite O_functor_hfiber_natural. unfold O_functor_hfiber, functor_hfiber, functor_sigma; cbn. rewrite O_rec_beta; cbn. apply ap. unfold to_plus_natural. rewrite !inv_V, ap_pp, concat_p_pp. apply whiskerL. rewrite <- ap_compose. reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.