Hi all, although I cannot say much on coinduction itself, I would like to mention one possible point of view on "universal coalgebra" commented on by Dusko at the end of his message:
PS i have a great appreciation for jan rutten's work on coinduction, but it seems to me that the title of *universal coalgebra* is a bit exaggerated. universal algebra does not dualize. by design, it is meant to be model theory of algebraic theories. what would be the "coalgebraic theories", leading to coalgebras as their models? what would their functorial semantics look like? (implicitly, these questions are already in manes' book.)
and then, moving from coalgebraic theories to comonads, like from algebraic theories to monads, should presumably yield an HSP-like characterization for the categories of (comonad) coalgebras. but coalgebras for a comonad over a topos usually form just another topos.
i may be missing something essential here, but then i do stand to be corrected.
I would say that, although there is no straightforward dualization, there might be a "hidden" one. In my opinion, comonads can sometimes play the role of "strengtheners" or "enrichers" for monads, so that while monads can be viewed as a "substrate for structure", comonads are "substrate for semantics". Rather than trying to give sense to this vague phrase, let me give three illustrations. -1- S. Kobayashi, Monad as modality. Theoret. Comput. Sci. 175 (1997), no. 1, 29--74. The starting point in that paper is the monad semantics by Moggi. It seems that for computer-scientific purposes strength of the monad is too restrictive a requirement, and the author modifies the semantics by assuming strength of the monad *only*with* respect*to*a*comonad*. This means that the monad and comonad distribute in such a way that the monad descends to a strong monad on the category of coalgebras over the comonad. Under the Curry-Howard correspondence this yields an interesting intuitionistic version of the modal system S4. A realizability interpretation is also given. -2- Freyd, Yetter, Lawvere, Kock, Reyes and others have studied "atoms", or infinitesimal objects - objects I in a cartesian closed category with the property that the exponentiation functor I->(_) has a right adjoint. This induces a monad, which cannot be strong in a nontrivial way, just as in the previous example. There is a "largest possible" subcategory over which it is strong, namely the category of I-discrete objects, i.e. those objects X for which the adjunction unit from X to I->X is iso. In good cases the inclusion of this subcategory is comonadic. As Bill pointed out, one might view Cantor's idea of set theory as a case of this: the universe of sets is the largest - necessarily "discrete" - part of "analysis" over which the latter can be "enriched" (well, this is awfully inaccurate, sorry -- consider it as a metaphor). -3- In differential homotopical algebra, there was developed a notion of torsor (principal homogeneous object) which works in a non-cartesian monoidal category. This notion requires not just a (right) action of a monoid M on an object P, but also a "cartesianizer" in form of a left coaction of a comonoid C on P which commutes with the action, and is principal in an appropriate sense. It turns out that the monoid and the comonoid enter in an entirely symmetric way. In the monoidal category of differential graded modules over a commutative ring, principal C-M-objects are classified by s.c. twisting cochains from C to M. Moreover in that category, for a monoid M there is a universal choice of P and C given by the Eilenberg-Mac Lane bar construction, and for a comonoid C there is a universal choice of P and M, given by the Adams' cobar construction. I would be grateful for a reference to a version of these for general monads/comonads. Regards, Mamuka