What the differences between equivalence in HoTT and isomorphism in category？

Question

I'm new to HoTT. I can not understand equivalence in HoTT now. If prove that two types A and B are equivalent. In HoTT, I need use homotopies and find two functions g and h to show that f:A->B has a section and a retraction, satisfying the following properties: $$ \Sigma_{(g:B\to A)} f \circ g \thicksim id_B $$ $$ \Sigma_{(h:B\to A)} h \circ f \thicksim id_A $$

But in isomorphism, I only need to find two functions g' and h' to show the combinations of two functions are identity functions. Why homotopy equivalence has to use function f to define equivalence rather than like isomorphism? Is these are two perspectives of the same method? Or is there something wrong with my understanding?

Answer 1

I think your question is about the distinction between the property of being an isomorphism/equivalence, which is a property of a function $f : A \to B$, and the structure of an isomorphism/equivalence $A \simeq B$.

In the traditional, 1-categorical definition of isomorphism, we say that $f : A \to B$ is an isomorphism (or is invertible) if it has a two-sided inverse: that is, a morphism $g : B \to A$ such that $f \circ g = \mathrm{id}_B$ and $g \circ f = \mathrm{id}_A$. This is a property of $f$, in the sense that $f$ can only have at most one two-sided inverse: it can only be invertible in one way.

In HoTT, where we are dealing with higher homotopical information, this definition of isomorphism has the problem that it's not a property any more: it is possible to have types $A$ and $B$ and a function $f : A \to B$ such that the type $\text{is-isomorphism}(f)$ has two distinct inhabitants. Therefore, we use a different notion, that of equivalence: one way to define the type $\text{is-equiv}(f)$ is as the type of pairs of functions $g, h : B \to A$ such that $f \circ g = \mathrm{id}_B$ and $h \circ f = \mathrm{id}_A$. This is all explained in chapter 4 of the HoTT book, where isomorphisms as above are called "quasi-inverses" ($\text{qinv}$).

Finally, in both contexts, we say that an isomorphism (resp. equivalence) $A \simeq B$ is a function $f : A \to B$ that has the property of being an isomorphism (resp. equivalence): that is, an element of the type $\Sigma_{f : A \to B} \text{is-isomorphism}(f)$ (resp. $\Sigma_{f : A \to B} \text{is-equiv}(f)$).

Answer 2

I am adding another answer to additionally explain some claims in Naïm's answer, because one might incorrectly understand the answer as saying that a map $f$ can have two distinct inverses $g$ and $h$.

Consider a map $f : A \to B$ and suppose $g, h : B \to A$ are both inverses of $f$. Then $\mathrm{id}_A = g \circ f$, therefore $h = \mathrm{id}_A \circ h = g \circ f \circ h = g \circ \mathrm{id}_B = g$, hence $f = g$. This is a standard argument (in category theory and algebra) showing that inverses, when they exist, are unique.

In HoTT we need to be more careful and pay attention to identifications establishing the fact that something is an inverse. So let us do it again, more precisely. To say that $g : B \to A$ is an inverse of $f$ is to have three pieces of data:

1. a map $g : B \to A$,
2. an identification $p : \mathrm{id}_A = g \circ f$,
3. an identification $g : \mathrm{id}_B = f \circ g$.

Now suppose we also have:

1. a map $h : B \to A$,
2. an identification $r : \mathrm{id}_A = h \circ f$,
3. an identification $s : \mathrm{id}_B = f \circ h$.

In other words, $(g, p, q)$ and $(h, r, s)$ are elements of the type $$\textstyle\text{is-isomorphism}(f) = \sum_{k : B \to A} (\mathrm{id}_A = k \circ f) \times (\mathrm{id}_B = f \circ k).$$ We can still exhibit an identification $g = h$, like above, but to prove that $\text{is-isomorphism}(f)$ is a proposition we need to exhibit an identification $$(g, p, q) = (h, r, s).$$ And this is impossible, see the relevant chapter of the HoTT book. The intuitive way to think of this is that $f$ has at most one inverse $g$, but there may be multiple identifications $p, q$ showing that $g$ is an inverse of $f$, and this matters.

As it turns out, the definition of equivalence does not suffer from this deficiency, again, see the relevant discussions in the HoTT book.