The context of this question is constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF.

Let us say that a set $X$ is:

**finite**when there exists a natural number $n$ and a bijection $\{1,\ldots,n\} \to X$,**finitely enumerated**when there exists a natural number $n$ and a surjection $\{1,\ldots,n\} \to X$,**subfinite**when there exists a natural number $n$ and a bijection $D \to X$ for some subset $D \subseteq \{1,\ldots,n\}$,**subfinitely enumerated**when there exists a natural number $n$ and a surjection $D \to X$ for some subset $D \subseteq \{1,\ldots,n\}$,**Dedekind-finite**when every injection $X\to X$ is, in fact, a bijection.

Clearly, finite sets are finitely enumerated and subfinite, and finitely enumerated or subfinite sets are subfinitely enumerated, and it is not hard to give Brouwerian counterexamples to show that there are no further implications between these four notions. (However, a set $X$ is finite iff it is finitely enumerated and discrete, where “discrete” means that the diagonal $\Delta \subseteq X^2$ is a decidable subset.)

Also, finite sets are Dedekind-finite. But this leaves the question of which of the three remaining notions imply Dedekind-finiteness.

Note that a subset or a quotient of a Dedekind-finite set need not be Dedekind-finite: this is shown (by constructing appropriate topoi) in Stout, “Dedekind finiteness in topoi”, *J. Pure Appl. Algebra* **49** (1987) 219–225, but this paper doesn't say whether a subset or a quotient of a *finite* set need be Dedekind-finite.

So:

**Question:** Is a finitely enumerated set necessarily Dedekind-finite? Is a subfinite set necessarily Dedekind-finite? Is a subfinitely enumerated set necessarily Dedekind-finite?

(As usual, the answer “these are well-known open questions” will be deemed satisfactory, but the mere fact that the answer does not appear on the nLab page on the subject is not quite sufficient.)

notone of the forms considered in the question). $\endgroup$