Functions compose: given $\mathrm{f:X\to A}$ and $\mathrm{m:A\to U}$, the composite function $\mathrm{m(f): X\to U}$ maps $\mathrm{x:X}$ to $\mathrm{m(f(x)):U}$.

Entailments compose ****in sequence, along functions: given $i:Q\Rightarrow R$ over $\mathrm{f,g}$ and $j:R\Rightarrow S$ over $\mathrm{m,n}$, the composite entailment $i\cdot j: Q\Rightarrow S$ over $\mathrm{m(f), n(g)}$ is defined by applying the proof $i$, and then the proof $j$.

composite entailment $j(i): Q\Rightarrow S$

$j(i(q)):S(\mathrm{m(f(x)),n(g(y))})$

Process composition, and “sequential” inference composition, is associative and unital.

[draw]

<aside> 💡 This means that types and processes form a category, and so do relations and inferences. See Active Logics.

</aside>