As I see it, this is not so much a book at this stage as an introductory tutorial written by someone as they were learning Agda (about four years ago I think), as a contribution to the community to help other beginners. As such, one of the (unstated) assumptions is that the reader is already motivated to learn about programming with dependent types.
The early examples you see with inductive structures such as Nat are about learning the foundations, and you can't go on to do anything especially interesting without a solid understanding of the foundations. Its structure often also turns out to have a convenient correspondence with more realistic data structures, such as lists (their length) and trees (their depth).
I do sometimes wonder if we should start using something more obviously useful as an introductory example though. There's plenty of possibilities, and programmers aren't generally going to be using Nats in practice (I rarely do).
I don't use Agda myself (I use Idris, which is similar but is more directly aimed at general purpose programming) but I do know that it has primitive types...
Anyway, there's all kinds of interesting work going on at the minute which goes way beyond these introductory examples. For example, we're working on a way of specifying and verifying implementations of communication protocols (https://github.com/edwinb/Protocols), which we'd like to apply to cryptographic protocols when we've made some more progress. You can hear me waffling on about that, as well as about how we deal with stateful systems in general, here: https://www.youtube.com/watch?v=rXXn4UunOkE&feature=youtu.be
I post this mainly because I suspect I'm one of the wonks who was researching dependently typed programming at your university ten years ago. At the time, there was lots of foundational work to do, and there is still lots to do before it's industrial strength, but we've made a lot of progress, and I think the goal is worth striving for.
