natural metrics for proof length

The short answer is no.

The notion of length is related to distance and metric, and these are all concepts that topology obliterates, let alone homotopy theory. The popular explanations of homotopy type theory in terms of topological paths (continuous maps $[0,1] \to X$) are meant to help the intuition, but should not be and cannot be understood literally. Topological spaces do not form a model of homotopy type theory.

Since you are trying to make your way into homotopy type theory, you could draw your intuition from several places, depending on your background, in decreasing order of abstraction and correctness:

1. Higher category theory: an $(\infty,1)$-topos is more or less a model of homotopy type theory, while an $\infty$-groupoid is like a single type.

2. Homotopy theory: Simplicial sets, and more precisely Kan complexes form a model of homotopy type theory, so you can think of a type as a Kan complex. In general, certain kinds of model categories can be used to interpret (parts of) homotopy type theory.

3. Groupoids: a groupoid is like a 1-type in homotopy type theory. You can think of $\mathsf{Id}_A(a,b)$ as the collection of all isomorphisms from $a$ to $b$ in a groupoid $A$.

In all cases, the "paths" are of an abstract nature. For instance, the isomorphisms in a groupoid need not be paths, just like morphisms in a category need not be functions.

There are adaptations of homotopy type theory that do relate the abstract homotopy-theoretic models with topological, and even smooth models. These go under the name cohesive homotopy type theory, but I am not sure that's the best starting point for learning homotopy type theory.

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.