fact: Definition plusconnmap_diagonal {X Y : Type} (f : X -> Y) : PlusConnMap L O f -> PlusConnMap L O (diagonal f).
imports: HoTT.Basics HoTT.Types Extensions HFiber Truncations NullHomotopy Limits.Pullback Descent Lex Separated