nLab
dialgebra

Contents

Context

Category theory

Algebra

Contents

Idea

Dialgebras subsume the notion of algebras for an endofunctor and coalgebras for an endofunctor.

Definition

Definition

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.

Remark

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.

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.