{X : Type} (x y : X) : Plus L O (x = y) <~> (to_plus L O X x = to_plus L O X y). Proof. refine (equiv_path_O L (to O X x) (to O X y) oE _). apply equiv_O_functor. rapply equiv_path_O. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.