Countable sets

A set is countable if there exists an encoding of the set into the natural numbers. An encoding is an injection with a partial inverse, which can be viewed as a constructive analogue of countability. (For the most part, theorems about countable will be classical and encodable will be constructive.)

A non-empty set is countable iff there exists a surjection from the natural numbers onto the subtype induced by the set.

Enumerate elements in a countable set.