ora-0121

9.8 Persistent online abstractions

For a context object \(X\), define prefixwise behavioral equivalence by

\[ x\sim _t x' \quad \Longleftrightarrow \quad \widehat{\mathbf F}_t(x) \cong \widehat{\mathbf F}_t(x'). \]

Under conservative revelation, later semantics restricts to earlier semantics. Hence new evidence can split an earlier equivalence class but cannot identify behaviors that were already observably distinct:

\[ s\leq t \quad \Longrightarrow \quad \sim _t\; \subseteq \; \sim _s. \]

Proposition 9.7 Inverse system of online Kan quotients

Assume conservative revelation and the existence of the prefixwise quotients. Then \(s\leq t\) induces a canonical forgetting map

\[ X/{\sim _t}\longrightarrow X/{\sim _s}. \]

These maps satisfy identity and composition, so the minimal Kan-invariant abstractions form an inverse system, equivalently a presheaf on time.

Proof ▼

An isomorphism of later semantic values restricts to an isomorphism of the earlier values, so \(x\sim _t x'\) implies \(x\sim _s x'\). The quotient by the finer relation therefore maps canonically to the quotient by the coarser relation. Uniqueness of quotient factorization gives identity and composition.

This variance is important: evidence accumulates forward, whereas the operation that forgets newly learned distinctions points back toward the earlier quotient. If later evidence is allowed to revise rather than conservatively extend earlier semantics, these maps must be replaced by explicit repair comparisons.