What is the intuitive meaning of star and box in a pure type system? The systems of the λ-cube have the axiom $\star:\square$.
I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below.  What are the intuitive meanings of $\star$ and $\square$ in each interpretation?
$t : T : \star : \square$
Programs: t is a program of type T.  (Possibility: T is a program of type $\star$?)
Proofs: t is a proof of theorem T.  It's hard to see T as a proof of $\star$, though.
Set elements: t is a member of set T.  (Possibility: T is a member of the universe $\star$ of sets.  Then it seems difficult to assign a meaning to $\square$ that avoids the membership $\square : \star$.)
I'd like to fill out this table both vertically and horizontally, with both further interpretations and the missing descriptions of $\star$ and $\square$, and possibly meanings of $T : \square$ for $T \neq \star$.
Thank you!
 A: $\star$ is a kind, which classifies types.  $\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.
A: I seem to recall there’s a really good explanation of kinds and sorts in Sørensen and Urzyczyn’s Lectures on the Curry-Howard Isomorphism (a previous version is available online).
A: I've found you won't go far wrong if you think of the objects in * as sets, and the objects in $\Box$ as proper classes.  Thus, * is the proper class of all sets.
A: I found J. W. Roorda's masters thesis to be a good exposition of PTS.  It is linked from here:
http://people.cs.uu.nl/johanj/MSc/jwroorda/
