<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-CA" link="#0563C1" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">More precisely, my version of the story; my co-authors can tell their variations. This seems topical, given the recent discussion.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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.
<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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.]<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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).<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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).<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Jacques<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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.<o:p></o:p></p>
</div>
</body>
</html>