  Intersection types are a standard tool in operational and semantical studies
of the lambda calculus. De Carvalho showed how multi types, a quantitative
variant of intersection types providing a handy presentation of the relational
denotational model, allows one to extract precise bounds on the number of
$\beta$-steps and the size of normal forms.
  In the last few years, de Carvalho's work has been extended and adapted to a
number of lambda calculi, evaluation strategies, and abstract machines. These
works, however, only adapt the first part of his work, that extracts bounds
from multi type derivations, while never consider the second part, which deals
with extracting bounds from the multi types themselves. The reason is that this
second part is more technical, and requires to reason up to type substitutions.
It is however also the most interesting, because it shows that the bounding
power is inherent to the relational model (which is induced by the types,
without the derivations), independently of its presentation as a type system.
  Here we dissect and clarify the second part of de Carvalho's work,
establishing a link with principal multi types, and isolating a key property
independent of type substitutions.
