Process algebra and topos theory developed independently for decades. Process algebra classifies computational systems by how they behave — bisimulation, trace equivalence, simulation — organized into a spectrum of behavioral equivalences ordered by coarseness. Topos theory classifies mathematical structures by their internal logic — each geometric theory has a classifying topos that captures exactly the provable properties of its models. Both fields ask the same question from different directions: when are two systems the same?
They are aspects of a single structure.
Each labeled transition system receives a geometric theory whose classifying topos encodes its observable properties. Grothendieck topologies on the site of observations yield equivalence relations that correspond precisely to the behavioral equivalences from process algebra. Bisimulation, simulation, and trace equivalence emerge as different levels of topological refinement on the same underlying categorical structure. The hierarchy is not imposed — it is generated by the mathematical framework.
The unification reveals structure invisible to either field alone. Thirty behavioral equivalences organize as a finite sub-poset of an infinite coframe, seventeen of which are hybrid variants that had never been named. The observation-class approach — standard in process algebra for defining equivalences — proves inadequate for simulation, a limitation undetectable from within process algebra's own framework. The topos-theoretic perspective diagnoses the failure and provides the correct generalization.
The proofs are constructive, formalized in Lean 4. Mutual simulation is strictly coarser than bisimulation, which is strictly coarser than topos equivalence. Each level preserves different properties, and the inclusions are proper — there exist systems distinguishable by finer equivalences that are indistinguishable by coarser ones.
Two fields studying the same question in different languages. The translation reveals what neither language could express alone.