{X Y : Type} (f : X -> Y) : PlusConnMap L O f -> PlusConnMap L O (diagonal f). Proof. intros pc p. refine (plusconnected_equiv L O (hfiber_diagonal f p)^-1 _). apply plusconnected_path, pc. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.