{X Y : Type} (f : X -> Y) := forall y, PlusConnected (hfiber f y).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.