Your comment is a good first approximation to the motivation for HoTT! However, let me add a couple of remarks. Firstly, HoTT can also be used with classical l

Your comment is a good first approximation to the motivation for HoTT! However, let me add a couple of remarks. Firstly, HoTT can also be used with classical logic, i.e. where you freely use the law of excluded middle. This does not impact the ability to check proofs with the computer in any way. Secondly, HoTT is the first foundation with which computer-formalized proofs of nontrivial theorems in a subject called "homotopy theory" are possible. In theory, this is possible with any foundational theory; but in practice, the necessary encodings to, for instance, Zermelo--Fraenkel set theory, are too involved for computer formalization. In HoTT, one can define (and reason about) the basic concepts of homotopy theory straight from "day one". In contrast, with a more traditional foundation, one needs to setup a host of intermediate concepts first (like the real numbers, topological spaces, homotopies, ...). This is no problem for a trained mathematician, but becomes a nuisance when working with proof assistants. Thirdly, one intriguing aspect of HoTT is that it might be possible to "run" proofs (this is the objective of current research). For example, if you prove that some group contains finitely many elements, the vision is that you could run this proof to find out how many elements it contains. This "computational interpretation" is not unique to HoTT; in fact, this is what the linked nLab article is about. But because of the second point, many more theorems are amenable to such an approach. A last remark, not pertaining to HoTT but constructive mathematics. A simple reason why one might be interested in restricting oneself to constructive arguments is that thereby they are applicable to more general situations. There is a metatheorem to the effect that "a statement with a constructive proof holds in any topos", where "topos" is a precise formulation of "alternative mathematical universe". Such universes are routinely used in several subjects of mathematics, for instance algebraic geometry (after Grothendieck's revolution). There are also other reasons for why it's fun to argue constructively. See for instance these slides: https://github.com/iblech/talk-constructive-mathematics/raw/master/negneg-translation-notes.pdf https://github.com/iblech/talk-constructive-mathematics/raw/... (PDF pages 8ff.)