 The structure of intersection types is described by the conjunction–implication fragment of \(B\), the basic relevance logic. In the following presentation of this logic, \(\le\) is the main connective (an implication) of a formula and \(\Rightarrow\) separates the premises and the conclusion of an inference rule.