lin-0024

0.7.2 Coproducts, pushouts, and quotients

The dual constructions are defined by reversing arrows. A coproduct combines alternatives; a pushout glues objects along a shared part; a coequalizer identifies points or paths according to a declared relation. If \(p,q:X\rightrightarrows Y\), a coequalizer is a map \(c:Y\to Q\) satisfying \(c\circ p=c\circ q\), universal among maps with that property.

This makes a quotient more than deletion. It records which distinctions are declared irrelevant. LINCS uses quotients to remove presentation changes, gauge directions, advantage baselines, paraphrases, or other variations that should not consume repair effort.

Construction	Structural question	LINCS reading	Example
Product	Can several observations be paired?	assemble jointly available information	a block of diagnostic probes
Pullback	Which pairs agree over a shared target?	enforce relational compatibility	database joins in RADAR
Equalizer	Where do parallel maps agree?	identify a consistency locus	compatible sections in SID
Coproduct	How are alternatives combined?	retain typed alternatives	families of repair proposals
Pushout	How are pieces glued along a common part?	construct a candidate global object	source-bound argument fragments
Coequalizer	Which distinctions are identified?	form a declared quotient	null or gauge variation

Table 3 Universal constructions used as structural declarations in LINCS.

Boundary

A numerical optimizer may approximate a universal construction, but a low penalty is not itself the universal property. Existence, compatibility, and uniqueness obligations must be stated at the structural level and then connected to measurable tests.