<p>I recommend that everyone first read Andrej Bauer's answer, as he covers all the basics extremely well. I agree with everything he says in his answer. I humbly offer more comments, even though I know less on this topic than he does - but I was mentioned by name, as was my project.</p>
<p>When I gave a talk about agda-categories, I explained one thing about it that isn't in the paper: I am neither a proof-relevance zealot, nor was I seeking to become a proof-relevance champion. In fact, when it became clear that Agda's previous mechanism for proof irrelevance had somehow gotten quite 'broken', we simply set out to rebuild the library without using that. Jason suggested we go proof-relevant, and I decided to give it a try, mainly as an exploration of where/how things would go wrong. Much to my surprise, not only did things not go wrong, things were in fact quite smooth. The main conclusion that I draw from this is that &quot;category theory&quot; (note the distinct lack of <strong>1-</strong> there) can be proof relevant without real problems.</p>
<p>One take: proof relevance vs proof irrelevance is a false dichotomy. And Andrej's answer further shows that it should indeed be taken as a trichotomy. But that's not my point: you shouldn't be asking whether to choose one route or another. That is a <strong>false choice</strong>. What you should instead try to understand are the advantages and disadvantages of each route, and choose the route that is best suited to your current task. There is no point in asking to &quot;globally&quot; choose one versus the other.</p>
<p>It is indeed correct to point out that, strictly speaking (pun intended), agda-categories is not 1-category theory as classically envisioned. It isn't 2-category theory either, but rather feels like something &quot;in between&quot;. By and large, it works very much like 1-category theory almost all of the time, but once in a while, things 'leak in' from 2-category theory.</p>
<p>I think the main lesson from agda-categories, as far as proof-relevance is concerned, is that category theory seems to largely not care. In other words, category theory is very robust and can exist largely unscathed in a variety of meta-theories, especially when you are aware of the whole topic (i.e. from <span class="math-container">$-2$</span>-categories to <span class="math-container">$(\infty,1)$</span>-categories to <span class="math-container">$(n,k)$</span>-categories, enriched categories, etc). Then you see that all that changes is that some concerns move around a tiny bit, but that's it.</p>
<p>[Edit:] Oh, and I forgot to mention why Setoids make sense. As far as I can tell (and the nLab largely corroborates this), if you build up category theory constructively (i.e. your meta-theory does not have excluded middle or choice) starting from <span class="math-container">$-2$</span>-categories, then enrich your way up, <span class="math-container">$0$</span>-categories are Setoids and <span class="math-container">$1$</span>-categories are then forcibly Setoid-enriched. You need to use various axioms to 'squish down' pieces of the <span class="math-container">$-2\ldots 1$</span> sequence to get the classical view. There's nothing wrong (or right!) with that. It's just a choice (ooh, another pun!)  So I've come to think of Setoids here being quite natural, mostly because I'm currently happy exploring a particular part of the 'design space' of mathematics that sits inside a particular universe defined by a constructive meta-theory.</p>

