Now that we have learned how to extend the system, we want to extend it even more. For instance, we may want to have terms manipulating types. So, we want something like a term AND such that gives two types A and B, we get as a result the type "A&B". So, you see we are at different levels than before. So far the terms manipulated the terms, or the terms could manipulate types but giving back only values. Now we require to have terms that take types and give us back types. Now, what can be the type of a term like AND? If we assume that Prop stands for the collection of types, then AND takes a Prop, takes then another Prop - this capital A and this capital B in the slide - and gives back another type, another Prop - this type "A&B". Under these assumptions we have a stratification of layers. We have terms like our Lt lx:t.x. Then we have types for these terms, like the one in the slide. But at this level we also have constructors, that is terms like this one in the slide that manipulates types. And then, at the further level, we have what we may call the types of these terms manipulating types. We call "kinds" these new types. So, we have types here and the type of a type is a kind. We have one kind - Prop - and then we form other kinds by using this arrow constructor.

---