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.

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, i.e., the map isoToEquiv. Our proof comes essentially from the Cubical Agda library, where it is presented with a single comment:

-- Any iso is an equivalence

That’s helpful. So where does it come from?

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.

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.

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:

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 (univalent mathematics) 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:

(** 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.

But wait, the name “grad theorem” refers to graduate 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:

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

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.

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.

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).

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.

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.

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.