Let me attempt a longer answer. (@Andrej Bauer 's answer is mostly about learning homotopy type theory, as opposed to delving deeper into your question.)

Unsurprisingly, the answer is still **no**. One could try to define the length of a path by the size of the smallest of its witnesses. But that definition relies on *syntax*, i.e. you need to have a 'language' in which you express your witnesses. The thing is, while HoTT does give rise to programming languages rather naturally (see my work with Amr Sabry), they still are not really 'canonical'. While $\left(\infty,1\right)$-topos certainly point in the right direction, it's not settled yet if we don't in fact want a bit more structure (see the work of Shulman, Riehl, etc if you want to dive in the really deep end of that). So we don't even know what outer structure to work in, never mind the *internal language* that we'll end up having inside that structure.

Even if all of that settled down, why would you expect the internal language to be Turing-complete? That is one of the cornerstones of the validity of Kolmogorov Complexity. Without it, *length* becomes a rather whimsical notion. Even with Kolmogorov Complexity, *length* remains a 'fuzzy' notion, because it's only defined up to a constant. So even if it existed, it would not tell you much about 'short' proofs, it only really tells you something interesting when you have one proof which is significantly shorter than the others. Certainly there is no hope that such a length notion would be a metric, never mind carve out geodesics.

Nevertheless, I do hold out some hope that there will be some notion of 'size' that will turn out to be informative and meaningful. It's just not going to be simple, or as informative as one would like.