This video by is pretty fascinating: youtube.com/watch?v=3gBoP8 - I'm not used to seeing Peano numbers built on set theory! Lots of loopholes that need to be closed in comparison to building on top of type theory, where lots of the well-formedness rules are built in!