{X : Type} (x y : X) (pc : PlusConnected L O X) : PlusConnected L O (x = y). Proof. unfold PlusConnected in *. apply (cancelL_nullhomotopy_equiv _ (plus_path x y)). apply (nullhomotopy_homotopic (fun u => (plus_path_to_plus x y u)^)). apply nullhomotopy_ap; assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.