# nLab dialgebra

Contents

category theory

## Applications

#### Algebra

higher algebra

universal algebra

# Contents

## Idea

Dialgebras subsume the notion of algebras for an endofunctor and coalgebras for an endofunctor. They were originally introduced by Lambek as “subequalizers”.

## Definition

###### Definition

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$):

$\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 $C$. This yields the category of $(F, G)$-dialgebras, $\text{Dialg}(F, G)$, which comes with a forgetful functor to $C$.

###### Remark

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.

## 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 $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