“you can construct your own representation of the integers from the Peano axioms”

This is how the Idris prelude defines nat, the type of natural numbers (with some magic making it actually fast). I think that’s very cool.