[Agda] agda-categories, a story

[Carette, Jacques]

More precisely, my version of the story; my co-authors can tell their variations. This seems topical, given the recent discussion.

I had been co-maintainer of copumpkin’s library. We managed to keep it alive until agda 2.4.3 and limping in 2.4.4.  After that, it broke completely – irrelevance had changed, and things did not seem easily repairable. I tried to use the new Prop instead, but it was too new, and that just did not work.

Jason Hu then proposed that we rewrite it, from scratch, to be proof-relevant. And in compatible-with-most-extensions MLTT, so enabling –safe and  –without-K too.  Cubical was then way too new and experimental, and ‘main’ Agda still needed a proper category theory library.

I was quite convinced that that effort would be doomed to fail. However, I was extremely curious as to why/where. I figured it wouldn’t take long to encounter some unsurmountable roadblock, I would learn something cool in that failure, and move on. I had been in “Setoid hell” before, and it was quite unpleasant indeed. subst-hell, however, is considerably worse, but that’s another story.

But, much to our mutual surprise, things did not fail. It wasn’t even hard. One did have to be careful:
- avoid strictness at all costs. Never, ever, ever, compare objects for equality.  But that’s ok, so does modern category theory.
- avoid heterogeneous equality at all costs. That’s ok, so does modern category theory.
- explicit levels are your friends. use them, just like types, they guide you to the ‘nice’ answers.
- definitional equality is important. borrow other’s variants of definitions that obey the usual symmetries definitionally.
- embrace the fact that, in that setting, bits and pieces of higher category leaks in.

And we ended up building the largest, in terms of number of concepts and theorems, category theory library in any proof assistant. [See the paper for the details of that.  A preprint is on the arxiv, it’s been accepted to CPP 2021.  Though Lean might surpass us soon on sheer size.]

Some things work out really, really nicely. For example, a Bicategory is defined as a category-enriched category with 2 extra coherence laws. Very simple. Compare to the ‘expanded’ definition on the nLab (or in other’s libraries).

The setting also saved me at least once: I foolishly believed the too-naïve version of the Grothendieck construction that’s on Wikipedia and tried to implement it. And it worked… except for that most pesky of Setoid-induced law ∘-resp-≈. Because, well, it’s false. Because the Grothendieck construction really doesn’t work on the 1-categorical level, it really really does need a Pseudofunctor. The nLab, as usual, saved the day.

And while I’m telling a story, categorical stories without Adjoint Functors is not quite complete, right? [I’ll forgo Yoneda, this once 😉 ]. There are, in the literature, multiple definitions of adjointness, and proofs of their equivalence. The good proofs have weasel words here and there about size issues. Here, Agda shines: the normal encoding of all the definitions ‘work’, but the most elegant definition (Hom isomorphism) is not level polymorphic, while the unit-counit definition is! This was quite shocking. There are a few other definitions in CT that are like that too, where only one of the various definitions is fully level-polymorphic. I think this betrays the fact that most of CT was worked out in a set-theoretic meta-theory, where universe sizes are not first-class.

Personally, I am a big fan of the “mathematics multiverse” (thanks for Andrej Bauer for the phrasing), where one ought to explore what mathematics looks like in different meta-theories. I kind of like poking around in various bits of it, whether it’s fashionable or not.  Some math, such as category theory, seems remarkably robust with respect to changes in meta-theory (within reason).

So, for all who have managed to read this far: do I think that this is THE way to build category theory in Agda? No! It is _A_ way. A perfectly fine, surprisingly workable way. Would it be how I would build it in cubical Agda? Absolutely not! That would seem rather perverse.

Jacques

PS: Categories with Families. Those have stumped me in this setting. At least, Pi-types in that setting have. It’s subst-hell all over again. I’m going to wait until someone does Bicategories with Families, or whatever a proper 2-categorical equivalent is.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201216/50a4acd8/attachment.html>