ifc-0005
0.2 Categories: typed composition
A category \(\mathcal C\) consists of objects \(X,Y,Z,\ldots \), morphisms \(f:X\to Y\), an identity \(1_X:X\to X\) for each object, and a composite
whenever \(f:X\to Y\) and \(g:Y\to Z\). Composition is associative and identities are neutral:
The definition is deliberately silent about what objects contain. In \(\mathsf{Set}\), objects are sets and morphisms are functions. In a category of vector spaces they are vector spaces and linear maps. In a path category, objects are states and morphisms are composable paths. In a category of theories, objects may be presentations and morphisms may be admissible translations or extensions.
The first reading habit is type first. Before evaluating a formula or a generated proposal, identify the source and target of every map. A composition is meaningful only when adjacent types agree. This catches a basic form of creative nonsense: combining ideas whose verbal similarity hides incompatible roles.
Categories do not assert that everything composes. They record which compositions exist. Nor does associativity say that a composite is true, useful, or executable. It says that a legal chain has a coherent parenthesization. Semantic interpretation and admission supply the remaining obligations.