{X : Type} (x y : X) : plus_path x y o to_plus L O (x = y) == @ap _ _ (to_plus L O X) x y. Proof. intros p; unfold plus_path, to_plus, equiv_path_O, equiv_path_OO, path_OO. cbn. rewrite to_O_natural. rewrite O_rec_beta. rewrite (ap_compose (to O X) (to L (O X))). apply ap. apply O_rec_beta. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.