(X : Type) : to_plus (Plus X) == plus_functor (to_plus X). Proof. rapply (@O_indpaths L). intros ox. unfold to_plus, plus_functor; cbn. refine (_ @ (to_O_natural L _ ox)^). apply ap. revert ox; apply O_indpaths; intros x. exact ((to_O_natural O _ x)^). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.