show/hide this revision's text 2 fixed \Box to \square

$\star$ is a kind, which classifies types. $\Box$ \square$ is a sort, and it classifies kinds. So this is a 4-layer deep classification. Once you get to have type-constructors, kinds get really useful. Eventually, you wish for kind-constructors too, and then you need sorts.

Turns out that you really rarely ever need to get deeper than that (even though Coq and Agda have infinitely many such levels). I am not sure I have ever read a good Curry-Howard explanation of kinds and sorts. I would hazard a guess that classical mathematics rarely worries about kinds/sorts, I would tend to dig into $n$-categories to find a good relation.
show/hide this revision's text 1

$\star$ is a kind, which classifies types. $\Box$ is a sort, and it classifies kinds. So this is a 4-layer deep classification. Once you get to have type-constructors, kinds get really useful. Eventually, you wish for kind-constructors too, and then you need sorts.

Turns out that you really rarely ever need to get deeper than that (even though Coq and Agda have infinitely many such levels). I am not sure I have ever read a good Curry-Howard explanation of kinds and sorts. I would hazard a guess that classical mathematics rarely worries about kinds/sorts, I would tend to dig into $n$-categories to find a good relation.