Context: I'm starting with being interested in type theory as a framework within which to do mathematics (e.g. practically, using proof assistants based on type theory), and my understanding is that HoTT is motivated partially/primarily from that perspective. I and am not interested in homotopy theory per se, or in using type theory to understand homotopy theory.
My understanding of homotopy type theory is limited, but I know that in HoTT we think of a type $T$ as a space, of instances $x,y:T$ of the type as points in that space, and of proofs $p:x=_Ty$ of equality as paths in the space.
How I can understand "proofs of equality as paths"
My interpretation of proofs of equality is that they are computational paths between terms. If we think of $x$ and $y$ as actual constructed terms in e.g. a proof assistant such as Coq, then the way to prove $x=_Ty$ is to show a sequence of computational steps (or at least, a program that would produce one, such as in an inductive proof) from $x$ to $y$. E.g. with the standard inductive definition of the natural numbers, it could be a transformation from $(1+1)+1$ (i.e. $x$) to $3$ (i.e. $y$), by repeatedly applying the addition rules to get $s (s (s (0)))$ and then applying the definition of $3$. i.e. proofs of $x=_Ty$ are computationally valid paths between terms, using the underlying computational system's (lambda calculus I'd presume) valid computation rules (e.g. beta-reduction, delta-reduction of lambda-terms).
So the way I think of it is: two terms may be different syntactically (e.g. $1+1$ and $2$), and are therefore different points in the "space belonging to their type" (e.g. $\mathbb N$). But they are semantically equal to each other, so that there is a computational path between them.
proofs of equality in homotopy type theory
In explanations of homotopy type theory that I've seen, the explanation usually asks you to think of types as spaces, where usually they are pictured as topological spaces (circles, donuts, etc). Then the point is made that two proofs $p,q:x=_Ty$ are fundamentally different, if there is no homotopy between them, and some image like this is shown to suggest that two proofs are not homotopic:
But afaik, a homotopy has to be continuous, meaning that the space has to have some kind of topological structure. However, the computational steps that we make in reasoning e.g. that $(1+1)+1 = 3$, are finite. My understanding is that it's fundamental to intuitionistic type theory that all the terms of a type are actually constructible terms, i.e. strings of symbols that we can write down, and hence that the "space" belonging to a type $T$ is discrete. But the only reasonable topology that I can think of on such a space would be the topology generated by the base set consisting of equivalence classes of terms based on $=_T$, which would I think imply that all paths $p,q:x=_Ty$ are homotopy equivalent (since any path consisting of points inside such a base set is continuous).
This makes me confused about homotopy type theory itself: It seems to me that in order to formalize the idea of proofs being fundamentally different, we'd have to think of a discrete object, probably a finite graph (where nodes are terms and links are basic computational steps), and concepts like homotopy and continuous functions and spaces are out of place.
Where is the mistake in my thinking?
Best Answer
I would say there is no mistake in your thinking. Rather, the mistake happened many decades ago when algebraic topologists gradually came to use the word "space" for a discrete object that should really be called an "$\infty$-groupoid". The correct thing to say is then that HoTT interprets types as $\infty$-groupoids (though not, of course, necessarily finite ones). This is even true semantically: all the formal mathematical interpretations of HoTT sending types to "spaces" actually use structures such as simplicial sets or cubical sets, which are discrete objects --- it's just that homotopy theorists have come to abuse the word "space" to refer to those things rather than to actual topological spaces.
The reason the word "space" took on this meaning is that topological spaces can be used as presentations of $\infty$-groupoids via a construction called the "fundamental $\infty$-groupoid of a space", and (at least, assuming classical logic) every $\infty$-groupoid is equivalent to one arising in this way. Moreover, the fundamental $\infty$-groupoid of a space remembers (and is "determined by", in an appropriate sense) all of the algebraic invariants constructible from a topological space, and so algebraic topologists studying these invariants came gradually to identify a topological space with its fundamental $\infty$-groupoid --- and this was historically before anyone had given a precise definition of $\infty$-groupoid at all.
However, nowadays this conflation of spaces with $\infty$-groupoids has real dangers, one of which is the difficulty of intuition that you've run across. Another is that we also sometimes want to study spatial $\infty$-groupoids, i.e. $\infty$-groupoids that also have an additional topology on their underlying sets that's unrelated to their $\infty$-groupoid structure, and if "space" means $\infty$-groupoid then that gets very confusing.
I have written some introductions to HoTT that emphasize this perspective, called A synthetic approach to higher equalities and The logic of space.