Re: coinduction

["Mamuka Jibladze" <jibladze@agel.ucl.ac.be>]

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