Names For Equivalences

Names For Equivalences:

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→B a function, and consider the following additional structures.

1. A function g:B→A and homotopies ρ:fg∼1 B and σ:gf∼1 A.


2. A function g:B→A, homotopies ρ:fg∼1 B and σ:gf∼1 A, and a higher homotopy f(σ)∼ρ f.


3. Two functions g:B→A and h:B→A, and homotopies ρ:fg∼1 B and σ:hf∼1 A.


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


5. 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”.


6. 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(ρ)∼σ 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.

DIGITAL JUICE