nLab dialgebra



Category theory




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,DC, D and functors F,G:CDF, G: C \to D, a dialgebra of FF and GG (or an (F,G)(F, G)-dialgebra) is an object XX in CC (the carrier) and a morphism α:F(X)G(X)\alpha\colon F(X) \to G(X).

A homomorphism between two (F,G)(F, G)-dialgebras (X,α)(X, \alpha) and (Y,β)(Y, \beta) is a morphism m:XYm\colon X \to Y in CC such that the following square commutes (that is, that α\alpha and β\beta form XX- and YY-components of a natural transformation from FF to GG):

F(X) F(m) F(Y) α β G(X) G(m) G(Y). \array{ F(X) & \stackrel{F(m)}{\rightarrow} & F(Y) \\ \alpha\downarrow && \downarrow \beta \\ G(X) & \stackrel{G(m)}{\rightarrow} & G(Y) } \,.

Composition of such morphisms of algebras is given by composition of the underlying morphisms in CC. This yields the category of (F,G)(F, G)-dialgebras, Dialg(F,G)\text{Dialg}(F, G), which comes with a forgetful functor to CC.


When C=DC = D, then an algebra for an endofunctor is simply an (F,id C)(F, id_C)-dialgebra and a coalgebra for an endofunctor is simply an (id C,F)(id_C, F)-dialgebra.


Abstractly, the category of dialgebras is the inserter of FF and GG in the 2-category Cat.

Relationship to inductive-inductive types

Initial dialgebras provide categorical semantics for inductive-inductive types.

Relationship to program semantics (process calculi)

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 FF). 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

  • Erik Poll, Jan Zwanenburg, From Algebras and Coalgebras to Dialgebras, Electronic Notes in Theoretical Computer Science 44(1), May 2001, 289-307, (doi:10.1016/S1571-0661(04)80915-0).

  • 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

  • Jim de Groot, Dirk Pattinson, Modal Intuitionistic Logics as Dialgebraic Logics, LICS ‘20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science July 2020, 355–369 (doi:10.1145/3373718.3394807).

A dialgebraic account of labeled transition systems is in

  • Fabrizio Montesi, Marco Peressotti, Linear Logic, the π\pi-calculus, and their Metatheory: A Recipe for Proofs as Processes (arXiv:2106.11818)

Last revised on November 22, 2022 at 15:22:10. See the history of this page for a list of all contributions to it.