5.8.1 Transport does not choose the creative extension

5.8.1 Transport does not choose the creative extension

Kan extension begins only after the theory map \(\iota :\mathbb S\to \mathbb S^+\) has been supplied. It can determine a universal way to propagate semantics along that map, but it does not decide that a new sort, mechanism, invariant, or law should exist, nor does it choose among rival extensions. Searching over a registered category of candidate maps may be useful, but remains creative only relative to that previously declared metalanguage.

This locates Kan transport precisely in the DIAL workflow. Double involution diagnoses the interaction between assimilatory and proto-accommodative local variation. A proposal engine turns the localized frontier into a finite sketch map \(\iota \). Kan extensions then transport old semantics through the proposal. Admission finally determines whether the transported model is coherent, empirically adequate, and useful. The universal construction neither replaces proposal nor certifies admission.

There is also a prior sketch-theoretic layer. If the two local repair directions are presented by enriched limit sketches \(\mathbb A\) and \(\mathbb B\), their interaction can be presented by \(\mathbb A\otimes \mathbb B\). The equivalence between iterated models and models of the tensor product makes horizontal-first and vertical-first interpretations comparable before any domain theory is extended [ MacAdam , 2023 ] . Thus DIAL’s local declaration may itself be an algebraic theory, while \(\iota :\mathbb S\to \mathbb S^+\) changes the theory being investigated. These are distinct levels: tensoring presents how two repair calculi interact; Kan extension transports models after a particular theory change has been proposed.

. DIAL diagnoses and helps organize a change of theory; Kan extensions transport semantics across a supplied change of theory. Do not identify the universal transport with the abductive act that proposed its indexing map.