I read this book twice, one of my favorite reads. If you can look past the student-teacher discussion format (which I personally enjoy) it's an excellent introduction to dependent types.