This is a question that I've puzzled about myself, and I don't pretend to have The Answer. But here's one thought that I've found illuminating. Let's start by comparing the behavior of induction and coinduction in a programming language that has them both.

Inductive datatypes are static. They store information in a particular configuration, with constructors that put that information together and destructors that inspect that information recursively. The constructors of an inductive datatype compute immediately to a value, unless they get stuck on an axiom or a variable; this is the content of "canonicity" results for type theory.

By contrast, coinductive codatatypes are dynamic. According to the modern "copattern matching" perspective on computation with codata, the constructor of a codatatype doesn't compute until a destructor is applied to it, in which case it computes only one step to expose the result and another instance of the constructor. Thus, an inhabitant of a codatatype is like an "object" in the OOP sense, which maintains an internal state (the domain of an application of the corecursor) and can be sent messages (the destructors) that return results and alter the internal state. More precisely, the return values can include versions of the object with altered state, so this is "immutable OOP".

I was first clued into this viewpoint by a remark in Conor McBride’s "Let’s see how things unfold":

As a total programmer, I am often asked ‘how do I implement a server as a program in your terminating language?’, and I reply that I do not: a server is a coprogram in a language guaranteeing liveness.

I found this remark rather cryptic at first, but recently I’ve come to appreciate it much more. In particular, I prefer this perspective on codata to its common description as "infinite objects". The infinite object underlying an element of a codatatype is essentially the trace of all possible execution paths of all possible method calls that might be applied to it in all possible sequences. This can be helpful to have in mind (particularly when constructing categorical semantics), but it has little to do with how we actually use codata. On the one hand, the "infinite object" description is static and fails to correctly describe the dynamic behavior of codata; while on the other hand, if what we *actually* care about is an infinite object, there are much more flexible and direct ways to represent them.

The simplest kind of codata is of course a stream, which corresponds to an "infinite list". But another way to represent an infinite list is with a function $\mathbb{N} \to A$. From the "static" perspective of "representing an infinite list" the two are equivalent, and the latter can even be preferable because it is more flexible in what we can do with it, and that style can represent more different kinds of infinite objects. But from a dynamic perspective, if we view a stream as a *program* that computes one result every time it is queried and moving into a new state suitable for computing the next result, then the representation as $\mathbb{N} \to A$ is terribly inefficient: every time we ask for the $n$th result, the program has to start from 0 and compute all the previous results on its way to the $n$th one, even if all those results were already computed. Can you imagine if the only way a web server could respond to a single request is by being passed, every time, the entire sequence of all the requests it had received up until that point, and replaying from square one all the calculations and updates it had to do in response to them?

Why, then, does coinduction get short shrift? From this perspective I would suggest that:

In programming, coinduction is implicitly present everywhere, particularly in object-oriented programming. But the prevalence of imperative programming languages and mutable state, which achieve essentially the same effect in an "easier" way (but without a conceptual framework and in a way that's hard to reason formally about), means that it is rarely explicitly recognized.

In mathematics, coinduction makes occasional appearances, but it is just not as useful, because mathematics (at least as it's generally done nowadays) is basically static. Apart from some constructivists and type theorists trying to change the world, mathematicians don't really care about computational interpretations of what they write; so it's natural to prefer the more flexible static representations of infinite objects over the coinductive versions that are more tailored to their computational behavior.

appearsto be somehow more general than induction, even though (I assume!) it's not? $\endgroup$definedto mean reasoning from the existence and universal properties of some terminal coalgebras. $\endgroup$syntax, we are using the foundation as a formal system to do mathematics. Thesemanticsof coinduction is provided by terminal coalgebras. You are probably confused by the fact thatinsidethe syntactical foundation you can talk about terminal coalgebras. But that's different from using the "principle of coinduction". $\endgroup$9more comments