I believe the original post asked what coalgebras might be good for. Dusko Pavlovic already talked about examples of coinduction in analysis. Let me mention two examples from constructive mathematics. They are both examples of final coalgebras for polynomial functors. A polynomial functor P_f with signature f: B --> A is a functor of the form P_f(X) = \sum_{a \in A} X^{f^{*} a} where \sum is a dependent sum, and f^{*} is the inverse image of f. For the purposes of this post you can think of a polynomial functor as one of the form P(X) = C_0 + C_1 x X^{N_1} + ... + C_k x X^{N_k} where C_0, ..., C_k and N_0, ..., N_k are (constant) objects. Suppose we are in a constructive setting (a variant of Martin-Lof type theory, effective topos, a PER model, ...) in which every polynomial functor has a final coalgebra. Example 1: In constructive mathematics _spreads_ and _fans_ play an important role. They are examples of final coalgebras. For example, a fan is a finitely branching tree (can be infinite!) in which the nodes are labeled with natural numbers. The space of all fans FAN satisfies the identity FAN = N + N x FAN + N x FAN^2 + N x FAN^3 + ... = sum_{k \in N} N x FAN^k it is the final coalgebra for the polynomial functor P(X) = \sum_{k \in N} N x FAN^k I find this presentation conceptually cleaner than the usual encoding of spreads as sets of Goedel codes of finite sequences of natural numbers (of course, this presentation requires a richer type theory). Also, this definition is easily adapted to fans and spreads labeled by elements of any set A (just replace N x FAN^k with A x FAN^k), and of any branching type. By the way, FAN is isomorphic to N^N, and N^N is the final coalgebra for the functor P(X) = N x X. Example 2: The initial algebra for P(X) = 1 + X is the set of natural numbers. The final coalgebra N^+ for this functor is best thought of as the one-point compactification of the natural numbers, as it consists of the natural numbers together with one extra point "at infinity". In classical set theory, this is no different from natural numbers, but in a constructive setting the point at infinity is not isolated. If one wants to prove anything interesting about N^+, just about the only way to do it is to use coinduction and corecursion. It's a good exercise. This is neat because we get a one-point compactification of N without any reference to topology. If we compute N^+ in PER(D), where D is some topological model of the untyped lambda calculus, such as P(omega) or the universal Scott domain, we get _precisely_ the one-point compactification of natural numbers. In the effective topos N^+ can be described as an equivalence relation on partial recursive functions, where two such functions are equivalent if, and only if, they terminate in the same number of steps (when applied to some fixed input) or they diverge. The divergent functions represent the point at infinity, and those terminating in exactly k steps represent the number k. Andrej