So we have a console key, and we have a monad key, and a bar.

And we need to show that Te, which is Te of x plus e, is a monad.

So, Te at a circle flex and cross.

And then we need to show that, firstly, that this is the x-dagger, which is the identity on Te x.

Secondly, the f-dagger, which goes to f of star x, is the same as f.

As this function from x to the y.

I think it shows Te y.

And lastly, we need to show that Te dagger is the same as Te dagger composed of f-dagger.

The first two parts we showed already, and now I'll have to show the last part.

So, I wrote down what this exactly denotes in terms of how the dagger was defined.

So we need to show.

So, this is the problem.

Basically, the G-dagger is the f-dagger, which is...

I did introduce a shorter notation for the problem.

I did introduce G to the G at z plus e, so look in the right.

G-dagger was defined as G tilde star.

I'll just have to show that this is G-dagger and G tilde star, so f tilde star, and I'll show that this is equal to G-dagger, so f tilde star.

Which is...

Yeah, which is the following G-dagger and G tilde star.

So, the method that you used in the institution was like a post-composite first interval, and from that conclude this identity.

This identity was the...

Well, I...

So, in the future, we'll be following the creation of three in another way, and because this is co-pairing, I just need to show that this here is the same co-pairing of those two paths.

I'll just go and...

So...

Did I already do the first part of this?

Yes, you did, but I didn't remember which one was the first part.

So, the actual four RCS.

Ah, yeah. I did show that...

We can simply cancel the stars here, just like I did show.

Yes, I remember there was something like that, but now I didn't see how you can cancel them.

Well, here is the star in the other hand.

Yes, but on the left hand side there is no star.

Yes, but the star is the star of the Monad, so we have the following G tilde star, so F tilde star,

and the same as G tilde star, so F tilde star.

Yes, this is correct. Now you can cancel it.

And now we can cancel this star and that star.

So, I think when you write this identity, we just need to prove it.

Yes. Then, in such a way as to show G tilde star is equal to F tilde,

just the same as G dagger with the F, and cancel the Y plus E with the right.

And now I always showed last time that...

Well, it's very basic really.

This here, cheese star, so, yes, is the same as...

And left is the same as G dagger, well, as the right side, so it's on the left.

Here, and one, two, and left.

Well, this is basically the definition, because this here is just G dagger star back,

and by definition, this is G dagger star F, something else, star inlet, which is G dagger star F.

So, this identity holds.

Now I'll only show that those, the right part.

So basically you're using the LL-line here, right?