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.

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.

References

• 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

Created on November 16, 2018 at 14:24:54. See the history of this page for a list of all contributions to it.