{X Y : Type} `{In Meet Y} : ooExtendableAlong (to_plus X) (fun _ => Y). Proof. apply (ooextendable_compose _ (to O X) (to L (O X))); rapply extendable_to_O. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.