17
$\begingroup$

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?

$\endgroup$
4
  • 2
    $\begingroup$ 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. $\endgroup$
    – xavierm02
    Dec 30, 2020 at 13:37
  • 1
    $\begingroup$ @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. $\endgroup$ Dec 30, 2020 at 15:33
  • 3
    $\begingroup$ Here's an interesting perspective: logic.math.su.se/palmgren-memorial/slides/… $\endgroup$ Jan 1, 2021 at 6:01
  • 1
    $\begingroup$ 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 lists.chalmers.se/pipermail/agda/2020/012405.html $\endgroup$ Jan 1, 2021 at 12:57

2 Answers 2

21
$\begingroup$

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.

$\endgroup$
12
  • 4
    $\begingroup$ 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. $\endgroup$ Dec 30, 2020 at 15:19
  • $\begingroup$ In item 3 of the second list, $p$ should be of type $P(a)$, not $A(a)$. $\endgroup$ Jan 1, 2021 at 20:12
  • $\begingroup$ @AndreasBlass: fixed, thanks. By the way, everyone can edit answers. $\endgroup$ Jan 1, 2021 at 23:58
  • $\begingroup$ 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$? $\endgroup$ Nov 23 at 3:03
  • 1
    $\begingroup$ 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)} $$ $\endgroup$ Nov 24 at 12:00
14
$\begingroup$

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.

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.