(X : Type) : PlusConnMap L O (to_plus L O X). Proof. intros y; unfold PlusConnected. apply (cancelL_nullhomotopy_equiv _ (plus_hfiber (to_plus L O X) y)). apply (nullhomotopy_homotopic (fun u => (plus_hfiber_to_plus (to_plus L O X) y u)^)). unfold NullHomotopy, hfiber. unshelve refine ((y ; _) ; _). { symmetry; apply wellpointed_plus. } intros [x p]; destruct p. unfold functor_hfiber, functor_sigma; cbn. apply ap. rewrite inv_V, concat_p1. unfold wellpointed_plus. rewrite !O_indpaths_beta. rewrite inv_pp, ap_V, !inv_V. reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.