Projects
Path Constraints
Something I've been really interested in lately are what I've been calling (coalgebraic) path constraints. For details, if you really want to grasp what's below, you should check out the paper, Coalgebraic Path Constraints, presented at CMCS 2026.
But anyway, for the sake of making this page even somewhat self-contained, here are the relevant definitions.
Definition. (Path Shape)
Let \(F \colon \mathbf C \to \mathbf C\) be an endofunctor on a complete category \(\mathbf C\).
The set \(\mathrm{Shape}(F)\) of path shapes generated by \(F\) is the set of functors obtained from the following grammar
\[
\mathrm{Shape}(F) \ni J,K,J_i ::= \mathrm{Id} \mid F \mid \prod_{i \in I} J_i \mid K \circ J
\]
where \(I\) ranges over sets.
Given a coalgebra \(\beta \colon X \to FX\), its corresponding \(J\)-step coalgebra is the coalgebra \(\beta^J \colon X \to JX\) constructed inductively by
\[\begin{gathered}
\beta^{\mathrm{Id}} = \mathit{id}_X
\quad
\beta^F = \beta
\quad
\beta^{\prod J_i} = \langle J_i\rangle_{i \in I}
\quad
\beta^{K \circ J} = K(\beta^J) \circ \beta^K
\end{gathered}\]
where the notation \(\langle -\rangle_{i \in I}\) denotes a tuple indexed by \(I\).
Definition. (Path Constraint)
Given a shape \(J \in \mathrm{Shape}(F)\), a path constraint of shape \(J\) is a subfunctor \(e \colon E \subseteq J\).
An \(F\)-coalgebra \(\beta \colon X \to FX\) satisfies \(E\) if \(\beta^J\) factors through \(e\) (that is, there exists an arrow \(g \colon X \to EX\) such that \(\beta^J = e_X \circ g\)).
Given a functor \(H \colon \mathbf C \to \mathbf C\), a path constraint \(e \colon E \subseteq J\) is called equational over \(H\) if there are two natural transformations \(\lambda,\rho \colon J \rightrightarrows H\) such that for any object \(X\), \[ EX \xrightarrow{e} JX \stackrel{\lambda_X, \rho_X}{\rightrightarrows} HX \] is an equalizer diagram. In this case, we write \(E = (\lambda \equiv \rho)\).
Given a functor \(H \colon \mathbf C \to \mathbf C\), a path constraint \(e \colon E \subseteq J\) is called equational over \(H\) if there are two natural transformations \(\lambda,\rho \colon J \rightrightarrows H\) such that for any object \(X\), \[ EX \xrightarrow{e} JX \stackrel{\lambda_X, \rho_X}{\rightrightarrows} HX \] is an equalizer diagram. In this case, we write \(E = (\lambda \equiv \rho)\).
Since they are pretty new, not a ton is known about the characterization of the coalgebraic properties that can be captured as equational path constraints. What follows is basically as many examples (that do not appear in the paper above) as I have come across and have been willing to put on paper. If you come up with one that you would like to share, please get in touch with me and your example will appear here with credit!
Examples
(Lassos)
A stream generator is a coalgebra for the functor \(F = B \times \mathrm{Id} \colon \mathbf {Set} \to \mathbf{Set}\).
A stream generator \(\langle o, \partial \rangle \colon X \to B \times X\) is a lasso if for any \(x \in X\), there are lengths \(p,l \in \mathbb N\) such that for any \(n > l\), \(\partial^{n + p} (x) = \partial^n(x)\).
This can be given a path constraint description with
\[
J = \prod_{n \in \mathbb N} (B \times \mathrm{Id})^n \cong \prod_{n \in \mathbb N} B^n \times \mathrm{Id}
\]
and
\[
EX = \{(v_n, x_n)_{n \in \mathbb N} \mid \exists p,l, \text{ for any \(n > l\), \(x_{n+p} = x_n\)}\} \subseteq JX
\]
Is this equational?
(Deterministic Transition Systems)
This property is captured by the modal formula \(\Diamond p \to \Box p\) on transition systems \(\beta \colon X \to \mathcal P X\), where \(\mathcal P\) is the covariant powerset functor on \(\mathbf{Set}\).
Essentially what it says is that for any states \(x,y,z\) in \(X\), if \(x \to y\) and \(x \to z\), then \(y = z\).
This is equational for the following transformations:
\[\begin{aligned}
\lambda,\rho \colon J = \mathrm{Id} \times \mathcal P &\rightrightarrows H = \mathcal P^2
\\
\lambda_X(x, U) &= \{\{\}\} \cup \{\{y\} \mid y \in X\} \qquad\text{(this is constant)} \\
\rho_X(x, U) &= \{U\} \cup \lambda_X(x, U)
\end{aligned}\]
The basic idea is that \(\lambda_X \circ \beta^J(x) = \rho_X \circ \beta^J(x)\) iff \(\beta(x)\) is a subset of \(X\) of size at most \(1\).
(Local Finiteness)
Given a transition system \(\beta \colon X \to \mathcal P X\), we say that it is locally finite if for any \(x \in X\), the set of states reachable from \(x\) is finite.
This property is captured by the following path constraint.
\[
J = \prod_{n \in \mathbb N} \mathcal P^n
\qquad
EX = \{(\Phi_n)_{n\in \mathbb N} \mid \bigcup_n \Phi_n \text{ is finite}\} \subseteq J
\]
Is this equational?
(This probably generalizes to arbitrary monads in place of \(\mathcal P\).)
(This probably generalizes to arbitrary monads in place of \(\mathcal P\).)
(Euclidean Transition Systems)
These correspond to the modal S5 axiom \(\Diamond p \to \Box \Diamond p\).
Essentially, this says that in a transition system \(\beta \colon X \to \mathcal P X\), if \(x \to y\) and \(x \to z\), then \(y \to z\) (and therefore also \(z \to y\)).
In this scenario, we take
\[\begin{aligned}
\lambda,\rho \colon J = \mathcal P \times \mathcal P^2 &\rightrightarrows H = \mathcal P^2
\\
\lambda_X(U, \Phi) &= \{U \cup V \mid V \in \Phi\} \\
\rho_X(U, \Phi) &= \Phi
\end{aligned}\]
The basic idea is that \(\beta^2(x) = \{\beta(x) \cup \beta(y) \mid y \in \beta(x)\}\) if and only if \(\beta(x) \subseteq \beta(y)\) for every \(y \in \beta(x)\).