E.g.: Is the hope to make something all mathematicians will eventually use? Is it targeted at a relatively narrow mathematical field? Is the audience instead programmers looking to prove things about algorithms they're working on?
'Understand' is a big word. I've played around with Idris (which is a Haskell-like programming language that supports Homotopy type theory as well). I have a grasp of the underlying mathematics but don't really understand the stuff deeply.
Yes, I went on a bit of a rant and totally ignored your (totally reasonable) question. Theorem proving and proof checking are quite niche, both within computer science and mathematics. In computer science, the idea is that you can formally prove the correctness of computer programs to avoid software failures and have very robust programs. In mathematics, the ideal is to have
1. A universal language for proofs
2. A database of computer-verified results
3. Easy verification of new results