Reference Sheet 9: Coalgebra & Bisimulation for Infinite Processes

Target audience: Forge auditor who knows S5 modal logic, CEM, FOL, basic game theory, and the contents of Sheets 1–8 but needs coalgebra for formalizing th11 (Stakes Without Death) and reasoning about persistent, potentially infinite processes.

1. Orientation

Algebra builds up: start with constructors, combine them into finite structures, reason by induction (“if it holds for the base case and the inductive step, it holds for all finite structures”). Coalgebra observes out: start with a system that produces observations, reason by coinduction (“if two systems produce the same observations at every step, they are the same”). The duality is fundamental. Algebra is the mathematics of finite construction; coalgebra is the mathematics of infinite behavior.

th11 (Stakes Without Death) posits finite agents with eternal stakes in an infinite game. Classical algebraic reasoning cannot directly handle “infinite stakes” — induction stops at finite horizons. Coalgebra handles this natively: the infinite game is a coalgebra, its observable behavior is a stream of game states, and the question “do two strategies lead to the same infinite outcome?” is answered by bisimulation. ax21 (Permanent Mediator) posits a role that persists indefinitely — a coinductive object par excellence.

None of the existing 8 sheets address infinite processes directly. Category theory (Sheet 1) provides the language; coalgebra uses that language to model systems whose behavior unfolds without bound.

2. Key Concepts

Coalgebra for a functor. Given an endofunctor F: C → C, an F-coalgebra is a pair (X, γ) where X is an object (the state space) and γ: X → F(X) is a morphism (the transition/observation structure). Contrast with F-algebra: (A, α: F(A) → A), which folds structure in. A coalgebra unfolds structure out.

Example: For F(X) = A × X (where A is an observation type), an F-coalgebra is a system that, given a state, produces an observation in A and a next state. This is a stream producer — an infinite sequence of A-values.

Matheology use: The infinite game in th11 is a coalgebra. At each step, the game state produces an observable outcome (who benefits, what innovations occur, what consequences follow) and transitions to a next state. The functor F encodes what “one step” of the game looks like.

Final coalgebra. An F-coalgebra (Z, ζ: Z → F(Z)) is final if for every F-coalgebra (X, γ) there exists a unique coalgebra morphism h: X → Z. The final coalgebra is the “canonical infinite behavior” — it classifies all possible infinite unfoldings up to observational equivalence.

Matheology use: The final coalgebra for the infinite game functor is “the” canonical space of all possible infinite game trajectories. Every specific strategy maps uniquely into this space. Two strategies that produce the same trajectory (same map into the final coalgebra) are the same strategy from an observational standpoint.

Bisimulation. A bisimulation between coalgebras (X, γ) and (Y, δ) is a relation R ⊆ X × Y such that if (x, y) ∈ R, then the observations from x and y are “compatible” and the successor states are again related by R. Formally: there exists an F-coalgebra structure on R making both projections coalgebra morphisms.

Two states are bisimilar if they are related by some bisimulation. Bisimilar states are observationally indistinguishable — no finite sequence of observations can tell them apart.

Matheology use: Two formulations of ax21 (Permanent Mediator) describe bisimilar processes if they produce the same sequence of mediator-actions at every step, regardless of how the internal mechanism differs. Bisimulation is the right equivalence for persistent roles: not “built the same way” but “acts the same way forever.”

Coinduction (proof principle). To prove that two states are bisimilar (observationally equal), exhibit a bisimulation containing them. This is the coinductive counterpart of induction. Where induction proves a property holds for all finite constructions by checking base and step, coinduction proves two infinite behaviors are the same by checking that each step preserves the relation.

Matheology use: To prove that two Jubilee-System cycle strategies produce the same infinite economic trajectory, construct a bisimulation: show that at each cycle boundary, the two strategies produce the same observable outcomes and enter bisimilar next-cycle states.

Stream and colist. A stream over A is an element of the final coalgebra for F(X) = A × X: an infinite sequence of A-values. A colist is an element of the final coalgebra for F(X) = 1 + A × X: a possibly-infinite sequence (may terminate). Streams and colists are the coinductive counterparts of lists (inductive, necessarily finite).

Matheology use: The “eternal stakes” in th11 are a stream: an infinite sequence of stake-states, one for each period of the game. The game itself may or may not terminate — if it can terminate, it is a colist. th11 claims stakes are eternal (stream), not merely potentially long (colist).

Coalgebraic modal logic. Modal operators (□, ◇ from S5) can be given coalgebraic semantics: □φ holds at state x if φ holds at all states reachable from x in one F-step. This unifies modal logic with coalgebraic state-transition reasoning. Different functors F yield different modal logics.

