ifc-0079

5.8 Kan extensions as the transport semantics of DIAL

The restriction functor \(\iota ^*\) explains how to forget the additional structure of a proposed theory. The converse problem is just as important: given an old model

\[ M:\mathbb S\longrightarrow \mathcal C, \]

how should it be transported into the proposed theory \(\mathbb S^+\)? In the ambient functor categories, the canonical candidates are the left and right Kan extensions along \(\iota \):

\[ \operatorname {Lan}_{\iota }M, \qquad \operatorname {Ran}_{\iota }M. \]

When these constructions restrict to the doctrine-preserving model categories, they form an adjoint triple

\[ \iota _!\dashv \iota ^*\dashv \iota _*, \qquad \iota _!M=\operatorname {Lan}_{\iota }M, \quad \iota _*M=\operatorname {Ran}_{\iota }M \]

[ Mac Lane , 1998 , Riehl , 2016 ] .

Pointwise, when the required colimits and limits exist, their values at an object \(s^+\in \mathbb S^+\) are

\[ (\operatorname {Lan}_{\iota }M)(s^+) \cong \mathop{\operatorname {colim}}_{(\iota \downarrow s^+)}M(s), \qquad (\operatorname {Ran}_{\iota }M)(s^+) \cong \mathop{\operatorname {lim}}_{(s^+\downarrow \iota )}M(s). \]

The left extension therefore propagates old semantics through the generators and relations directed into \(s^+\); the right extension gathers compatible semantics constrained by arrows directed back toward the old theory. It is often useful to read the former as a free or generative transport and the latter as a compatibility envelope. Those phrases describe universal properties, not probabilities, causal interventions, or empirical validity.

The unit and counit

\[ M\longrightarrow \iota ^*\iota _!M, \qquad \iota ^*\iota _*M\longrightarrow M \]

make continuity with the old theory explicit. If \(\iota \) is fully faithful, the corresponding ambient Kan extension recovers \(M\) on the old objects. For a genuine sketch doctrine, however, an ambient pointwise Kan extension need not preserve the products, limits, tensors, covers, or tangent structure required of a model. One must prove that \(\iota _!\) or \(\iota _*\) exists inside the relevant model categories, or apply an explicitly justified reflection back into them. In enriched or internal settings the needed construction is an enriched or internal Kan extension [ Kelly , 1982 ] . Existence is an admission obligation, not notation.