sufficient to solve it. And basically I don't think it's very complicated because the thing is it just involves lots of new terms, but in essence if you know these terms then the solutions are not complex, not very complex equations.

One thing that I forget to say is that this notation for function, so it's a function which goes from a1 to a2 to b1 and b2, provided that f goes from a1 to b2 and g goes from b2.

So that's a game of teleportation, basically the leap, this product constructor from object to function.

And it's not something new, that's expressible using the other syntactic construction that we introduced in the lecture. So p r, m f, g p r, m. So it's just this thing.

And I made a footnote that the exercise is just to check it, to try to... I wonder if there's something else on here about the exercise maybe.

So otherwise I would propose that we proceed with the previous exercise we told, the first part of it I think we came to, yes, we argued continuity I guess, more or less.

So I am talking about assignment one, so I propose that we proceed further and do exercise three, so maybe someone will be eager to do it.

How about you? I can give you your real solution.

So which one is yours?

So you need a promo set.

And the programming conditional functions like co-product.

And then we need to find the structure to work for this.

So if x is applied a and we do inner on x, then we get an object of type a plus b. As PCF doesn't allow us to do polymorphism in a nice way, I could apply the meanness of the function. So it's a nice solution for that.

Yeah, so we did the big individually for products, so I didn't write down the index, but this is...

For products it's b here, because for products you have four types.

So for products you can guess the type, right?

And here we can't infer it.

And then we need function application on the co-product. So if you have two functions, f of a, c, and b to c.

And then you can infer that f of g is from type a plus b.

So that was the easy part.

Maybe we'll stick to this a bit and maybe we'll experiment with it.

So this is alright, this is a correct solution, but do you maybe know the case operator?

So there is a case operator and it has to be present, I'm not sure, but there is like case of etc. Do you know it?

Yeah, that's the question, so that's why I call it an extended period.

So maybe instead of this word rule we could develop another rule, basically capturing the instruction case, something of type emr, and then a function of emr, another function.

Something of type emr, that.

Basically I want this, I can write it down, this is already the case.

Let's say b of n rule x, q, enter y, say r.

So that's, we'll maybe need to check, I think there is something like that in Pascal, but I'm not sure about the syntax.

But that can be done too.

That's the only thing we can express using this.

But can you maybe just on the fly design a type and go for it?

So my p is something returning a product type.

P is of a, q, that's the answer.

No, q is a term which depends on x, and x is of the right.

Yeah, x is of type a and y is of type b. So q is the function from a to?

Well, we can treat it as a term, because it's a term which depends on x.

So like we did lambda abstraction, so when we constructed lambda abstraction, then we have a term dependent on x and we return a negative function.

And the same thing, the same trick I showed for if I guess, or for while.

So basically you just need to specify this q as a term in context where you add x to the context.

Okay.

And q returns some other type.

And same thing.

Yes.

That's the real thing.

Well, that's index that's the term.

No, no, not index, that's supposed to be r.

Yeah, and then you can start the...

There is no second term, so I'll just...

This is more or less the argument, but this, I guess you can write it like this.