CC BY-SA 4.0
2020-12-30T15:40:02.517Z
2020-12-30T16:40:38.863Z
2020-12-30T16:40:38.863Z
Jacques Carette
<p>There are several possible notions of proof relevance. Let us consider three similar situations:</p>
<ol>
<li><p>An element of a sum <span class="math-container">$\Sigma (x : A) . P(x)$</span> is a pair <span class="math-container">$(a, p)$</span> where <span class="math-container">$a : A$</span> and <span class="math-container">$p$</span> is a proof of <span class="math-container">$P(a)$</span>.</p>
</li>
<li><p>An element of <span class="math-container">$\Sigma (x : A) . \|P(x)\|$</span>, where <span class="math-container">$\|{-}\|$</span> is propositional truncation, is a pair <span class="math-container">$(a, q)$</span> where <span class="math-container">$a : A$</span> and <span class="math-container">$q$</span> is an <em>equivalence class</em> of proofs of <span class="math-container">$P(a)$</span> (where any two proofs of <span class="math-container">$P(a)$</span> are considered equivalent).</p>
</li>
<li><p>In set theory, an element of the subset <span class="math-container">$\{x \in A \mid \phi(x)\}$</span>, where <span class="math-container">$\phi(x)$</span> is a logical formula, is just <span class="math-container">$a \in A$</span> such that <span class="math-container">$\phi(a)$</span> holds.</p>
</li>
</ol>
<p>The first situation is <em>proof relevant</em> because we get full access to the proof <span class="math-container">$p$</span>, and in particular we may analyze <span class="math-container">$p$</span>.</p>
<p>The third situation is <em>proof irrelevant</em> because we get access just to <span class="math-container">$a \in A$</span> but have no further information as to why <span class="math-container">$\phi(a)$</span> holds, just that it does.</p>
<p>The second situation <em>looks</em> like proof irrelevance, but is actually a form of <em>restricted</em> proof relevance: we do not <em>delete</em> the proof of <span class="math-container">$P(a)$</span> but just <em>control</em> its uses with truncation. That is, from <span class="math-container">$q$</span> we may extract a representative proof <span class="math-container">$p$</span> of <span class="math-container">$P(a)$</span>, so long as the choice of <span class="math-container">$p$</span> is irrelevant.</p>
<p>There is a cruicial difference between the third and the second situation, for having restricted access to <span class="math-container">$p$</span> is not at all the same as not having access at all. Here is a concrete example. Given <span class="math-container">$f : \mathbb{N} \to \mathbb{N}$</span>, define
<span class="math-container">$$
Z(f) = \Sigma(x : \mathbb{N}) . \Pi (y : \mathbb{N}) . \mathrm{Id}(f(x + y), 0)
$$</span>
An element of <span class="math-container">$Z(f)$</span> is a pair <span class="math-container">$(m, p)$</span> witnessing the fact that <span class="math-container">$f(n)$</span> is zero for all <span class="math-container">$n \geq m$</span>. Given <span class="math-container">$f$</span> with this property, we want to define the sum <span class="math-container">$S(f) = f(0) + f(1) + f(2) + \cdots$</span>, which of course should be a natural number since eventually the terms are all zero. But proof relevance matters:</p>
<ol>
<li><p>We may define <span class="math-container">$S : (\Sigma (f : \mathbb{N} \to \mathbb{N}) . Z(f)) \to \mathbb{N}$</span> by
<span class="math-container">$$S(f, (m, p)) = f(0) + \cdots + f(m)$$</span></p>
</li>
<li><p>We may define <span class="math-container">$S : (\Sigma (f : \mathbb{N} \to \mathbb{N}) . \|Z(f)\|) \to \mathbb{N}$</span> by
<span class="math-container">$$S(f, |(m,p)|) = f(0) + \cdots + f(m),$$</span>
where <span class="math-container">$|(m,p)|$</span> is the truncated witness of <span class="math-container">$Z(f)$</span>. This is a valid definition because using a different representative <span class="math-container">$(m',p')$</span> leads to the same value (as we just end up adding fewer or more zeroes).</p>
</li>
<li><p>Imagining that in type theory we had proof irrelevant subset types
<span class="math-container">$$\frac{\vdash a : A \qquad \vdash p : P(a)}{\vdash a : \{x : A \mid P(x)\}}$$</span>
we <strong>cannot</strong> define <span class="math-container">$S : \{f : \mathbb{N} \to \mathbb{N} \mid Z(f)\} \to \mathbb{N}$</span> because we have no information that would allow us to limit the number of terms <span class="math-container">$f(0), f(1), f(2), \ldots$</span> that need to be added. (There are other things we can do, but that is beside the point here.)</p>
</li>
</ol>
<p>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).</p>
<p>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).</p>
<p>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 <em>too much</em> proof relevance. Concretely, in a 1-category <span class="math-container">$\mathcal{C}$</span>, equality of morphisms <span class="math-container">$f, g : A \to B$</span> should be &quot;irrelevant&quot; in the sense that it never matter <em>how</em> <span class="math-container">$f$</span> and <span class="math-container">$g$</span> are equal, only that they are. In HoTT this is expressed by requiring that <span class="math-container">$\mathrm{Id}(f,g)$</span> have at most one element, which amounts to
<span class="math-container">$\mathrm{Hom}_\mathcal{C}(A,B)$</span> being an h-set.</p>
<p>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.</p>

