--- title: The Complete History of isoToEquiv date: December 17th, 2021 --- # What's isoToEquiv? It's a standard fact in (higher) category theory and homotopy theory that any equivalence of categories (homotopy equivalence) can be improved to an _adjoint_ equivalence of categories (strong homotopy equivalence). Adjoint equivalences (and strong homotopy equivalences) are "more structured" notions in the sense that the data of an adjoint equivalence is _contractible if inhabited_. In Homotopy Type Theory, the notion of (half) adjoint equivalence lets us split the type $A \simeq B$ into _structure_ and _property_: the structure is a function $A \to B$, and the property is "being an equivalence". This is in contrast to the type of _isomorphisms_ $A \cong B$, which are the _structure_ of maps $f : A \to B$ and $g : B \to A$ together with homotopies $f \circ g \sim \mathrm{id}$ and $g \circ f \sim \mathrm{id}$. Notably, the type of "isomorphism data" for a particular function is [not always a proposition], whereas [being an equivalence is]. [not always a proposition]: https://cubical.1lab.dev/1Lab.Counterexamples.IsIso.html [being an equivalence is]: https://cubical.1lab.dev/1Lab.Equiv.html#isProp-isEquiv Recently, I've been working on [the 1Lab], an open-source, formalised and explorable resource for univalent mathematics. This means that, among other things, I had to write an explanation for [the proof that isomorphisms can be made into equivalences][1], i.e., the map `isoToEquiv`. Our proof comes essentially from [the Cubical Agda library], where it is presented with a single comment: ```agda -- Any iso is an equivalence ``` That's helpful. So where does it come from? [the 1Lab]: https://cubical.1lab.dev [1]: https://cubical.1lab.dev/1Lab.Equiv.html#equivalences-from-isomorphisms [the Cubical Agda library]: https://github.com/agda/cubical/blob/22bea9586b67fa90cf90abea04360080d369c68c/Cubical/Foundations/Isomorphism.agda#L53-L112 # Where it comes from Since _I_ know where I got it from, I knew where to start looking. On the Git log of the Cubical Agda library, we find that the Cubical Agda version of `isoToEquiv` was added in [October 31, 2018] by Anders Mörtberg, with the same handy comment and no attribution. It's reasonable to assume, then, that Mörtberg proved it himself right then and there. However, the HoTT book, published in 2013, already has a proof that any isomorphism data can be "strengthened" into equivalence data, so it seems unreasonable to assume that the first time this was formalised was 2018. Fortunately, we're not dead in the water. [October 31, 2018]: https://github.com/agda/cubical/commit/e139a6f09ea59da2032be8ebaf07e8b5fc8bc0c4 The Cubical Agda implementation of `isoToEquiv` comes from [cubicaltt], an older, prototype implementation of cubical type theory. Looking at _that_ Git history, we find that it was added by.. Mörtberg again! This time on [January 4, 2016], over two years prior. Again, there is no attribution, and this is the oldest implementation of cubical type theory, so it's reasonable to assume that this is where the proof originates, right? Wrong. [cubicaltt]: https://github.com/mortberg/cubicaltt/blob/a5c6f94bfc0da84e214641e0b87aa9649ea114ea/examples/equiv.ctt#L177-L225 [January 4, 2016]: https://github.com/mortberg/cubicaltt/commit/26b70046ce7e45197f14ead82daae7e0354e9945 # The name "gradLemma" If you look at the commit that originally introduced a proof that `isIso f → isEquiv f` to cubicaltt, you'll see that the map _wasn't_ named `isoToEquiv`, it was named `gradLemma`. This name is _especially_ unhelpful, [quoting Mike Shulman]: [quoting Mike Shulman]: https://github.com/mortberg/cubicaltt/issues/72 > Generally there are two ways that theorems and lemmas are named in > mathematics: descriptively (giving some information about what the > theorem says, e.g. "the intermediate value theorem") and attributively > (giving credit to whoever proved it, e.g. "Cauchy's theorem"). Whatever > your feelings about the relative merits of the two, the name "grad > lemma" achieves neither: it conveys no information about what the lemma > says, nor does it give any credit to the people it refers to, instead > depersonalizing them as "some nameless graduate students". Moreover it > is even factually incorrect, since some of the people in question were > actually postdocs at the time. Shulman is right! The name is depersonalizing, and it does not credit the people who originally came up with the proof. So who _are_ they? Where does this proof come from? Well, reading the rest of those GitHub issues, we learn two things: 1. Mörtberg did not come up with the proof out of thin air, though as far as I can tell he was the first to adapt it to a direct cubical argument; 2. The name "gradLemma" comes from UniMath. # UniMath UniMath (**uni**valent **math**ematics) is the second oldest library for Homotopy Type Theory in a proof assistant, and the oldest actively maintained. It was, in fact, originally written by Voevodsky himself! Thus, it comes with its own proof of `isoToEquiv`, which we find [in the massive file `Foundations/PartA.v`][3]: [3]: https://github.com/UniMath/UniMath/blob/f9645aeb354f34f0841cb796e33ccc0a5cba1d67/UniMath/Foundations/PartA.v ``` (** This is kept to preserve compatibility with publications that use the name "gradth" for the "grad theorem". *) Definition gradth {X Y : UU} (f : X -> Y) (g : Y -> X) (egf: ∏ x : X, g (f x) = x) (efg: ∏ y : Y, f (g y) = y) : isweq f := isweq_iso f g egf efg. ``` Good to know that at least the theorem isn't _called_ "grad theorem" anymore, but there are still many references to `gradth` in the codebase. By the way, the name `isweq_iso`? [Changed by Mörtberg]! It's him we have to thank for introducing the _useful_ name `isweq_iso`, and the corresponding `isoToEquiv`. Thank goodness we don't call it "grad theorem" anymore. [Changed by Mörtberg]: https://github.com/UniMath/UniMath/pull/848 But wait, the name "grad theorem" refers to *grad*uate students.. And graduate students are _people_.. So who are these people? Let's keep digging. The README to UniMath mentions that it is based on a previous library, [Foundations]: [Foundations]: https://github.com/UniMath/Foundations > The UniMath project was started in 2014 by merging the repository > Foundations, by Vladimir Voevodsky (written in 2010), \[...\] I'll cut to the chase: The history of `gradth` ends with foundations; It's been there since [the initial commit]. This means that the trail has run cold. Voevodsky certainly wasn't a grad student in 2010, he was a fields medalist! Mörtberg didn't name the theorem either. And so, I kept digging. I started looking for sources other than code: talks, papers, theses, etc. # An unlikely source [the initial commit]: https://github.com/UniMath/Foundations/commit/d56271180c00a8a545c29db06001ae71a910c1b1#diff-ba65cad07cb794c06ab63e0e04dc95d785fee1374791ea974099e355ff20ff7bR433-R439 I found a handful of papers ([here] [are] [some]) which refer to this result as "the graduate theorem", but none of them mentioned _who_ the graduate students are. However, I did find a source, however unlikely. [here]: https://arxiv.org/pdf/1809.11168.pdf [are]: https://arxiv.org/pdf/1401.0053.pdf [some]: https://arxiv.org/pdf/1210.5658.pdf In 2011, Mike Shulman wrote [a series of posts] introducing the $n$-category café to the ideas of homotopy type theory. In this post, Shulman mentions the notion of equivalence following Voevodsky, but he also mentions the notion of [half-adjoint equivalence], and mentions where it comes from: > This other way to define $\mathrm{IsEquiv}$ should be attributed to a > handful of people who came up with it a year ago at an informal > gathering at CMU, but I don’t know the full list of names; maybe someone > else can supply it. [a series of posts]: https://golem.ph.utexas.edu/category/2011/03/homotopy_type_theory_ii.html [half-adjoint equivalence]: https://cubical.1lab.dev/1Lab.Equiv.HalfAdjoint.html Now, as Shulman says, he does not know the full list of names. However, Steve Awodey does, [as is stated in a comment]: > Let’s see: Mike Shulman, Peter Lumdaine, Michael Warren, Dan Licata – > right? I think it’s called “gradlemma” in VV’s coq files (although only > 2 of the 4 were actually still grad students at the time). [as is stated in a comment]: https://golem.ph.utexas.edu/category/2011/03/homotopy_type_theory_ii.html#c037120 However, note the use of "right?" - this comment isn't a primary source (Awodey wasn't involved in coming up with the graduate lemma), and it's not even certain on top of that. However, you know what would be a primary source? Someone who was there. And you know who follows me on twitter? [Dan Licata]. [Dan Licata]: https://twitter.com/admitscut/status/1472014521673859072 # The Complete History of isoToEquiv With this, we have a full picture of the history of isoToEquiv, albeit with a handful of details still fuzzy. Here's a timeline: * (2010-??-??) Mike Shulman, Peter Lumsdaine, Michael Warren and Dan Licata come up the notion of half-adjoint equivalence in homotopy type theory, and adapt a standard result from category theory to show that any isomorphism improves to a half-adjoint equivalence. **This is the origin of `isoToEquiv`**; The "grad" in "grad theorem" refers to Licata and Lumsdaine, who were graduate students at the time. * (2010-10-04) Vladimir Voevodsky makes the first commit of Foundations, where `isoToEquiv` is present - under the name `gradth`. Nowhere in the repository, its entire history, or anywhere in Voevodsky's works are the grads from the th mentioned. There are no git logs that can trace the history of `isoToEquiv` before this point. * (2014-03-21) Foundations becomes UniMath, and the name `gradth` is kept. This is the first “leap” in the history of `isoToEquiv`, the first non-trivial historical path. * (2016-01-04) Mörtberg adapts the proof of `gradth` from UniMath to his experimental implementation of Cubbical Type Theory, which at the time was brand new. There, the result is called `gradLemma`. As far as I can tell, this is the origin of the code for `isoToEquiv` that can still be found, alive and kicking, in the Cubical library (and the 1lab) to this day. I've emailed Mörtberg to set the record straight, but I'm writing this at 11:00pm on a Friday, so I still haven't heard back. I'll update the post when (and if) he replies. * (2017-08-11) Mike Shulman files an issue in the cubicaltt repository complaining about the name `gradLemma`. Mörtberg addresses the issue by renaming it to `isoToEquiv`. * (2018-10-30) Mörtberg ports `isoToEquiv` from cubicaltt to Cubical Agda, which is where I stole it from. I am in no position to speculate as to _why_ Voevodsky did not credit Licata, Lumsdaine, Shulman and Warren with `gradth`, or why he chose a name that mentions the existence of graduate students without naming the students. It feels like a great misstep in the history of our community that such a fundamental result was never properly accredited. While the Wikipedia page for Homotopy Type Theory has mentioned Licata, Lumsdaine, Shulman and Warren as the authors of the proof [since 2014], _none_ of the primary sources I consulted - the Foundations repo, the UniMath repo, the cubicaltt repo, the Cubical Agda repo, or _any_ of the associated papers - do. [since 2014]: https://en.wikipedia.org/w/index.php?title=Homotopy_type_theory&diff=prev&oldid=638938391 I'm glad the name `gradth` is no longer in widespread usage (outside of UniMath, which has neglected to remove the deprecated name). If we were to name it after people, it should be called the Licata-Lumsdaine-Shulman-Warren Theorem, and that's unwieldy. Let's stick with `isoToEquiv`, but acknowledge where it comes from. I know this post isn't what I usually write - I'm not a historian, after all - so thanks for reading it. I wanted to chronicle how I spent the afternoon and evening of a Friday in December 2021: Chasing the ghost of proper attribution. I'm probably not going to write any technical content on this blog for a while yet; I might write a short announcement of the 1lab, which otherwise takes up all of my spoons.