On the other hand, embedding mathematics in the types of a language has equivalence with writing theorems (writing the values in that language with proving them

On the other hand, embedding mathematics in the types of a language has equivalence with writing theorems (writing the values in that language with proving them) so it's not such an unnatural setting in at least one way.