This series of books has always been aimed at people who want to implement the underlying systems. If you’re more interested in the application side of dependent types you might like the book Functional Programming in Lean by the same author, which is freely available online!