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?