Universal typing axiom
= Universal typing axiom
{title2=$\varnothing\mapsto p:\star\quad\text{for every }p$}
An extension of <simple type> assignment that assigns a distinguished atomic <type variable> $\star$ to every <lambda term> in the empty <typing context>. The recorded assumptions therefore need not contain all <free variables> of the subject. This is a rule admitting a <typing judgment>, rather than an implicit conversion to every <simple type> or a general <subtyping> rule.