  In this paper we work in o-minimal structures with definable Skolem functions
and show that a continuous definable map between Hausdorff locally definably
compact definable spaces is definably proper if and only if it is proper
morphism in the category of definable spaces. We give several other
characterizations of definably proper including one involving the existence of
limits of definable types. We also prove the basic properties of definably
proper maps and the invariance of definably proper in elementary extensions and
o-minimal expansions.
