It is that latter property which makes it well suited for proofs in homotopy theory (and category theory). Most of the examples in slides you link to are about homotopy theory.
I found a textbook after reading the slides, which may be clearer. I really don’t think their mathematical aspirations are limited to homotopy theory, after reading the book’s introduction—or even the small text blurb on the site:
Homotopy type theory offers a new “univalent” foundation of mathematics, in which a central role is played by Voevodsky’s univalence axiom and higher inductive types. The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning
I found a textbook after reading the slides, which may be clearer. I really don’t think their mathematical aspirations are limited to homotopy theory, after reading the book’s introduction—or even the small text blurb on the site: