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!