Top-free disjoint intersections

Chapter 21 fixes the top-free 2016 ${\lambda }_i$ variant. Source types are integers, arrows, products, and intersections; target types are integers, arrows, and products. There is no $\mathsf{Top}$, no top-like exception, no effects, and no implicit intersection re-association.

Semantic disjointness quantifies over unrestricted raw common supertype witnesses. Its structural decision procedure is exact for well formed inputs by theorem 21.8. In particular, an ill formed domain intersection may witness that two arrows are not disjoint.

By lemma 21.3, coercions are target typed. Disjoint intersections have a unique ordinary contributor by lemma 21.5. Coercions are unique by lemma 21.10, and synthesized types are unique by lemma 21.11. Elaboration preservation is theorem 21.12; alpha-syntactic coherence is theorem 21.13. Target progress and preservation give corollary 21.14.

Removing disjointness from both merge and intersection well-formedness admits two integer projections with observations $1$ and $2$. Removing the ordinary-target premise leaves coercion typing intact but destroys coercion uniqueness. The theorems do not identify elaborations of merely isomorphic intersection associations.

The finite Kappa corpus in artifacts/ch21-disjoint-merge/ executes source subtyping, merge formation, and contributor selection in eight structural examples, including a nested-product demand, plus the two observations of the rejected counterfactual. It is not a proof of the decision, coherence, or safety theorems.