Let $X$ be a D11: Set.

Then $X$ is a D16: Countable set if and only if \begin{equation} \mathsf{Inj}(X \to \mathbb{N}) \neq \emptyset \end{equation}