Proof relevance vs. proof irrelevance I want to use use Agda to help me write proofs, but I am getting contradictory feedback about the value of proof relevance.
Jacques Carette wrote a Proof-relevant Category Theory in Agda library. But some seem to think (perhaps here, but I was told elsewhere) that proof relevance can be problematic. 1-Category Theory is supposed to be proof irrelevant (and I guess above two categories, this is no longer the case?) I even heard that one may not get the same results if one uses proof relevant category theory.
At the same time I believe the Category Theory in the HoTT book and the implementation in Cubical Agda are proof irrelevant (as the HomSets are Sets, i.e., have only one way of being equal).
When should I be happy to have proof relevance? When should I rather choose a proof irrelevant library or proof assistant? What are the advantages of each? Would proof irrelevance be problematic as I move to two categories?
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.