Zhixuan Yang on Nostr: For a fixed set \(\Sigma\), let \(C : Set \to Set\) be the functor \(2 \times ...

For a fixed set \(\Sigma\), let \(C : Set \to Set\) be the functor \(2 \times ({-})^\Sigma\). A \(C\)-coalgebra \(S, c : S \to C S\) is exactly a deterministic transition system: every element \(s \in S\) is a state, \(\pi_1(c(s))\) tells us whether \(s\) is an accepting state, \(\pi_2(c(s)) : \Sigma \to S\) tells us the new state for each input \(\in\Sigma\).

Let \(C_*\) be the cofree comonad over \(C\). An element of \(C_*1\) is an infinite \(\Sigma\)-branching tree with every node labelled by 2. Such a tree should be thought of as a "behaviour" of a state s in a deterministic transition system — it tells you starting from this state s, after making a series of transitions, whether you are still in an accepting state. For every coalgebra \((S, c)\), there is a map \(\mathit{unfold} : S \to C_* 1\) that "unrolls" every state to its behaviour.

Define category \(\mathbb{B}\) to have objects \(C_*1\) and morphisms \(\mathbb{B}(b_1, b_2) := \{ p \in \Sigma^* \mid b_1 ! p = b_2\}\), where \(b_1 ! p = b2\) means that \(b_2\) is the subtree of \(b_1\) after descending along the path \(p\).

Then I claim the category of coalgebras of \(C\), i.e. deterministic LTSs, is equivalent to the functor category \([\mathbb{B}, Set]\). A coalgebra \(S, c : S \to C S\) corresponds to the functor \(F : \mathbb{B} \to Set\) sending every \(b \in \mathbb{B}\) to the set \(\{s \in S \mid \mathit{unfold}(s) = b\}\). And the action of \(F\) on every morphism \(p \in \mathbb{B}(b_1, b_2)\) sends every \(s \in F b_1\) to the state obtained by running \(p\) from \(s\).