every dependently typed purrogramming language gives really confusing errors because they refur to underlying notation that is being hidden from you fur ergonomic reasons. but then you look at a textbook full of terms like

Π u: ℕ. Π α: Sort u. Π x: α. x

which is just the identity function, and you start to get why language design is a challenge fur any language based on a dependently type theory

(The Little Typer is also (unintentionally?) really good at motivating the notational decisions and feature sets of any actually remotely purractical dependently typed language because holy shit would the language developed fur that book be annoying to use fur anything remotely interesting)