Matheology use: The existing S5 modal logic for PET can be understood coalgebraically: each possible world is a state, the accessibility relation is the coalgebra structure, and □ and ◇ are the corresponding modal operators. This embeds S5 into the coalgebraic framework without changing its content — but opens the door to extending it with coalgebraic temporal operators (always, eventually, until) needed for reasoning about infinite game trajectories in th11.

Corecursion (definition principle). To define a function into a final coalgebra, specify what observation it produces at each step as a function of the input. The unique coalgebra morphism (guaranteed by finality) then defines the complete infinite behavior. This is the coinductive counterpart of recursion: recursion defines functions out of initial algebras; corecursion defines functions into final coalgebras.

Matheology use: To define the infinite game trajectory starting from any initial economic state, specify the one-step outcome function (what happens in one Jubilee cycle). Corecursion then uniquely determines the infinite trajectory — no need to reason about “what happens at infinity” directly.

Coalgebra morphism. A function h: X → Y between coalgebras (X, γ) and (Y, δ) such that δ ∘ h = F(h) ∘ γ. This is the structure-preserving map for coalgebras — the coinductive counterpart of algebra homomorphisms. Every coalgebra morphism induces bisimilar states: h(x) is bisimilar to x for all x.

Matheology use: A model simplification (reducing the state space of the economic dynamics) is valid if it is a coalgebra morphism: the simplified model produces the same observations as the full model at every step.

3. Critical Theorems

Lambek’s lemma (coalgebraic version). The structure map of a final coalgebra ζ: Z → F(Z) is an isomorphism: Z ≅ F(Z). The final coalgebra is a fixed point of the functor. For streams: the type of infinite sequences over A satisfies Stream(A) ≅ A × Stream(A) — an infinite sequence is an element followed by an infinite sequence. Why it matters: The infinite game’s canonical trajectory space is self-similar: the game from step n onward has the same structure as the game from step 0. This justifies th11’s claim that eternal stakes are structurally coherent — they are not an ad hoc infinity but a fixed point of a well-defined functor.

Coinduction principle. Two states in an F-coalgebra are bisimilar if and only if they map to the same element of the final coalgebra (when it exists). Equivalently: bisimilarity is the largest bisimulation, and it coincides with equality in the final coalgebra. Why it matters: This gives a complete method for proving infinite behavioral equivalence. To show two strategies produce the same eternal outcome, it suffices to find any bisimulation relating them — the coinduction principle guarantees this implies full equality of infinite behavior.

Rutten’s fundamental theorem of universal coalgebra. For any set functor F that preserves weak pullbacks, the final F-coalgebra exists and bisimilarity is a congruence (compatible with the coalgebra structure). Moreover, the final coalgebra is the quotient of any coalgebra by bisimilarity. Why it matters: For reasonable game functors (and most are reasonable), the canonical trajectory space exists, and observationally equivalent strategies can be formally identified. This is the coalgebraic foundation that makes th11’s reasoning possible: the infinite game has a well-defined behavioral semantics.

Coalgebraic Hennessy-Milner theorem. For image-finite coalgebras, two states are bisimilar if and only if they satisfy the same modal formulas. Observational equivalence (bisimulation) and logical equivalence (same modal properties) coincide. Why it matters: The modal logic already used in PET (S5) can serve as the language for distinguishing infinite game trajectories. If two trajectories satisfy the same S5+temporal formulas, they are bisimilar — and vice versa. This connects the existing formal apparatus to the new coalgebraic framework without requiring a separate logical system.

Moss’s coalgebraic logic. For any set functor F, there is a canonical modal logic whose formulas are built from F’s structure. The modality ∇ (nabla) directly encodes one-step coalgebraic transitions. This logic is adequate: it distinguishes all non-bisimilar states. Why it matters: If the game functor F is specified (as part of formalizing th11), Moss’s construction automatically generates the “right” modal logic for reasoning about the game. This eliminates the need to manually design a temporal logic — it emerges from the functor.

4. Common Pitfalls

Trying to use induction on infinite objects. Induction proves properties of all finite prefixes of an infinite behavior. It does not prove properties of the infinite behavior itself. “Every finite prefix of the stream is good” does not imply “the stream is good” — the limit may introduce new phenomena. Use coinduction for properties of the whole infinite behavior.

Confusing final coalgebra with greatest fixed point. In a lattice-theoretic setting (like domain theory), final coalgebras often coincide with greatest fixed points. But in the category-theoretic setting, they are defined by a universal property, not by maximality. The distinction matters when the functor is not monotone on a lattice — the universal property still works but the lattice-theoretic characterization may fail.

