Okay, so there is a script of this lecture kindly provided by Hans Petter.

And I put it on the webpage, it's going to be updated once in a while.

So you're welcome to find errors, possibly contribute if you want.

So there is a git repository and there is a reference to the sources on the webpage.

You can create patches and send them by email, etc.

All right, there was a lecture given at the previous week by Christoph Rauh.

He has explained several things including nature transformations.

I would like to complete this a little bit.

And then we proceed with the discussion of the computation of metalanguage,

which I gave several lectures before, but now we accumulated enough background

to give a semantics of it.

So concerning nature transformation, there was some sort of notation which is often used for it.

Okay, first of all we can write them like this.

So this is a natural transformation from F to G, where F and G are functors.

And this is equivalently denoted as like this.

So this is a notation which is often used too, which is equivalent to this one,

but which contains also a bit more information because here we use functors as arrows

from this category to that category, so G2, and this is like a transformation filling this cell.

And this also induces

a notation to indicate that it's really a natural transformation when you use a double line like this.

So that's just often done in the literature, but we are not going to do it in particular

because we can justify this kind of notation, and we justify it with a theorem.

So we have a cut.

The cut defined as follows, or it's not like this, wait.

Okay, that's not going to be a justification, but anyway it's a good example.

So objects are all small.

So I don't remember if I explained that a category is small if this class of its object is a set,

but anyway, so I explained here.

So cut defined as follows, objects are categories, and homes are functors,

as itself a category.

So this is an example which we should probably have considered before.

So here we can say more, we can say what the identity morphisms are.

So this is ID, let's say C, going from C to C.

So this is a composition,

which goes like this, F, D, C, E.

So that could have been formulated right after we have given the definition of a category and a functor.

So the proof is trivial.

So you just verify the axioms of a category and there's no problem about it.

All right, so but actually what I originally intended was given a different example.

So we grow our stock of example of categories.

So the next example would be fun, I think.

I'm not sure if it's a standard name.

So fun defined as follows.

Ah, OK, fun C. No, wait.

OK, I know that I can now remember the standard notation.

But I'm not actually sure it's a very good notation.

I think it's like this, or CD.

So I want to make it a category.

I say objects of C to D are functors from C to D.

And home FG are natural.