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$.