lin-0277
Categorical declarations
Notation Meaning Role in lincs \(\mathcal C,\mathcal D\) categories Typed domains of objects and composable maps. \(f:X\to Y\) morphism A legal computation, translation, observation, or intervention channel. \(g\circ f\) composite The structural operation whose declared coherence is tested. \(D:J\to \mathcal C\) diagram A typed family of objects and maps with shape \(J\). \(\mathbb S\) sketch or structural declaration Generators, equations, cones, cocones, and other obligations imposed before choosing a loss. \(\operatorname {Mod}(\mathbb S,\mathcal C)\) models of \(\mathbb S\) in \(\mathcal C\) Realizations satisfying the declared sketch structure. \(\operatorname {Path}(\mathbb S)\) path category of a sketch Formal composites generated by the declared arrows. \(p,q:X\rightrightarrows Y\) parallel paths Two computations declared or tested to agree. \(\operatorname {Fact}\) factorization comparison The typed test used to compare a direct arrow with a declared composite. \(F:\mathcal C\to \mathcal D\) functor A compositional translation between structural domains. \(\eta :F\Rightarrow G\) natural transformation A coherent change of functorial realization. \((\mathcal V,\otimes ,I)\) enriching symmetric monoidal category Supplies the type of hom-objects and the tensor used to compose them. \(\mathcal C(X,Y)\in \mathcal V\) enriched hom-object Records structured maps from \(X\) to \(Y\), such as an order, distance, or vector space of maps. \(\mathbb S_{\mathcal V}\) \(\mathcal V\)-enriched sketch A compositional declaration using enriched equations and designated weighted limits or colimits. \(\Omega \) subobject classifier Internal object of truth values; its Heyting-algebra structure need not be Boolean. \(\chi _A:X\to \Omega \) characteristic map of \(A\hookrightarrow X\) Classifies a predicate or context-dependent subobject without assuming that it has a decidable complement.
Graphical convention. In the 2-categorical figures, a region denotes a category, a wire separating two regions denotes a functor from the region on its left to the region on its right, and a box denotes a natural transformation read from bottom to top. Horizontal pasting is whiskering; vertical stacking is composition of natural transformations. Teal wires mark tangent structure and amber boxes mark comparison or diagnostic cells. Color is explanatory and carries no additional type information.