This proof irrelevance is one of the problems of classic foundations.
In Type Theory, however, we represent mathematical statements as types, which enables us to treat proofs as mathematical objects. This is because of a well-known isomorphism between types and propositions a.k.a. Curry-Howard Correspondence, which roughly says that to find a proof of a statement A is to find a inhabitant of this type:
Which, in the point of view of logic, can be read 'a is a proof of the proposition A'.
In this sense, to prove a proposition is to construct an inhabitant of a type, which means that every mathematical proof can be seen as an algorithm. This is related with "constructive" (intuitionistic) conception of logic where (i) to prove a statement of the form "A and B" is to find a proof of A and a proof of B, (i) to prove that A implies B is to find a function that converts a proof of A into a proof of B (iii) every prove that something exists carries with it enough information to exhibit such object and so on. Hence equality of elements of a type (proofs) is treated intensionally.
Now Homotopy Type Theory thinks of types as "homotopical spaces", interpreting, as stated in the comments, the relation of identity $a=b$ between elements (proofs) of the same type (proposition) $a,b: A$ as homotopical equivalence, understood as a path from the point $a$ to the point $b$ in the space $A$. The HoTT book is available for free in the project website.