The attached full manuscript develops a categorical expansion of the source note, Semantic Uniqueness and Non-Uniqueness of Machine Realizations. The PDF contains the complete proofs, further examples, and notes on prior work.
Observations and the space of realizers
Let $\mathcal C$ be an $\infty$-category of machines and $\operatorname{Op}:\mathcal C\to\mathcal X$ an operational functor into an $\infty$-topos. Set $Q_n=\tau_{\le n}\operatorname{Op}$ for $n\ge-2$. Two machines share a degree-$n$ semantic class when their images under $Q_n$ are equivalent.
For a functor $Q:\mathcal C\to\mathcal D$ and $p\in\mathcal D$, define $$ \operatorname{Real}_Q(p)=\mathcal C^\simeq\times_{\mathcal D^\simeq}\{p\}. $$ Its objects are pairs $(M,\alpha:QM\simeq p)$. A path to $(N,\beta)$ is a machine equivalence $u$ together with a homotopy $\beta Q(u)\simeq\alpha$. Thus the path space is the homotopy fiber of $\operatorname{Eq}_{\mathcal C}(M,N)\to\operatorname{Eq}_{\mathcal D}(QM,QN)$ over $\beta^{-1}\alpha$. The categorical pullback $\mathcal C\times_{\mathcal D}\{p\}$ also retains noninvertible arrows with compatible images.
A discrete two-object category mapped to a point shows that conservativity need not distinguish inequivalent objects. The one-object category with additive endomorphism monoid $\mathbb N$ shows that a nonconservative functor can still distinguish all source classes. If each target equivalence is represented by a source arrow, conservativity implies injectivity on classes. Full faithfulness on cores holds exactly when every marked fiber is empty or contractible. For $BG\to BH$ induced by a group homomorphism $\phi$, the fiber is the action groupoid for right multiplication on $H$ through $\phi$. Its components are the cosets $h\phi(G)$ and each is equivalent to $B\ker\phi$.
Truncation and changes of interface
Truncation preserves finite products. Thus if $T$ is a machine operation with $\operatorname{Op}(TM)\simeq\operatorname{Op}(M)\times D$ naturally and $\tau_{\le n}D\simeq 1$, then $Q_nT\simeq Q_n$. A difference at degree $n+1$ certifies that the machines are inequivalent. In spaces the choice $D=K(A,n+1)$ for a nontrivial abelian group $A$ and $n\ge0$ supplies such a difference on a machine with contractible operational object.
Relative truncation commutes with base change because the connected–truncated factorization is stable under pullback. If $B$ is already $n$-truncated, the truncation of a pullback over $B$ is the pullback of the truncations. This follows by identifying relative and absolute truncation over such a base and using product preservation in the slice. In contrast, the pullback of the two base-point maps into $K(A,n+1)$ is $K(A,n)$, whereas the pullback of the truncated diagram is a point. Composition by matching can reveal homotopy discarded by separate observations.
The homotopy fiber of $BC_2\to K(\mathbb F_2,3)$ classifying the nonzero cube of the degree-one cohomology generator has the same homotopy groups as $BC_2\times K(\mathbb F_2,2)$. The two types are inequivalent because only the latter has a section over its $1$-truncation. When the operational objects and $p$ are recovered by their Postnikov towers, the full-precision marked realization space is the inverse limit of $\operatorname{Real}_{Q_n}(\tau_{\le n}p)$. This follows by commuting limits with marked pullbacks and using the truncation adjunction. Termwise inhabitation need not provide compatible points.
Specifications, traces, and a canonical quotient
A finite presentation has one realized semantic class when the semantic image of its sound realizers has exactly one component. This can follow from a structural rule or a universal property. A finite list of tests alone may leave distinct behaviors, since a unary transducer can delay its first differing output beyond every test length.
A coherent trace factorization means a functor $R_n$ and a natural equivalence $R_nT\simeq Q_n$, where $T$ is a trace functor. If $T$ exhibits localization at $W$, the factorization exists exactly when $Q_n$ inverts $W$, by the universal property of localization. In other cases it requires a separate argument. For example, two nondeterministic systems can have the same trace language but different branching behavior when different successor choices permit different extensions of a trace.
For a reachable initialized deterministic Mealy machine with behavior $b$, let $D_b$ be the set of derivatives $b_w(v)=b(wv)$. With transitions given by derivatives and initial state $b$, $D_b$ is itself reachable. A strict initialized homomorphism is determined on the state reached by each word, so the residual map onto $D_b$ is unique and surjective. This gives terminality and the sharp size bound for finite machines. The entire category of reachable realizers is equivalent to the poset of right congruences on words refining equality of derivatives. Its core is the discrete set of those congruences. In particular the unary constant-zero $m$-cycles are pairwise inequivalent and admit a strict quotient from length $m$ to length $d$ exactly when $d$ divides $m$.
Local and directed realization
An internal machine map $\mathscr M\to\mathscr B$ in a sheaf $\infty$-topos gives a marked realization object $U\times_{\mathscr B}\mathscr M$ for a specification $U\to\mathscr B$. Its sections are the totalization of sections over the Cech nerve of an effective cover by the mapping property of the Cech colimit. Local inhabitation can fail to yield a global section, as for the regular $C_2$-set in the topos of $C_2$-actions. A global section would be a fixed point.
For a timeline $u:I\to B$ into a semantic space, the comma space $|b\downarrow u|$ is the homotopy fiber of $|I|\to B$ at $b$. The comma category is the Grothendieck construction of $i\mapsto\operatorname{Map}_B(b,u(i))$. Its groupoid completion is the colimit of this diagram, which is also the pullback at $b$ of the colimit of the diagram of points over $B$. Coverage requires inhabitation of the comma spaces, while finality requires contractibility. A constant directed timeline into $BH$ covers its class and fails finality for nontrivial $H$.
Recursive improvement and feasible paths
To lift a semantic orbit to a machine trajectory requires a category of semantic updates, a functor from allowed machine updates, and a section over the orbit diagram. Nonempty stage fibers are insufficient. Even edges over each consecutive step can fail to compose when they use different intermediate machines. A coCartesian fibration supplies forward lifts from a specified initial machine by transporting along consecutive semantic edges. A cost or progress condition is an additional ingredient of an improvement claim.
For a fixed orbit in sets, let $\Gamma(U)$ be the states with a certified edge into $U$. Using dependent choice, a state admits an infinite continuation exactly when it belongs to the greatest fixed point of $\Gamma$. With finite branching this is the intersection of the finite-horizon viable sets. A state surviving every horizon has a successor in the intersection of the nested nonempty finite sets of viable successors, which proves the fixed-point assertion.
For a prefix-monotone cost and a fixed starting machine with arbitrarily long legal paths in a finitely branching tree, the minimum infinite-path cost equals the supremum of finite-horizon minima. The subtree of prefixes whose costs are at most this supremum contains paths at every depth and is prefix closed, so it has an infinite branch. The analogous intersection argument handles nested observation constraints when the same finitely branching tree supports every finite horizon and every observation degree. A computable finitely branching tree can have infinite paths with no computable one, as the manuscript shows by diagonalization.
Prior work and scope
- Lurie's Higher Topos Theory supplies the truncation, descent, and coCartesian fibration background. See also Kerodon, Section 7.2.3 for finality.
- Rutten's universal coalgebra supplies the final-coalgebra context. Joyal, Nielsen, and Winskel treat path lifting and bisimulation. Milner gives the program-semantics context for full abstraction.
- Hatcher's Algebraic Topology gives the cohomology and Postnikov tools. Clausen and Mathew give background on hyperdescent and Postnikov completeness.
- Tarski supplies the lattice-theoretic fixed-point argument used for viability.
The manuscript uses proofs and counterexamples as evidence. Its conclusions depend on the operational functor, machine equivalences, update certificates, and the stated branching and cost hypotheses. Generative AI assisted in drafting, mathematical development, and preparation of references. The responsible author or research group is identified through the submission form.