@ionchy it's interesting. I also can't answer this, especially not in a context of a GADT lecture, however I know what I would avoid doing while attempting to anyway. I would avoid invoking type-value dichotomy! I would probably answer like this, informally:

===

Consider a set of elements. A type then is, informally, a way to split this set into two subsets: one belonging to that type and the other not belonging to that type. As we create the set of these types, it is completely disjoint from the set of elements (it lives in a higher universe), this is why we can use elements from the intial set as we define types.

For example, we can define types that discriminate the elements based on a natural number parameter (natural numbers are normally also elements of the initial set we were considering). These kind of types are called "indexed types" in the literature.

Observe that now that we have this "type zero" universe, we can now consider it as the underlying set of elements and build up "type one" universe by creating types that discriminate the elements of "type zero".

===

I would then tie it back to GADTs like this:

===

In this mental framework then, GADTs over a way to combine several ways to include elements of the underlying into a single type, perhaps recursively.

===

Here I would point at a simple Expr GADT explaining how it allows us to capture all the Nats, all the Bools and, recursively, all the Expr Nats and Expr Bools via Add and And constructors, while at all points creating type Expr a. I would then emphasise that even though Expr a seems to be really open (i.e., one can write Expr String), it really isn't because there is no way to construct `Expr String` with the constructors we wrote down.

But it's certainly a tricky one to come up with on the spot. I wonder how did you respond? :)