We have been dealing with the concept of the initial algebra last time and we looked at a bunch of examples.

Some of these examples were the initial algebra, as we see them, practically from our point of view,

data types on the edge of quantities.

And we looked at one example where it was a little more subtle, where we took a different basic category,

the ordered quantities, and found that more things play into it,

especially if you choose the function correctly, then the initial algebra is also equipped with a non-trivial order.

And we have to pay attention to things like how the algebra structure is then also monotone.

Well, that's the case in this case, but we get a fold principle for that, where the folds that we get are monotone images

from the initial algebra and have that in this specific case with the initial algebra for the function of x to x bottom,

so an order x expanded into a new smallest element. We looked at this specifically, but the initial algebra was the natural number

with the usual order and you got as folds monotone images of the natural number.

Let's see.

I'll make it a little brighter.

Let's pull the darkening from the back.

Let's see.

Let's see.

So, better.

Okay.

Let's see.

We looked at the two proof rules when we talked about data types on quantities, with which we can define things by recursive functions,

that is, by folds, systematically.

We now get them in general, also for data types in any category, and we see one of the effects with which the category theory is always being housed.

First of all, what has been proven is of course much more general than before.

We no longer have to do this by type per data type, but we get it for all data types at once, by encapsulating the data types as functions.

And secondly, we get it for general sub-categories, rather than only the category of the quantities.

So we can do it in any sub-category that we do not put as much of a challenge on,

except that the initial algebra we are talking about now only exists.

But secondly, the proof of these rules will also be shorter. We will find that it will not be short, it will be too trivial, both.

And thirdly, it is better understood. So you understand the proof better than the principle itself.

And that looks like this.

On the one hand, we have the identity law.

So we assume that we have an initial algebra for a point F, let's say, I with a structure formation i.

And that is actually the only requirement we put on the category.

So there has to be this initial algebra, otherwise we should not be able to talk about it in the sentence.

And I remember our banana notation.

So a banana from any algebra for a function is always the clear representation of the initial algebra into the given algebra.

Of course, we can apply this, especially to the initial algebra itself.

We can use the banana from i. And I claim that banana from i is the identity.

And secondly, we have the fusion rule.

The fusion rule had a somewhat difficult condition last time, which practically stated that you want to attach a shape to a square.

So that it has to commute my algebra with the operations.

We can say that much shorter.

So we can say that if, wait a minute, what was the thing called back then?

I think it was called k back then.

So I have a k from one algebra to another.

That is a F-homomorphism.

So that thing is supposed to be a homomorphism of F-algebra.

I'll write down what that means.

That means, wait a minute, what's the deal?

So you can't draw diagrams, you can just throw them away.