CC BY-SA 4.0
2020-12-30T15:19:31.893Z
I was hoping you'd show up and answer this question! I'll try to expand on the points that you decided to leave alone.
Jacques Carette
CC BY-SA 4.0
2021-01-01T20:12:59.143Z
In item 3 of the second list, $p$ should be of type $P(a)$, not $A(a)$.
Andreas Blass
CC BY-SA 4.0
2021-01-01T23:58:40.867Z
@AndreasBlass: fixed, thanks. By the way, everyone can edit answers.
Andrej Bauer
CC BY-SA 4.0
2023-11-23T03:03:05.630Z
In the "subset types" case, suppose we also had a rule $A:\text{Type},P:A\to\text{Prop} \vdash \text{pf}_{A,P}: \Pi_{a:\{x:A | P(x)\}} P(a)$.  Couldn't this be used to define $S$?
Joshua Meyers
CC BY-SA 4.0
2023-11-23T18:47:19.000Z
@JoshuaMeyers: Yes we could, but your suggestion make subset types equivalent to dependent sums, because $\mathrm{pf}$ is just the second projection from  $\Sigma (x : A) \, P(x)$ in disguise, so I think you managed to make the subset types equivalent to dependent sums.
Andrej Bauer
CC BY-SA 4.0
2023-11-24T03:20:48.760Z
The difference seems to me that whether we use $\text{pf}:P(a)$ or a distinct $\text{pf}':P(a)$, your generating rule in 3 still gives the same $a:\{x:A|P(x)\}$, and $\text{pf}_{A,P}(a)$ is not necessarily equal to either $\text{pf}$ or $\text{pf}'$.  Am I doing something incorrect?
Joshua Meyers
CC BY-SA 4.0
2023-11-24T12:00:58.167Z
Oh I see, you're *not* assuming the $\beta$-rules for projections, which keeps the proof opaque. Yes, that would be a reasonable way of doing it, assuming we've got some sort of proof irrelevance going on so that $\mathrm{pf}$ does not get stuck during normalization. Minor quibble: I would not use $\Pi$ to express the rule, but rather something like
$$
\frac{\vdash A \;\mathrm{type} \qquad x : A \vdash P(x) : \mathrm{Prop} \qquad \vdash a : \lbrace x : A \mid P(x) \rbrace }{\vdash \mathrm{pf}(A, x.P(x), a) : P(a)}
$$
Andrej Bauer
CC BY-SA 4.0
2023-11-24T20:55:01.243Z
So this approach seems like the **best one** to me, in the sense that it accurately represents what mathematicians do in their practice.  For example, proofs of the group axioms are not at all part of the data of a group $G$, even as an equivalence class, but opaque proofs of these axioms can be recovered from $G$ -- i.e. we can write "since $G$ is a group, associativity holds".  Do you agree?
Joshua Meyers
CC BY-SA 4.0
2023-11-25T01:20:38.257Z
Also btw I agree with your minor quibble, it's cleaner that way
Joshua Meyers
CC BY-SA 4.0
2023-11-25T09:09:53.150Z
As I said, there is trickery involved with judgemental equality when there are opaque proofs that don't compute. Are we going to just have equality checker blocking on comparison of `pf(a) ≡ p : P(a)`, or will these be automatically equal (this is known as strict `Prop`)? If they are automatically equal, then it's not so easy to have untyped normalization, and also to eliminate proofs of propositions (in particular, $\exists$-elimination is a bummer). Of course, these considerations are not appreciated by mathematicians, even though they expect their proof assistant to work well.
Andrej Bauer
CC BY-SA 4.0
2023-12-02T14:52:53.220Z
As a mathematician, what should I do / read in order to appreciate these concerns? Presently I don't really know why untyped normalization is important, or why opaque proofs would get in the way of $\exists$-elimination.  I don't even understand why canonicity/adequacy is important (also asking about this last point on Zulip right now)
Joshua Meyers
CC BY-SA 4.0
2023-12-03T08:55:23.547Z
Hmm, that's a *very* good question. I don't recall any experts writing this stuff up, they just expect PhD students to learn by osmosis. Perhaps someone else knows? What's a piece of writing directed at "normal" mathematicians that explains the relevance of proof irrelevance? (Oooh, I just got a title for a blog post.)
Andrej Bauer
CC BY-SA 4.0
2020-12-30T15:14:42.543Z
2021-01-01T23:58:24.913Z
2021-01-01T23:58:24.913Z
Andrej Bauer
<p>I want to use use Agda to help me write proofs, but I am getting contradictory feedback about the value of proof relevance.</p>
<p>Jacques Carette wrote a <a href="https://arxiv.org/abs/2005.07059" rel="noreferrer">Proof-relevant Category Theory in Agda</a> library. But some seem to think (<a href="https://stackoverflow.com/questions/65493694/why-do-calculus-of-construction-based-languages-use-setoids-so-much/65500321#65500321">perhaps here</a>, 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.</p>
<p>At the same time I believe the Category Theory in the HoTT book and the <a href="https://github.com/agda/cubical/tree/master/Cubical/Categories" rel="noreferrer">implementation in Cubical Agda</a> are proof irrelevant (as the HomSets are Sets, i.e., have only one way of being equal).</p>
<p>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?</p>

CC BY-SA 4.0
2020-12-30T13:37:02.270Z
You can think of a proof irrelevant type as the quotient of a proof relevant version of this type by the full equivalence relation. The advantage of quotienting a type is that for a dependent type B that depends on x of type A, by replacing A by its quotient, you make transports between $A[t/x]$ and $A[u/x]$ easier because $t$ and $u$ sometimes land in the same equivalence class. The disadvantage of quotienting is that some maps are easy to define with domain A, but proving that they factor through the quotient can be tedious. I'm not sure which one is better for categories.
xavierm02
CC BY-SA 4.0
2020-12-30T15:33:31.397Z
@xavierm02: you are describing a situation where the *choice* of proofs is irrelevant, but the proofs themselves are still relevant (recorded). A stronger form of proof irrelevance actually deletes the proofs. Judgmental equality is like that.
Andrej Bauer
CC BY-SA 4.0
2021-01-01T06:01:49.113Z
Here's an interesting perspective: http://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf
Mike Shulman
CC BY-SA 4.0
2021-01-01T12:57:06.850Z
I just discovered that there was an interesting discussion on the topic on the agda mailing list in November 2020 on this topic and setoids https://lists.chalmers.se/pipermail/agda/2020/012405.html
Henry Story
<ct.category-theory><proof-theory><proof-assistants><homotopy-type-theory><agda>
Proof relevance vs. proof irrelevance
Henry Story
# Proof relevance vs. proof irrelevance

(Asked by: username_0 on 2020-12-30)

I want to use use Agda to help me write proofs, but I am getting contradictory feedback about the value of proof relevance.

username_4 wrote a [Proof-relevant Category Theory in Agda](https://arxiv.org/abs/2005.07059) library. But some seem to think ([perhaps here](https://stackoverflow.com/questions/65493694/why-do-calculus-of-construction-based-languages-use-setoids-so-much/65500321#65500321), 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](https://github.com/agda/cubical/tree/master/Cubical/Categories) 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?

**Tags:** ct.category-theory, proof-theory, proof-assistants, homotopy-type-theory, agda

> **Comments:**
> **username_1**: You can think of a proof irrelevant type as the quotient of a proof relevant version of this type by the full equivalence relation. The advantage of quotienting a type is that for a dependent type B that depends on x of type A, by replacing A by its quotient, you make transports between $A[t/x]$ and $A[u/x]$ easier because $t$ and $u$ sometimes land in the same equivalence class. The disadvantage of quotienting is that some maps are easy to define with domain A, but proving that they factor through the quotient can be tedious. I'm not sure which one is better for categories.  
> **username_2**: @username_1: you are describing a situation where the *choice* of proofs is irrelevant, but the proofs themselves are still relevant (recorded). A stronger form of proof irrelevance actually deletes the proofs. Judgmental equality is like that.  
> **username_3**: Here's an interesting perspective: http://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf  
> **username_0**: I just discovered that there was an interesting discussion on the topic on the agda mailing list in November 2020 on this topic and setoids https://lists.chalmers.se/pipermail/agda/2020/012405.html  

---

## 2 answers

### Answer by username_2 on 2020-12-30. Score: 26 | Accepted answer

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

1. 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)$.
2. 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).
3. 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:

