Again, I'm trying to connect different pictures that I have given here.

So like quite a few lectures ago I have introduced this computational mental language.

This is something that has no programmers know.

And then we have discussed monads and strong monads.

These are things, sort of gadgets, categorical gadgets that are third,

independently in the category of words and they have been studied by mathematicians.

And basically this story of strong monads in terms of categories and diagrams

is the one what the categories stick to.

And these words are connected by the mental language and hopefully this also suggests how the theory and practices are connected.

So I'm going to make this connection precise, more or less module-like some details,

because it's actually quite difficult to present too many details.

I noticed that actually things which I have got used to,

there are lots of underlying theories and demos behind and there is no way to present all this.

So I just give you the general picture and give some statements without proofs.

So we have seen these trainings and so I believe we have started interpreting the mental language.

So we said that we interpret types as objects of a category

and we interpret trends in context as morphisms in this category.

So the last thing we have to do was to define this do-construction, do-constructs.

And these are defined like this.

So semantics of the big...

semantics of the computation in mental language.

So return T.

So this is what this says.

Just the composition of each of these semantics of these things.

So semantics of the computation in mental language.

And in Haskell the name for it is return, but we shorten it to it for the sake of synthesis.

And then there is this do-expq and this is equal to Tb equal to...

So what we have to interpret...

Composer equals Tb, and T. Gamma objects also gamma objects.

And here is also forgetting the other thing.

And this is the index.

So the type of this thing is from gamma to gamma times T.

So this is Tb.

So this is the gamma to gamma times T.

And this thing is from gamma...

Ah, okay, I forgot to spell all this because I'm missing all the arrows.

Okay, after I have spelled all this and stuff here, the title composes.

So we start with this and we get this, we apply strings to this, and then we apply the semantics of Q with the class get-start.

Now you see that everything which we have introduced, all the structure as in use.

So we need the moment operations and we need the strings.

Correct?

Okay, it's a standard story.

I don't know, we've been to several theoretical courses and you might have noticed that pattern if we introduce a calculus,

then normally what we introduce is a model and some reasoning and we state some of these in complete distributives.

This is the case here.

So I have already given the semantics.

Basically I specify what my model is. My model is a Cartesian category with a strong monad in it.

And this is a semantic for my transform with it. And then what's the logical calculus for that? That's the equation of logic.

So how we do the equation of logic? We specify number of rules and we derive the conclusions from premises.

So the premises are used in axioms and you apply rules to the axioms and you nest it until you get a conclusion.