Proof relevance vs. proof irrelevance
There are several possible notions of proof relevance. Let us consider three similar situations:

An element of a sum $\Sigma (x : A) . P(x)$ is a pair $(a, p)$ where $a : A$ and $p$ is a proof of $P(a)$.

An element of $\Sigma (x : A) . \|P(x)\|$, where $\|{-}\|$ is propositional truncation, is a pair $(a, q)$ where $a : A$ and $q$ is an equivalence class of proofs of $P(a)$ (where any two proofs of $P(a)$ are considered equivalent).

In set theory, an element of the subset $\{x \in A \mid \phi(x)\}$, where $\phi(x)$ is a logical formula, is just $a \in A$ such that $\phi(a)$ holds.


The first situation is proof relevant because we get full access to the proof $p$, and in particular we may analyze $p$.
The third situation is proof irrelevant because we get access just to $a \in A$ but have no further information as to why $\phi(a)$ holds, just that it does.
The second situation looks like proof irrelevance, but is actually a form of restricted proof relevance: we do not delete the proof of $P(a)$ but just control its uses with truncation. That is, from $q$ we may extract a representative proof $p$ of $P(a)$, so long as the choice of $p$ is irrelevant.
There is a cruicial difference between the third and the second situation, for having restricted access to $p$ is not at all the same as not having access at all. Here is a concrete example. Given $f : \mathbb{N} \to \mathbb{N}$, define
$$
Z(f) = \Sigma(x : \mathbb{N}) . \Pi (y : \mathbb{N}) . \mathrm{Id}(f(x + y), 0)
$$
An element of $Z(f)$ is a pair $(m, p)$ witnessing the fact that $f(n)$ is zero for all $n \geq m$. Given $f$ with this property, we want to define the sum $S(f) = f(0) + f(1) + f(2) + \cdots$, which of course should be a natural number since eventually the terms are all zero. But proof relevance matters:

We may define $S : (\Sigma (f : \mathbb{N} \to \mathbb{N}) . Z(f)) \to \mathbb{N}$ by
$$S(f, (m, p)) = f(0) + \cdots + f(m)$$

We may define $S : (\Sigma (f : \mathbb{N} \to \mathbb{N}) . \|Z(f)\|) \to \mathbb{N}$ by
$$S(f, |(m,p)|) = f(0) + \cdots + f(m),$$
where $|(m,p)|$ is the truncated witness of $Z(f)$. This is a valid definition because using a different representative $(m',p')$ leads to the same value (as we just end up adding fewer or more zeroes).

Imagining that in type theory we had proof irrelevant subset types
$$\frac{\vdash a : A \qquad \vdash p : P(a)}{\vdash a : \{x : A \mid P(x)\}}$$
we cannot define $S : \{f : \mathbb{N} \to \mathbb{N} \mid Z(f)\} \to \mathbb{N}$ because we have no information that would allow us to limit the number of terms $f(0), f(1), f(2), \ldots$ that need to be added. (There are other things we can do, but that is beside the point here.)


As long as one works in type theory, the only truly proof irrelevant judgements are judgemental equalities. We never define subset types, such as the one above, because that ruins many good properties of type theory (although it would be interesting to investigate this direction).
In the old days type theory did not have propositional truncation or any other form of quotienting, and so one was forced to work in a completely proof relevant way all the time. This is unsatisfactory because it fails to capture properly a great deal of mathematical reasoning. People invented setoids to deal with the problem, and later on introduced propositional truncation (and other forms of quotienting).
You ask wheter 1-categories are &quot;proof relevant&quot;. Well, everything in type theory is proof relevant, the only question is how do we deal with having too much proof relevance. Concretely, in a 1-category $\mathcal{C}$, equality of morphisms $f, g : A \to B$ should be &quot;irrelevant&quot; in the sense that it never matter how $f$ and $g$ are equal, only that they are. In HoTT this is expressed by requiring that $\mathrm{Id}(f,g)$ have at most one element, which amounts to
$\mathrm{Hom}_\mathcal{C}(A,B)$ being an h-set.
In setoid-based formulations of category theory, one needs to account for this phenomenon in some other way, or else one is secretly doing something other than 1-category theory. But I never liked the setoid approach (or Bishop's notion of sets, for that matter), so I will let someone else explain why and how it all makes sense.