ifc-0074

5.2 Sketches present theories

A fully completed category of operations is too large and redundant to be a convenient output format. A sketch presents it by generators and relations. Following Ehresmann, a sketch contains a graph of formal objects and arrows, specified commutative diagrams, and designated cones or cocones [ Ehresmann , 1968 , Barr and Wells , 1999 ] . A model maps this presentation into a target category and realizes the designated diagrams and universal constructions.

For a finite-product sketch \(\mathbb S\), a model

\[ D:\mathbb S\longrightarrow \mathcal C \]

must send each designated product cone to a product cone in \(\mathcal C\) and satisfy the declared path equations. Closing the presentation under the required finite products and equations yields the corresponding algebraic theory. In this precise sense, the sketch is a finite specification of the theory rather than a second semantic model of it.

A sketch is a compact presentation, not the entire theory. Its completion determines a doctrine-specific category of operations; preserving functors realize the theory in a semantic category.
Figure 5.1 A sketch is a compact presentation, not the entire theory. Its completion determines a doctrine-specific category of operations; preserving functors realize the theory in a semantic category.

This distinction gives synthetic creativity an auditable output format. A frontier model may propose prose, but an admitted theoretical contribution must identify which sorts, operations, equations, cones, or cocones have been added. Its consequences can then be tested across models rather than only in the example that inspired the proposal.