[Agda] Tips for working around proof relevance

[Jacques Carette]

On 2020-Dec.-19 16:18 , Nicolai Kraus wrote:
>
> Univalent categories have no redundancy, and the agda-categories 
> library includes a lot of redundancy. What if we remove some 
> redundancy from agda-categories? If, for example, we remove `sym-assoc` in
> https://agda.github.io/agda-categories/Categories.Category.Core.html
> and replace all occurrences by what we get from `assoc` and the 
> witness of `IsEquivalence (_≈_)`? This would cause more work in some 
> places (judging by the comment on why `sym-assoc` was included), but 
> could all constructions still be fixed? I would expect they can, but I 
> don't think it's a priori clear. Jacques, did you find that some 
> redundancy is really required rather than just convenient in the 
> implementation?

"Required" is complicated.

The reason for sym-assoc is for definitional equality. This way C.op.op 
is definitionally equal to C. Otherwise, it is merely propositionally 
equal, and this means that some things that normally typecheck in 
category theory no longer do.  This idea first arose in Coq 
https://arxiv.org/abs/1401.7694 (published in ITP 2014) in work of 
Gross, Chlipala and Spivak.  Without this, quite a few things end up 
needing noisy trivial isomorphisms inserted, and higher category theory 
gets ugly, when it shouldn't.

Basically: if you believe that Duality is something that is core to 
category theory, and that this should be reflected by a lot of 
double-duals being definitionally true (not just 'op' on categories, but 
for many other categorical constructions), then this redundancy is 
something you want.

That is one slight cost of being proof-relevant. In practice, because of 
our "smart constructors", end-users are not affected by this, unless 
they blindly let Agda expanded out the needed records instead of taking 
a second to ponder how to best build things.

We believe that it is "required", in the sense that this way our 
statements of most of category theory look very familiar, i.e. 
correspond closely to what is in textbooks. It is not required in the 
sense that it would be possible to force things to work without them, at 
the cost of more and more constructions looking noisy.

Not that they would be wrong. A better way to look at it would be that 
much more of higher category theory would "leak down" without that 
redundancy.

Jacques