<div dir="ltr"><div>Thanks for sharing this story, Jacques. Quite interesting reading!<br></div><div>Aaron<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Dec 16, 2020 at 4:59 PM Carette, Jacques <<a href="mailto:carette@mcmaster.ca">carette@mcmaster.ca</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div style="overflow-wrap: break-word;" lang="EN-CA">
<div class="gmail-m_-347991759044469020WordSection1">
<p class="MsoNormal">More precisely, my version of the story; my co-authors can tell their variations. This seems topical, given the recent discussion.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">But, much to our mutual surprise, things did not fail. It wasn’t even hard. One did have to be careful:<br>
- avoid strictness at all costs. Never, ever, ever, compare objects for equality. But that’s ok, so does modern category theory.<br>
- avoid heterogeneous equality at all costs. That’s ok, so does modern category theory.<br>
- explicit levels are your friends. use them, just like types, they guide you to the ‘nice’ answers.<br>
- definitional equality is important. borrow other’s variants of definitions that obey the usual symmetries definitionally.<br>
- embrace the fact that, in that setting, bits and pieces of higher category leaks in.
<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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.]<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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).<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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
<span style="font-family:"Cambria Math",serif">∘</span>-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.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">And while I’m telling a story, categorical stories without Adjoint Functors is not quite complete, right? [I’ll forgo Yoneda, this once
<span style="font-family:"Segoe UI Emoji",sans-serif">😉</span> ]. 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.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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).<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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 _<i>A</i>_ 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.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Jacques<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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.<u></u><u></u></p>
</div>
</div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>