### Coinductive Definitions

#### Posted by Mike Shulman

I’ve come to believe, over the past couple of years, that anyone trying to study $\omega$-categories (a.k.a. $(\infty,\infty)$-categories) without knowing about coinductive definitions is going to be struggling against nature due to not having the proper tools. But although coinductive definitions are a basic notion in mathematics, for some reason they don’t seem to be taught, even to graduate students. Write something like

A 1-morphism $f\colon x\to y$ in an $(n+1)$-category is an

equivalenceif there exists a 1-morphism $g\colon y\to x$ and equivalences $1_x \to g f$ and $f g\to 1_y$ in the relevant hom-$n$-categories; and every 1-morphism in a 0-category is an equivalence

and any mathematician (who has some inkling of what $n$-categories are) will be happy. If you ask why this definition isn’t circular, since it defines the notion of “equivalence” in terms of “equivalence”, the mathematician will say “it’s an inductive definition” and expect you to stop complaining. But if you write something like

A 1-morphism $f\colon x\to y$ in an $\omega$-category is an

equivalenceif there exists a 1-morphism $g\colon y\to x$ and equivalences $1_x \to g f$ and $f g\to 1_y$ in the relevant hom-$\omega$-categories

the same mathematician will object loudly, saying that this definition is circular. (In fact, not very long ago, that mathematician was me.) But actually, this latter is a perfectly valid *coinductive* definition.

One way of saying what an inductive definition means is that it defines the *smallest* class of things that is closed under some “constructor” operations. That is, the above definition of equivalences in $n$-categories for finite $n$ says, when unraveled a bit, that the class of “equivalences in $n$-categories” is the smallest class $\mathcal{E}$ such that

- Every morphism in a 0-category is in $\mathcal{E}$, and
- If $f\colon x\to y$ has the property that there exists $g\colon y\to x$, and also morphisms $1_x \to g f$ and $f g\to 1_y$ that are in $\mathcal{E}$, then $f$ is in $\mathcal{E}$.

As usual, “smallest” means “minimum”, i.e. it is contained in every other such class $\mathcal{E}$. How do we know that there is a smallest such class? Because of the nature of the closure conditions (each of them takes some input consisting of things in $\mathcal{E}$ and produces something else in $\mathcal{E}$), the collection of classes $\mathcal{E}$ satisfying them is closed under intersection; thus we can take the intersection of all such $\mathcal{E}$ to obtain the smallest one.

Inductive definitions are best-adapted to proving stuff *about* things which satisfy the definition. Namely, if we want to prove that all equivalences in $n$-categories have property $P$, all we need to do is prove that morphisms in 0-categories have property $P$, and (2) given $f\colon x\to y$ and $g\colon y\to x$, and $1_x \to g f$ and $f g\to 1_y$ with property $P$, also $f$ has property $P$. Then the class of things satisfying $P$ will be one of the classes $\mathcal{E}$, and hence contain the class of equivalences. This is called a *proof by induction*.

Dually, a *coinductive* definition defines the *largest* class of things that is closed under some “destructor” operations. Thus, the above definition of equivalences in $\omega$-categories says that the class of “equivalences in $\omega$-categories” is the largest class $\mathcal{E}$ such that

- If $f\colon x\to y$ is in $\mathcal{E}$, then there exists a $g\colon y\to x$, and also morphisms $1_x \to g f$ and $f g\to 1_y$ that are in $\mathcal{E}$.

As usual, “largest” means “maximum”, i.e. containing every other such class $\mathcal{E}$. How do we know that there is a largest such class? Because of the nature of the closure conditions (each of them takes *one* input in $\mathcal{E}$ and produces some number of other things in $\mathcal{E}$), the collection of classes $\mathcal{E}$ satisfying them is closed under unions; thus we can take the union of all such $\mathcal{E}$ to obtain the largest one.

Coinductive definitions are best-adapted to proving that things *do* satisfy the definition. Namely, if we want to prove that some morphism $f$ in an $\omega$-category is an equivalence, all we need to do is prove that $f$ belongs to some class $\mathcal{E}$ of morphisms with the above property. Then $\mathcal{E}$ will be contained in the class of equivalences, so that $f$ is an equivalence. This is called a *proof by coinduction*.

The theory of $\omega$-categories is full of concepts that are naturally defined coinductively. For instance:

A functor $f\colon C\to D$ between $\omega$-categories is an equivalence if (1) for each $y\in D$, there exists an $x\in C$ and an equivalence $f(x) \to y$, and (2) for each $x_1,x_2\in C$, the functor $f\colon C(x_1,x_2) \to D(f(x_1),f(x_2))$ is an equivalence between $\omega$-categories.

The schematic definition of n-fibration makes perfect sense as a definition of $\omega$-fibration, if interpreted coinductively.

In fact, $\omega$-categories themselves are naturally defined coinductively!

- An $\omega$-category is a category enriched over $\omega$-categories.

This requires a more general kind of coinductive definition, though, since now we are defining a *structure* coinductively, rather than a *property* of elements of some existing structure.

Here’s a way of rephrasing the inductive definition of equivalences in an $n$-category. Consider the poset of “classes of morphisms in $n$-categories” for finite $n$, and given such a class $\mathcal{E}$, let $F(\mathcal{E})$ be the class of all morphisms which are either (1) morphisms in 0-categories, or (2) are morphisms $f\colon x\to y$ such that there exists $g\colon y\to x$, and also morphisms $1_x \to g f$ and $f g\to 1_y$ that are in $\mathcal{E}$. Then $F$ is an endofunctor of this poset, and the inductive definition says that the equivalences are the *initial algebra* for this endofunctor, i.e. the smallest $\mathcal{E}$ such that $F(\mathcal{E})\subseteq \mathcal{E}$.

Similarly, we can consider the poset of “classes of morphisms in $\omega$-categories” and define $G(\mathcal{E})$ to be the class of all morphisms $f\colon x\to y$ such that there exists a $g\colon y\to x$, and also morphisms $1_x \to g f$ and $f g\to 1_y$ that are in $\mathcal{E}$. Then the coinductive definition says that $\mathcal{E}$ is the *terminal coalgebra* for the endofunctor $G$, i.e. the largest $\mathcal{E}$ such that $\mathcal{E}\subseteq G(\mathcal{E})$.

The generalization to structure, rather than properties, is now immediate: in general, an inductively defined gadget is an initial algebra for some endofunctor, and a coinductively defined gadget is a terminal coalgebra for some endofunctor. Of course, we need some conditions on the endofunctor to ensure that initial or terminal coalgebras exist; usually one asks them to be polynomial.

For instance, the natural numbers are the initial algebra for the endofunctor $X\mapsto X+1$ of $Set$. This automatically gives us the principle of definition by iteration or recursion.

Similarly, we can exhibit $\omega$-categories as the terminal coalgebra for an endofunctor of a suitable category. The above coinductive definition suggests that the endofunctor in question should take $C$ and output the collection of $C$-enriched categories. Thus, $C$ must belong to a category of “things we can enrich over.” If we take our endofunctor to live on the category of cartesian monoidal categories (or, I think, even all symmetric monoidal categories), and use the usual notion of enrichment, then we obtain as terminal coalgebra the category of strict $\omega$-categories. And Eugenia and Tom showed here that if we use Todd Trimble’s notion of operadic iterated enrichment, then we obtain a Trimblean model for weak $\omega$-categories.

## Re: Coinductive Definitions

Nice post! I occasionally run into computer sciencey types who fling around coinduction with gay abandon, and I admit that it makes me a bit nervous. It probably comes down to a lack of practice.