### Names For Equivalences

#### Posted by Mike Shulman

Homotopy type theory has a problem: we need names for a bunch of slightly different kinds of “equivalences”. Until now, we’ve been muddling along with some fairly ad hoc choices. Can you help think of better names?

Hardly any knowledge of type theory is necessary in order to help. Just read on…

In the world of type theory, we have things called *types*, which are kind of like sets and kind of like groupoids and kind of like spaces. We also have *functions* or *maps* between types, and *homotopies* between functions, and higher homotopies and so on. Moreover, we can also make *logical statements* about types and their elements, as if they were sets or spaces, and these logical statements can be interpreted in a canonical way as specifying certain data.

Let $A$ and $B$ be types and $f:A\to B$ a function, and consider the following additional structures.

A function $g:B\to A$ and homotopies $\rho : f g \sim 1_B$ and $\sigma : g f \sim 1_A$.

A function $g:B\to A$, homotopies $\rho : f g \sim 1_B$ and $\sigma : g f \sim 1_A$, and a higher homotopy $f(\sigma) \sim \rho_f$.

Two functions $g:B\to A$ and $h:B\to A$, and homotopies $\rho : f g \sim 1_B$ and $\sigma : h f \sim 1_A$.

The assertion that every homotopy fiber of $f$ is a contractible space (= type).

The assertion that every fiber of $f$ is a singleton. A type $S$ is called a singleton if “there exists an $s_0$ in $S$, and for all $s$ in $S$ we have $s=s_0$”.

The assertions that $f$ is both surjective (“for every $b$ in $B$, there exists an $a$ in $A$ such that $f(a)=b$”) and injective (“if $f(a) = f(a')$, then $a=a'$”).

The question is, what names would you give to each of these notions? Before you answer, however, some remarks are in order.

Firstly, (4) and (5) are actually identical. But I’ve stated them separately in case the different phrasings suggest different names to your mind.

Secondly, all of these notions are “logically equivalent” in the sense that given the data in any one of them, you can construct the data in any other. However, not all of them are on an equal footing homotopically. In particular, (1) and (6) are poorly behaved, and to be eschewed. More precisely, if the data specified in any (hence all) of these notions exists, then each collection of data (2), (3), (4), and (5) is itself a contractible space, whereas this is not true of (1) and (6).

For this reason, I would like to avoid applying convenient and familiar words to (1) and (6), because we don’t use them very much, so it would be a waste of a good word. On the other hand, we don’t want to choose names in a way that will be unnecessarily confusing to newcomers, either.

Thirdly, the seeming asymmetry in (2) is an illusion: it would be equivalent to ask for a higher homotopy $g(\rho) \sim \sigma_g$ instead. (But if we asked for *both*, then we would get something ill-behaved like (1) and (6), unless we also asked for one tertiary homotopy.)

There are words for some of these notions that we’ve been using in homotopy type theory for the past year or two. However, they were chosen in a sort of ad hoc way, and right now we’re overhauling the HoTT Coq library, so we have a chance to try to improve the common terminology. Hence, I’m not going to mention yet what the words are that we have been using. If you happen to know, try to forget, and look at the definitions afresh.

## Re: Names For Equivalences

Hmmm… just as the things themselves, 3 is just that $f$ has a section and a retraction; 1 is that $f$ has an equal section and retraction; since $f$ having both a section and a retraction already implies there is a canonical homotopy between them, 1 therefore means a section and a retraction and an

extrahomotopy between them; 2 is a 1 with … a contraction of something? Off the top of my head I can’t tell what, just because the datum is in the wrong space for my intuition; though of course mapping back by the inverse equivalence should fix that for me. But this is what you were calling “adjoint equivalence” before, yes? 4/5 of course … “has contractible fibers” is really quite straightforward. 6 sounds dangerous, just because I can’t tell whether you meanmerelyexisting or what. It seems to me it might be interpretable as a component bijection, though that’s surely not what you intend here.Anyways, I therefore prognosticate

Or at least, that’s a quick slap-dash and idiosyncratic assignment of names which just as likely won’t help anyone.