3 Category-Theoretic Interface and Terminality
The ISAR kernel provides a category-theoretic interpretation of representation-free substrates and semantic views. We formalize this using the category of semantic kernels and morphisms, and prove that the canonical invariant quotient space is a terminal object in this category. This universal property of terminality establishes the mathematical foundation of view-independence.
3.1 The Category of Semantic Kernels
The definitions and structures in this section are mechanically verified in src/ISAR/KernelCategory.lean and src/ISAR/DialectKernel.lean. We define the category \(\mathcal{K}\) of admissible semantic kernels over the substrate.
An admissible semantic kernel \(K \in \mathcal{K}\) consists of:
A carrier type \(\text{Carrier}\).
A view mapping \(\text{view\_ of} : \text{ISKSubtype} \to \text{Carrier}\).
An observational equivalence relation \(\approx \) on \(\text{Carrier}\).
A soundness property: operational equivalence in the substrate implies view equivalence:
\[ \forall t, u, \quad t \sim _{op} u \implies \text{view\_ of } t \approx \text{view\_ of } u \]A decoding/reconstruction mapping \(\text{decode} : \text{Carrier} \to \text{ISKSubtype}\).
Coherence axioms:
\(\text{decode}(\text{view\_ of } t) \sim _{op} t\)
\(\text{view\_ of}(\text{decode } c) \approx c\)
\(c_1 \approx c_2 \implies \text{decode } c_1 \sim _{op} \text{decode } c_2\)
The identity kernel mapping the substrate directly to itself is the canonical presentation.
The computable kernel parametrized by normalization fuel.
The computable kernel instantiated with optimal fuel computed from the term size for linearly-typed terms.
A morphism \(f : K_1 \to K_2\) in the category \(\mathcal{K}\) is a carrier mapping \(\text{hom} : K_1.\text{Carrier} \to K_2.\text{Carrier}\) that:
Preserves the view representations: \(\forall t \in \text{ISKSubtype}, \quad K_2.\text{view\_ of } t \approx _2 \text{hom}(K_1.\text{view\_ of } t)\)
Respects carrier equivalence: \(\forall c_1, c_2, \quad c_1 \approx _1 c_2 \implies \text{hom}(c_1) \approx _2 \text{hom}(c_2)\)
For any kernel \(K\), the canonical homomorphism into \(\text{ISAR\_ Kernel}\) is defined by the decoding mapping.
3.2 Universal Factorization and Terminality
The uniqueness and terminality theorems are formalized and proved in src/ISAR/KernelCategory.lean. We prove that the canonical representation-free kernel is terminal, meaning that any admissible view can be uniquely decoded into it.
Any structure-preserving morphism \(f : K \to \text{ISAR\_ Kernel}\) is observationally equivalent to the canonical decoding morphism:
The quotient of the morphism space \(\text{KernelHom } K\ \text{ISAR\_ Kernel}\) modulo observational equivalence is a singleton:
Thus, \(\text{ISAR\_ Kernel}\) is a terminal object in the category \(\mathcal{K}\) of semantic kernels.
This category-theoretic result is not a naming convention: it is an algebraic theorem stating that the Invariant Layer is the unique (up to isomorphism) cofinal quotient that retains only the information visible to observational equivalence. Any other view is mathematically guaranteed to factor uniquely through it, separating the dialect-specific representation from the coordinate-free invariant semantics.
3.3 The Dialect Subsystem
The Dialect structures in this section are verified in src/ISAR/DialectKernel.lean. A Dialect is an alternative abstract view over the substrate.
A Dialect specifies:
A type of dialect objects.
A type of observations and observational equivalence.
An evaluation mapping, an encoder to substrate terms, and a decoder from the substrate.
A coherence law: evaluation commutes with encoding and decoding.