Two sentence summary that glosses over a lot of things:

1. Types can be used to classify programs.

2. Dependent types can be used to classify programs by running other programs on them.

If you would like to learn more about dependent types, ‘The Little Typer’ is newly out and a lot of fun to read:

https://mitpress.mit.edu/books/little-typer