lin-0018

0.1 Categories: typed composition

Definition 0.1 Category

A category \(\mathcal C\) consists of:

a collection of objects \(X,Y,Z,\ldots \);
for every pair \(X,Y\), a collection of morphisms \(f:X\to Y\);
an identity morphism \(1_X:X\to X\) for every object; and
a composite \(g\circ f:X\to Z\) whenever \(f:X\to Y\) and \(g:Y\to Z\).

Composition is associative, and identities are neutral:

\[ h\circ (g\circ f)=(h\circ g)\circ f, \qquad f\circ 1_X=f=1_Y\circ f. \]

The definition is deliberately spare. It says nothing about what an object “really is” or how a morphism is represented in software. That abstraction lets the same language describe several levels of a learning system.

Category	Objects	Morphisms	Composition means
\(\mathsf{Set}\)	sets	functions	ordinary function composition
\(\mathsf{Vect}_{\mathbb R}\)	real vector spaces	linear maps	matrix or linear-map composition
\(\mathsf{Smooth}\)	smooth manifolds	smooth maps	composition of differentiable transformations
A path category	nodes of a typed graph	directed paths	concatenating executable steps
A schema category	entity and relation types	declared relational paths	following foreign keys or joins
A category of models	model states or structured realizations	admissible transformations	transporting one realization to another

Table 1 The word category fixes a discipline of typed composition, not a single choice of mathematical object.

A morphism is not merely an arrow drawn on paper. Its type \(f:X\to Y\) is a contract. The composite \(g\circ f\) exists only when the output type of \(f\) matches the input type of \(g\). Many bugs in complex learning systems are already visible as type failures: an adapter expects a representation that an earlier adapter does not produce, a local database chart lacks the join witness needed by a downstream map, or a proposed argument repair changes a claim where only a warrant edit was authorized.

Example 0.2 A skill pipeline

In LASKO, a retrieval step \(r:Q\to E\) maps a query to evidence, and a synthesis step \(s:E\to A\) maps evidence to an answer. Their composite \(s\circ r:Q\to A\) is a candidate skill. If a verifier \(v:A\to V\) follows, then associativity guarantees that

\[ v\circ (s\circ r)=(v\circ s)\circ r. \]

Associativity does not guarantee that the result is correct or executable; it guarantees that the two parenthesizations name the same typed composite. Additional declarations supply the substantive promises.