Definition. sur_equi
sur f X Y ↔ map f X Y ∧ rng f = Y