Comment by lylecubed

> An introduction to dependent types, demonstrating the most beautiful aspects, one step at a time.

Is there a companion book detailing the ugly downsides of dependent types and how to avoid them, one step at a time?