Despite its old age, this is the best available book on dependent types. It has its drawbacks, there are a lot of areas which aren't covered well. However, it's way better than any tutorials on dependent types you can find on internet.