A denumerable type is one which is (constructively) bijective with ℕ. Although we already have a name for this property, namely α ≃ ℕ, we are here interested in using it as a typeclass.