domain name

degree

located

Of course, the full operation is a function on some type C,

and both the constant and the function H live on C.

Basically, these two parameters make C into a type

that is sort of like the natural numbers.

In particular, it has something that matches the zero,

that's the C, and it has something that matches

the successor function H.

And what the full operation does, it just takes a term

which represents the natural number,

a term that consists of one zero at the end

and lots of successors before that, successor operations,

and it replaces the zero with the C

and all the occurrences of successor with the H.

And we have concluded the picture consisting of capital C

and little c and h.

I pick exactly the original natural numbers,

in particular I take c to be zero and h to be successor,

and this gives me the identity on the naturals.

And then, slightly more complicated, the fusion rule.

The fusion rule says something about application

of a function K which runs between two of these structures,

so types equipped with operations of this kind here.

And it makes an assumption, namely that K is compatible

with these structures.

So, K of C equals C prime and,

and regarding these two endo functions,

K basically commutes with them, that is,

the diagram here commutes.

Okay, and under these assumptions,

let's make this explicit, so I'm assuming that this holds,

and then,

I hope that this is wrong again.

Now, finally.

So, the fold operation, of course, consumes natural numbers.

How else would it replace occurrences of successor,

et cetera, with these functions?

And now, now we get two folds from these data,

C and H, and C prime H prime respectively.

So, a bit of a room here.

So here we have fold N of C and H,

which is a function into C, and we also have fold N

of C prime and H prime, which is a function into D,

and we have our K, which runs from C to D,

and this diagram commutes.

I'm occasionally going to emphasize commutation of diagrams

by writing this double cross in here,

or sharp, or whatever you want to call it.