Whenever I read a technical overview like this, I like to see references to existing literature. This report doesn't do this, see for example https://link.springer.com/chapter/10.1007/11541868_7 which is basically the same thing but in Coq.
I'm happy this exists, and that Agda has the facilities to make it feasible, but sad that automated formal systems are so primitive compared to software development tools. Is this gap just lack of motivation for more people to contribute, or the culture of formal systems, or some source of technical barriers, or ??
How one can type that ℕ and ℤ on the regular keyboard?..