monad on arbitrary categories

Stream: general

[Kenny Lau]

Would it be useful to have monads on categories instead of always on Types?

[Kenny Lau]

that would also require Cartesian-Closed-Categories though

[Johannes Hölzl]

Yes, they are also interesting for category theory. An instance I'm interested in is the monad on measurable spaces, i.e. the Giry monad. But keep in mind that they are different beasts than the Type-monads. The latter is very normal in DDT, the former is more involved.

[Johannes Hölzl]

Hm, I don't think so. Monads work on arbitrary functors no CCCs are required.

[Kenny Lau]

but we also want <*> don't we

[Johannes Hölzl]

I'm not sure what the best approach is. Keep in mind that monads in category theory are different, the morphisms are not necessary functions.

[Johannes Hölzl]

Often they are a subset of functions, but not in a CCC (at least not in Top or Meas)

[Simon Hudon]

I have a draft of those (monads and CCCs) on my drive. I can clean them up and PR them

[Simon Hudon]

@Johannes Hölzl Do you think it's a good idea to define monads as their Kleisli category and then derive a monoid from them?

[Johan Commelin]

For adjunctions we also had choices, and we came to the conclusion that we just wanted both.

[Johan Commelin]

Redundancy of data in definitions seems to be a good thing.

[Johannes Hölzl]

@Simon Hudon I think we should focus on what we need. Do you have a case where you get a Kleisli category? Or do you have a functor + monad properties? In my case I currently need the later.

[Simon Hudon]

When you say monad properties, do you mean as a monoid? I have a preference for the kleisli category because it does not depend on monoidal catergories (of which there seems to be an endless supply of bad definitions) and it is easier to connect to programming

[Reid Barton]

I think this has come up before, but my view is that we certainly want the ordinary definition of a monad at some point (i.e., a functor $T : C \to C$ with a unit $1 \to T$ and multiplication $T \circ T \to T$ such that ...), but monads aren't actually as useful for proving basic things about algebraic categories as books on category theory would have you believe.

[Reid Barton]

Because in the monad approach you still have to define the monad and its multiplication from scratch, and the monad is supposed to compute, for example, the free group on a set, and writing that down is most of the work of proving that the category of groups has colimits or whatever. And then you still have to check that algebras for the free group monad are the same as groups defined in the usual way, because your examples are all in the latter form.

[Reid Barton]

But there are also more significant applications of monads. Note this is all from a math perspective.

[Reid Barton]

The issue related to CCCs is I guess monad extends appllicative, which is supposed to mean a lax closed functor or lax monoidal functor depending on your point of view. That is something specific to the category of types (sets)--actually I'm not sure in what generality it holds. I actually don't see why the category being a CCC should be enough, I think you also need the monad to be a strong functor.
But anyways, that might cause some difficulty if we try to unify monad with the monads from category theory.

[Reid Barton]

@Simon Hudon by "the kleisli category" do you mean something like page 35 of http://www.cse.chalmers.se/research/group/logic/Types/Uustalo-lectures.pdf? That is, specifying a monad by giving its Kleisli category

[Simon Hudon]

That looks similar. I'm not too well versed in the who adjunction business but I think that's the same. You can specify a monad M on C by giving a category with the same objects as C and which defines a morphism between a --> b iff C has one between a --> M b

[Reid Barton]

Okay, but then you need to require something on the new category in order to know that it's the Kleisli category of some monad. (For example, it could also be the co-Kleisli category of a comonad.) Apparently, it's this right adjoint condition

[Simon Hudon]

Isn't that automatic?

[Reid Barton]

isn't what automatic?

[Reid Barton]

If I start with a monad, then I can build a Kleisli category, which has the same objects and a functor from the original category that is the identity on objects. But if I start with any nonsense such category, it might not come from a monad in this way (I already gave a counterexample--I could build other examples from a comonad)

[Reid Barton]

You also have to check that the Kleisli category "remembers" the entire monad, but I think that's some easy Yoneda argument

[Simon Hudon]

Ok, I see. I think I misunderstood your point. I now see that the comonad was your counterexample.

[Simon Hudon]

Does the whole monad have anything more than a monoid in the category of endofunctors?

[Reid Barton]

No, those definitions are equivalent

[Simon Hudon]

That's curious. I thought my Kleisli construction was sufficient to generate that monoid. I'll have to revisit it to see what I missed

[Reid Barton]

I agree trying to literally write "monoid object in the category of endofunctors" using monoidal categories would be a mess, but the definition you get by unraveling "monoid object" is rather simple (and what I think of as the usual one), see https://en.wikipedia.org/wiki/Monad_(category_theory)#Formal_definition

[Simon Hudon]

Nice! Thanks!

[Reid Barton]

If you start from the Kleisli category, let's call it D, you need some way to show that D(A, B) = C(A, TB) for some functor T on C. If you have that, then the monad laws for T should follow.
It's easier to just start with T.

[Simon Hudon]

Ah! Yes! That's what I did! I start with T and C and the monad instance define bind : (a --> T b) -> (b --> T c) -> (a --> T c and return : a --> T a with morphisms on C together with their laws. The Kleisli category is actually derived from that. I thought of it as the Kleisli category itself because of how close they are.

[Reid Barton]

Okay, so you were probably thinking of something like "T : C -> C, together with a category structure on Ob C with hom sets given by A -> TB"

[Simon Hudon]

Yes exactly