Sort of types. Usually \(\star\).

\[ \mathit{True} : \mathit{Bool} : \star \]

Sort of sort of types.

In lambda cube systems we have \(\star : \square\); in \(\lambda^\star\) we have \(\star : \star\).

Note that in STLC, \(\lambda^\to\) we don't have \((\square, \star, -) \in \mathcal{R}\) so we cannot have forAll, \(\forall\).

Some sorts have a types. \(\mathcal{A}\).

Just s2 = axiom s1 induces a typing rule

\[ \frac{}{ \Gamma \vdash s_1 \Rightarrow s_2 }\;\mathsf{Axiom} \]

Rules for products. \(\mathcal{R}\).

Just s3 = rule s1 s2 induces a typing rule

\[ \frac{ \Gamma \vdash \alpha \Leftarrow s_1 \qquad \alpha \Downarrow \alpha' \qquad \Gamma,x:\alpha' \vdash \beta \Leftarrow s_2 }{ \Gamma \vdash \forall x : \alpha.\beta \Rightarrow s_3 }\;\mathsf{Pi} \]