[Agda] agda-categories, a story

[Aaron Stump]

Thanks for sharing this story, Jacques.  Quite interesting reading!
Aaron

On Wed, Dec 16, 2020 at 4:59 PM Carette, Jacques <carette at mcmaster.ca>
wrote:

> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201216/35d9de87/attachment.html>