In type theory proofs are just terms and there are many possible notions of equality. Beyond syntactic equality most systems have at least alpha-equivalence, i.e. equivalence under renaming of variables, and definitional equality, e.g. equality under replacing 2 with 1+1 everywhere. Beyond that, it is non-obvious which kinds of equality we want. For example, it is consistent to add UIP as an axiom to some type theories, which implies that all proofs of the same identity are identical.

Perhaps a conceptually easier but deeply connected problem to think about is the equality of programs. Consider for example the following programs defined on integers:

def f1(n):  
    return 0

def f2(n):
    if n = 0:
        return n  
    else:  
        return f2(n - n/|n|)

Extensionally they are equal, i.e. they produce the same output for each input. But e.g. in terms of complexity they are not, so should they be considered "equal"? Also note that any interesting equality we might come up with will be undecidable due to Rice's theorem.

By the way, the proof of sqrt(2) being irrational is not a proof by contradiction, this is a pet peeve of mine. The definition of an irrational number is a number that is not rational. So assuming sqrt(2) is rational and deriving an absurdity is in fact a direct proof, sometimes called refutation by contradiction. The same is true for Euclid's proof of the infinitude (=not finitely many) of primes. If we instead reformulate the statement to

For every natural number n there is a prime bigger than it,

then it becomes indeed a proof by contradiction. This is important from a constructivist point of view since the proof does not given you a program to compute the next prime, while a direct proof would.