{X Y : Type} (f : X <~> Y) : PlusConnected X -> PlusConnected Y. Proof. intros [px e]. exists (plus_functor f px); intros y. refine (_ @ ap (plus_functor f) (e (f^-1 y))). rewrite to_plus_natural. symmetry; apply ap, eisretr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.