Dependent types are very cool and very frustrating. Once you get it, it opens up a whole new way to express program behavior; but until then, it all seems like pointless busywork. The Little Typer is somewhat tougher to get through than other Little books because the benefits of the paradigm it explains aren't apparent until you understand everything.
For anyone struggling to make sense of it, I suggest looking at the end of chapter 15, where a proof that the Principle of the Excluded Middle is not false is derived step by step. I found it analogous to the derivation of the Y combinator from The Little Schemer in terms of being a "holy shit" moment.
ThatGeoGuy's review gives a nice overview of the book's contents. I also wrote a detailed review that discusses what's cool and what's frustrating about the book:
For anyone struggling to make sense of it, I suggest looking at the end of chapter 15, where a proof that the Principle of the Excluded Middle is not false is derived step by step. I found it analogous to the derivation of the Y combinator from The Little Schemer in terms of being a "holy shit" moment.
ThatGeoGuy's review gives a nice overview of the book's contents. I also wrote a detailed review that discusses what's cool and what's frustrating about the book:
https://nickdrozd.github.io/2019/08/01/little-typer.html