Library / First Principles Framework (FPF) - Core Conceptual Specification
Jump to passage
In this reading

Link to current text

Published source confirmed at last check

Source changed 2026-10-03 07:42:37 UTC · snapshot created 2026-10-03 07:43:27 UTC · last check 2026-10-03 07:50:10 UTC

B.5:5.5 - Understand which composition a theory permits

A practitioner wants one input to feed two operations. Let X, Y and Z be distinct atomic types, with available operations f: X → Y and g: X → Z. A cartesian account supplies copying, Δ_X(x) = (x,x). The composite (f × g) ∘ Δ_X returns (f(x),g(x)) from one input.

Compare an account generated only by f, g, identities, serial composition, tensoring and exchange of factors. Here f ⊗ g runs the two operations on separately supplied inputs, X ⊗ X. Every permitted generator preserves the number of atomic factors; composition and tensoring preserve that property. Therefore those operations cannot construct X → Y ⊗ Z. The missing contribution is a second input or an additional copying operation.

The receiving work determines whether copying its input is admissible. The comparison exposes that requirement before selecting an implementation. Baez and Stay, §2.3, supplies the cartesian/monoidal distinction; the generated-operation case above makes its use explicit.