Alright, so yes, there is indeed an equivalent definition of Monad.

I gave a different one because I'm trying to emphasize the computational intuition,

because I started from this semantics, operational semantics and whole-biology semantics,

and I tried to motivate Monads as type constructors,

and I think it's easier to understand this concept using that definition that I gave,

because the star which I used is a lifting.

So you have a map, a function which is a generalized function in a sense,

so instead of taking this sort of morphisms as functions,

you consider this kind of morphisms as functions.

And these functions are a generalized form of these functions,

they might be what is called an effect.

So the simplest effect was when t was this lifting construction for domains,

and the effect was a divergence.

So every function either returns the result, which is b, or diverges.

And this lifting construction transforms this sort of functions to this sort of functions,

and it makes functions composable, because if you take just this function

and another function like this, then you cannot compose them.

And of course you want to compose the functions because you run one after another,

and you need to tell what the result of the composition is.

And apparently we use the star to have the composition,

because if I have f and g, so now I can lift g using the star

and compose it with f in the standard way.

And of course there is eta, which basically converts a normal function to this generalized function,

so it's a function with a possible effect captured by a monad.

I think for the programming intuition it's a nicer definition,

it's simpler, it captures this intuition,

and it doesn't involve too many categorical notions.

So I didn't even need to involve natural transformations to introduce it.

Yeah, so we'll return to this later.

And before I wanted to elaborate a bit on the material that I gave previously,

a more elementary one, like products.

So just do some simple things with them.

And first of all I need a definition of isomorphism.

So isomorphism.

So isomorphism.

So isomorphism between two objects in a category is given by a pair of morphisms,

well, f from a to b and g from b to a, such that, okay, can I possibly express it as a diagram?

So I start with a, and then I apply f, and then I apply g, and I get this.

So, and...

And if I compose it with f, b, then I have the identity here.

All right, so this is a way to express it as a diagram.

You can instead just write down two equations, and these two equations would say that f is inverse to g.

What g is left inverse to f, and f is right inverse to g.

And one can also draw two separate diagrams, but, yes?

I mean, you just take a and b and make I-V arrows just go from one point to the other.

Yeah, so you mean like this f.

Yeah, in this case it would work too.

This kind of diagram with loops there is sometimes dangerous because sometimes not everything commutes.

Yeah, so you could draw it as one diagram, you can draw it as two diagrams.

Sometimes you cannot draw, mix two diagrams into one.