1. 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)$$
2. 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).
3. 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 "proof relevant". 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 "irrelevant" 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.

> **Comments:**
> **username_4**: I was hoping you'd show up and answer this question! I'll try to expand on the points that you decided to leave alone.  
> **username_5**: In item 3 of the second list, $p$ should be of type $P(a)$, not $A(a)$.  
> **username_2**: @AndreasBlass: fixed, thanks. By the way, everyone can edit answers.  
> **username_6**: In the "subset types" case, suppose we also had a rule $A:\text{Type},P:A\to\text{Prop} \vdash \text{pf}_{A,P}: \Pi_{a:\{x:A | P(x)\}} P(a)$.  Couldn't this be used to define $S$?  
> **username_2**: @JoshuaMeyers: Yes we could, but your suggestion make subset types equivalent to dependent sums, because $\mathrm{pf}$ is just the second projection from  $\Sigma (x : A) \, P(x)$ in disguise, so I think you managed to make the subset types equivalent to dependent sums.  
> **username_6**: The difference seems to me that whether we use $\text{pf}:P(a)$ or a distinct $\text{pf}':P(a)$, your generating rule in 3 still gives the same $a:\{x:A|P(x)\}$, and $\text{pf}_{A,P}(a)$ is not necessarily equal to either $\text{pf}$ or $\text{pf}'$.  Am I doing something incorrect?  
> **username_2**: Oh I see, you're *not* assuming the $\beta$-rules for projections, which keeps the proof opaque. Yes, that would be a reasonable way of doing it, assuming we've got some sort of proof irrelevance going on so that $\mathrm{pf}$ does not get stuck during normalization. Minor quibble: I would not use $\Pi$ to express the rule, but rather something like $$ \frac{\vdash A \;\mathrm{type} \qquad x : A \vdash P(x) : \mathrm{Prop} \qquad \vdash a : \lbrace x : A \mid P(x) \rbrace }{\vdash \mathrm{pf}(A, x.P(x), a) : P(a)} $$  
> **username_6**: So this approach seems like the **best one** to me, in the sense that it accurately represents what mathematicians do in their practice.  For example, proofs of the group axioms are not at all part of the data of a group $G$, even as an equivalence class, but opaque proofs of these axioms can be recovered from $G$ -- i.e. we can write "since $G$ is a group, associativity holds".  Do you agree?  
> **username_6**: Also btw I agree with your minor quibble, it's cleaner that way  
> **username_2**: As I said, there is trickery involved with judgemental equality when there are opaque proofs that don't compute. Are we going to just have equality checker blocking on comparison of `pf(a) ≡ p : P(a)`, or will these be automatically equal (this is known as strict `Prop`)? If they are automatically equal, then it's not so easy to have untyped normalization, and also to eliminate proofs of propositions (in particular, $\exists$-elimination is a bummer). Of course, these considerations are not appreciated by mathematicians, even though they expect their proof assistant to work well.  
> **username_6**: As a mathematician, what should I do / read in order to appreciate these concerns? Presently I don't really know why untyped normalization is important, or why opaque proofs would get in the way of $\exists$-elimination.  I don't even understand why canonicity/adequacy is important (also asking about this last point on Zulip right now)  
> **username_2**: Hmm, that's a *very* good question. I don't recall any experts writing this stuff up, they just expect PhD students to learn by osmosis. Perhaps someone else knows? What's a piece of writing directed at "normal" mathematicians that explains the relevance of proof irrelevance? (Oooh, I just got a title for a blog post.)  

