symmetric monoidal (∞,1)-category of spectra
Dialgebras subsume the notion of algebras for an endofunctor and coalgebras for an endofunctor. They were originally introduced by Lambek as “subequalizers”.
For categories $C, D$ and functors $F, G: C \to D$, a dialgebra of $F$ and $G$ (or an $(F, G)$-dialgebra) is an object $X$ in $C$ (the carrier) and a morphism $\alpha\colon F(X) \to G(X)$.
A homomorphism between two $(F, G)$-dialgebras $(X, \alpha)$ and $(Y, \beta)$ is a morphism $m\colon X \to Y$ in $C$ such that the following square commutes (that is, that $\alpha$ and $\beta$ form $X$- and $Y$-components of a natural transformation from $F$ to $G$):
Composition of such morphisms of algebras is given by composition of the underlying morphisms in $C$. This yields the category of $(F, G)$-dialgebras, $\text{Dialg}(F, G)$, which comes with a forgetful functor to $C$.
When $C = D$, then an algebra for an endofunctor is simply an $(F, id_C)$-dialgebra and a coalgebra for an endofunctor is simply an $(id_C, F)$-dialgebra.
Initial dialgebras provide categorical semantics for inductive-inductive types.
Dialgebras can be used to provide semantics to interactive programs; coalgebras have also been frequently used for the purpose. In contrast, dialgebras provide a natural way to express interactions (using the functor $F$). Semantics in dialgebras is not obtained via final objects (which are frequently absent in categories of dialgebras), but rather via quotients.
Joachim Lambek, Subequalizers, 1970
Tatsuya Hagino, A Typed Lambda Calculus with Categorical Type Constructors, 2005, link
Thorsten Altenkirch, Peter Morris, Fredrik Nordvall Forsberg, Anton Setzer, A Categorical Semantics for Inductive-Inductive Definitions, CALCO, 2011 link
Vincenzo Ciancia, Interaction and Observation: Categorical Semantics of Reactive Systems Trough Dialgebras, CALCO, 2013 link
Alwin Blok, Interaction, observation and denotation. A study of dialgebras for program semantics Master Thesis, Institute for Logic, Language and Computation, University of Amsterdam. link
Last revised on October 7, 2021 at 00:47:55. See the history of this page for a list of all contributions to it.