# Equivalence in $\infty$-categories

In every $n$-category (weak or strict) can be defined the concept of equivalence via a recursive definition: * an equivalence in a set ($0$-category) is just an identity; * for each $n \in \mathbb N$ an equivalence between two object (or $0$-cell), let say $a$ and $b$, in a $n+1$-category is just a $1$-cell $f \colon a \to b$ such that exist a $1$-cell $g \colon b \to a$ and two $2$-cells $\alpha \colon g \circ f \to 1_a$ and $\beta \colon f \circ g \to 1_b$ which are equivalence into the $n$-categories $\hom(g\circ f, 1_a)$ and $\hom(f \circ g, 1_b)$ respectively. There is a good formal definition of equivalence also for $\infty$-category?

-

For some precise definitions and results, see this paper by Eugenia Cheng.

-
To be honest, I think that paper is seriously misleading. Her "Unsound definition" 5 is actually a perfectly sound definition; you just have to interpret it coinductively. Unfortunately, coinductive definitions don't seem to be as widely known as inductive ones. – Mike Shulman Jun 8 '11 at 16:25
That's interesting. But offhand, "seriously misleading" sounds like a pretty strong way to put it, as if the paper is invalid somehow. (I believe the paper predates Eugenia's involvement with corecursive definitions of $\infty$-categories. Aside from the label "unsound definition", is there anything actually wrong with the paper?) – Todd Trimble Jun 8 '11 at 17:57
I'm sorry if I came on too strong. I didn't mean to say there was anything wrong with the paper; it's a very nice paper overall! I just meant that specifically in the context of the question "how to define equivalences in &infin;-categories?", I think it is a misleading reference to give. To my mind, the best definition is actually the coinductive one, which that paper asserts to be unsound. – Mike Shulman Jun 19 '11 at 22:46
Ouch. :-) Could you provide a better reference, then? – Todd Trimble Jun 19 '11 at 23:12
I hope that Eugenia, if she is reading this, won't take offense at my comment. The fact that coinductive definitions are meaningful seems generally to be a secret well-kept by computer scientists and rarely taught to mathematicians. I only fairly recently learned it myself. In fact I learned it by reading a coinductive definition of infinity-equivalence, thinking "that's nonsense", and going to look it up and finding out that it wasn't! – Mike Shulman Jun 20 '11 at 3:32

A concise coinductive definition can be found, for the case of strict ∞-categories, in the paper "A folk model structure on omega-cat", arXiv. This can be unraveled in order to become equivalent to Eugenia's more explicit version.

-
This is very interesting! Presumably you can unroll the coinduction to make a definition in terms of the existence of an infinite binary tree of higher morphisms (although I don't know if this is a useful thing to do). – S. Carnahan Jun 20 '11 at 10:20
Yes, as I said, this version can be unraveled into Eugenia's. Perhaps (probably?) for some applications this would be useful. – Mike Shulman Jun 20 '11 at 22:06