ora-0119

9.6 Online Kan invariance

Ordinary Kan invariance says that a behavioral property depends only on the induced semantics \(\widehat F\), not on the syntactic presentation of \(F\). The online analogue must remember both every prefix semantics and the maps relating different prefixes.

Definition 9.4 Online Kan invariance

A property of filtered decision models is online Kan-invariant if it depends only on the natural-isomorphism class of

\[ \widehat{\mathbf F}:\mathbb T\to [\mathcal Q,\mathcal D]. \]

Two online models \(M,N\) are online Kan-bisimilar when

\[ \widehat{\mathbf F}^{\, M} \cong \widehat{\mathbf F}^{\, N} \]

naturally in time and decision context.

Pointwise equivalence at every time is necessary but not sufficient: the chosen isomorphisms must commute with the persistence maps. For every \(s\leq t\), an online bisimulation \(\eta \) requires

\begin{equation} \eta _t\circ u^M_{s,t} = u^N_{s,t}\circ \eta _s. \end{equation}

9.2

Theorem 9.5 Fixed-shape lifting of Kan invariance

Let \(\mathbb T,\mathcal{O},\mathcal C,\mathcal Q\) be small, let \(\mathcal D\) admit the relevant Kan extensions, and hold \(J\) and \(K\) fixed through time. Then the UDL operator lifts pointwise to

\[ [\mathbb T,\mathsf U]: [\mathbb T,[\mathcal{O},\mathcal D]] \longrightarrow [\mathbb T,[\mathcal Q,\mathcal D]], \]

with

\[ ([\mathbb T,\mathsf U](\mathbf F))_t \cong \operatorname {Ran}_K\operatorname {Lan}_JF_t. \]

Consequently, online Kan invariance is ordinary Kan invariance internal to the time-indexed functor category. Two models are online Kan-bisimilar if and only if their prefixwise Kan semantics admit a family of natural isomorphisms satisfying 9.2.

Proof ▼

The adjunctions \(\operatorname {Lan}_J\dashv J^*\) and \(K^*\dashv \operatorname {Ran}_K\) lift pointwise to functor categories. Their composite at time \(t\) is therefore \(\operatorname {Ran}_K\operatorname {Lan}_JF_t\). An isomorphism in a functor category is precisely a componentwise isomorphism natural in the indexing category, and its naturality square is 9.2.

In particular, a fixed-shape evidence filtration obtains formal persistence maps by functoriality of \(\mathsf U\). This does not imply that those maps are monic, lossless, computationally reusable, or beneficial on later tasks; those are additional persistence obligations rather than consequences of Kan functoriality.

This equivalence is the minimal fixed-shape formulation: time indexing adds adaptedness and coherence but does not change the universal construction. It also explains why merely proving \(\widehat F^M_t\cong \widehat F^N_t\) separately for every \(t\) is inadequate. Arbitrarily chosen pointwise isomorphisms can fail to preserve how knowledge is updated.