.. meta::
   :description: Reference sheet — Coalgebra and bisimulation for infinite processes in matheology forge sessions.
   :keywords: coalgebra, bisimulation, coinduction, final coalgebra, infinite process, th11, matheology

***********************************************************************
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.