symmetric monoidal (∞,1)-category of spectra
Dialgebras subsume the notion of algebras for an endofunctor and coalgebras for an endofunctor.
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.
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.