If we consider the STLC, and assume that the cardinality of a type is the number of $\rightarrow$ in the type, assuming the traditional rules, suppose we have that $\Gamma \vdash e : t$. Is there any theorem giving us an upper bound on the cardinality of $t$?
Furthermore, we have some well-typed terms of the form $\lambda x : s . f$. Is there an upper bound on $s$?
I would expect the same upper bound can be used in both cases.