Forgetting that bisimulation is coarser than equality. Two coalgebra states can be bisimilar (same observations) without being equal (same internal structure). This is a feature, not a bug — bisimulation captures observational equivalence, which is the relevant notion for external agents who cannot inspect internal states. But if the internal structure carries theological meaning (e.g., the mediator’s “inner state” matters in the model), bisimulation may be too coarse.

Assuming all coinductive objects are streams. Streams (F(X) = A × X) are the simplest coinductive type. Trees (F(X) = A × X^B, branching), processes with choice (F(X) = P(A × X), nondeterministic), and labeled transition systems (F(X) = (P(X))^A, input-driven) are all coalgebras with different structures. Match the functor to the system — th11’s infinite game likely has branching (choices at each step), making it tree-like rather than stream-like.

Neglecting well-foundedness concerns. Coinduction works for productivity — the system must produce an observation at each step. If the system can “stall” (produce no observation for an unbounded number of steps), the coalgebraic semantics may not apply directly. For th11, this means the infinite game must have a well-defined notion of “step” where something observable happens.

5. Bridge to Matheology

th11 (Stakes Without Death) as a coinductive theorem. th11 claims: eternal stakes are possible without infinite suffering. Coalgebraic formulation:

1. Define the game functor: F(X) = Outcome × X (simple stream) or F(X) = Outcome × X^{Action} (branching game tree). Outcome includes “stakes status” — the observable consequence for each agent.

2. Define the stake stream: By corecursion, specify how one period’s outcome leads to the next period’s initial state. The infinite game is the unique coalgebra morphism into the final coalgebra.

3. Prove the claim: Show that in the final coalgebra, there exist trajectories where (a) stakes are nonzero at every step (eternal stakes) but (b) no agent’s cumulative negative outcome diverges (no infinite suffering). This is a property of specific elements of the final coalgebra, proved by coinduction.

ax21 (Permanent Mediator) as a bisimulation class. ax21 posits a permanent mediation role. Different individuals may fill this role at different times, but the role’s observable behavior remains consistent. Coalgebraically: the mediator-role is an element of the final coalgebra for the mediation functor. Different individuals filling the role are different coalgebra states that are bisimilar — observationally indistinguishable from outside.

The question “is the mediator role well-defined?” becomes: is the bisimulation class nonempty? If yes, the role is coherent regardless of who fills it. If no, the role’s specification is internally contradictory.

Connecting to dynamical systems (Sheet 5). Sheet 5 models the system’s evolution as ẋ = f(x). Coalgebra models it as γ: X → F(X). The connection: discretizing the ODE at time steps Δt gives a coalgebra with F(X) = Observable × X, where the transition is x ↦ (observe(x), x + f(x)·Δt). The infinite trajectory in the final coalgebra corresponds to the solution curve φ_t(x₀) extended to all time. Basin of attraction (Sheet 5) corresponds to bisimulation class (this sheet): states in the same basin produce bisimilar infinite trajectories (both converge to the same attractor).

Connecting to HoTT (Sheet 2). In HoTT, coinductive types are defined as greatest fixed points of type operators, dual to inductive types (least fixed points / HITs). The infinite game in th11 can be defined as a coinductive type in HoTT, giving it computational content: a proof that an infinite trajectory has a certain property is a program that, at each step, produces evidence for that step and a continuation for the rest.

Connecting to ergodic theory (Sheet 6). Ergodic theory asks: does the infinite trajectory visit all regions? Coalgebra asks: what does the infinite trajectory look like? These are complementary. An ergodic coalgebra (if such a notion can be made precise — this is a research question) would be one where every element of the final coalgebra visits every observable region. This connects th9 (ergodicity) to th11 (infinite stakes) at a deep structural level.

New questions coalgebra enables:

• Is the infinite game in th11 a stream coalgebra (linear time) or a tree coalgebra (branching choices at each step)? The answer determines whether th11’s “stakes” are a single inevitable future or a branching tree of possibilities.

• Are the two attractors from th8 (river of life, BABL) distinguishable by bisimulation? If so, from what point in the game can an observer determine which attractor the trajectory is converging to?

• Can the Jubilee-System cycle (ax25) be formalized as a periodic coalgebra — one whose behavior repeats with period equal to the cycle length? If so, the infinite trajectory is determined by a single cycle, dramatically simplifying analysis.

• What is the coalgebraic modal logic for the game functor in th11? Moss’s construction would generate it automatically — providing the “right” temporal language for reasoning about eternal stakes.