The n-Category Café

I’m wondering now[ w]hether I’ve quite grasped the distinction between coinduction and corecursion.

I'd say yes. But I'd also warn anybody that the distinction between ‘induction’ and ‘recursion’ (and their duals) is not always observed in the literature.

There are actually three levels here. We produces proofs by (co)induction; that is, we define (which amounts to establishing the existence of, since they are necessarily unique) elements of a truth value. By (co)recursion, we define elements of a set, most fundamentally elements of a hom-set into a final coalgebra or out of an initial algebra. And then we can also define (co)inductive types, which are objects of a category.

Many people say ‘induction’ for all $3$ levels. Many people say ‘induction’, ‘recursion’, and then ‘induction’ again, while many people say ‘induction’, ‘recursion’, and then ‘recursion’ again. I'm inclined to say (which I just thought of, but now it looks obvious) to say ‘induction’, ‘recursion’, and ‘$2$-recursion’.

For example, give the polynomial $X \mapsto X + 1$, we rely on abstract nonsense to assure us that the category of sets has an initial algebra for this endofunctor; in this way, we $2$-recursively define the set $\mathbf{N}$ of natural numbers. Then when we run across some algebra $A$ for this endofunctor, such as a metric space equipped with a point (the theorem that you cite doesn't hold for the empty space) and a contractive endomap, we recursively define an algebra homomorphism $r$ from $\mathbf{N}$ to $A$. Then when we run across some algebra homomorphism $f$ from $\mathbf{N}$ to $A$, we inductively (or $0$-recursively) conclude that $f$ equals $r$.

A couple of things I’m wondering now. Whether I’ve quite grasped the distinction between coinduction and corecursion. From what I wrote there, this might seem better described as a ‘corecursive rule for complete metric spaces’. Please modify those nLab entries as necessary.

What you wrote in the nLab entry sure looks right to me. My only comment there is that you’ve generalized the quaternity “induction: coinduction :: recursion: corecursion” beyond the strictures of their usual meanings. For example, ordinary induction says that an $F$-subalgebra of the initial $F$-algebra $\mathbb{N}$ is $\mathbb{N}$ itself, where $F: Set \to Set$ takes $S$ to $1 + S$. But the same principle applies to an initial algebra of any endofunctor $F$ on any category, and this is a generalized meaning of ‘the induction principle’. And dually for ‘coinduction’, just in the way you’ve written it.

That said, it also seems okay to me for the authors to refer to the argument as an instance of coinduction. If the argument is that every coalgebra contains this fixed point $u$, then the terminal coalgebra $T$, constructed very softly as the join

$$T = \bigvee_{\emptyset \neq S \leq \overline{H}(S)} S$$

in the power set $P(X)$ under reverse inclusion, is nonempty, because it contains $u$. In other words, $T \leq \{u\}$, so $u$ is a coalgebra quotient of $T$ (with respect to $\leq$), hence must be equal to $T$ by the coinduction principle as you’ve written it.

And second, relating to my current interest in ‘symmetry breaking’ in mathematics, couldn’t Kozen and Ruozzi have defined their category $C$ to be nonempty closed subsets of $V$ with inclusions as morphisms? Then $\{u^*\}$ would have been the initial algebra of $\overline{H}$, and all would go through as before, producing an ‘inductive rule for complete metric spaces’.

Absolutely. In fact, this statement is the precise formal dual of what they have! (And maybe easier to grasp this way.)