---

### Answer by username_4 on 2020-12-30. Score: 15

I recommend that everyone first read username_2's answer, as he covers all the basics extremely well. I agree with everything he says in his answer. I humbly offer more comments, even though I know less on this topic than he does - but I was mentioned by name, as was my project.

When I gave a talk about agda-categories, I explained one thing about it that isn't in the paper: I am neither a proof-relevance zealot, nor was I seeking to become a proof-relevance champion. In fact, when it became clear that Agda's previous mechanism for proof irrelevance had somehow gotten quite 'broken', we simply set out to rebuild the library without using that. Jason suggested we go proof-relevant, and I decided to give it a try, mainly as an exploration of where/how things would go wrong. Much to my surprise, not only did things not go wrong, things were in fact quite smooth. The main conclusion that I draw from this is that "category theory" (note the distinct lack of **1-** there) can be proof relevant without real problems.

One take: proof relevance vs proof irrelevance is a false dichotomy. And Andrej's answer further shows that it should indeed be taken as a trichotomy. But that's not my point: you shouldn't be asking whether to choose one route or another. That is a **false choice**. What you should instead try to understand are the advantages and disadvantages of each route, and choose the route that is best suited to your current task. There is no point in asking to "globally" choose one versus the other.

It is indeed correct to point out that, strictly speaking (pun intended), agda-categories is not 1-category theory as classically envisioned. It isn't 2-category theory either, but rather feels like something "in between". By and large, it works very much like 1-category theory almost all of the time, but once in a while, things 'leak in' from 2-category theory.

I think the main lesson from agda-categories, as far as proof-relevance is concerned, is that category theory seems to largely not care. In other words, category theory is very robust and can exist largely unscathed in a variety of meta-theories, especially when you are aware of the whole topic (i.e. from $-2$-categories to $(\infty,1)$-categories to $(n,k)$-categories, enriched categories, etc). Then you see that all that changes is that some concerns move around a tiny bit, but that's it.

[Edit:] Oh, and I forgot to mention why Setoids make sense. As far as I can tell (and the nLab largely corroborates this), if you build up category theory constructively (i.e. your meta-theory does not have excluded middle or choice) starting from $-2$-categories, then enrich your way up, $0$-categories are Setoids and $1$-categories are then forcibly Setoid-enriched. You need to use various axioms to 'squish down' pieces of the $-2\ldots 1$ sequence to get the classical view. There's nothing wrong (or right!) with that. It's just a choice (ooh, another pun!) So I've come to think of Setoids here being quite natural, mostly because I'm currently happy exploring a particular part of the 'design space' of mathematics that sits inside a particular universe defined by a constructive meta-theory.


---

