F-coalgebra

In mathematics, specifically in category theory, an formula_1-coalgebra is a structure defined according to a functor formula_1, with specific properties as defined below. For both algebras and coalgebras, a functor is a convenient and general way of organizing a signature. This has applications in computer science: examples of coalgebras include lazy, infinite data structures, such as streams, and also transition systems.
formula_1-coalgebras are dual to formula_1-algebras. Just as the class of all algebras for a given signature and equational theory form a variety, so does the class of all formula_1-coalgebras satisfying a given equational theory form a covariety, where the signature is given by formula_1.
Definition.
Let 
be an endofunctor on a category formula_8.
An formula_1-coalgebra is an object formula_10 of formula_8 together with a morphism 
of formula_8, usually written as formula_14.
An formula_1-coalgebra homomorphism from formula_14 to another formula_1-coalgebra
formula_18 is a morphism 
in formula_8 such that 
Thus the formula_1-coalgebras for a given functor "F" constitute a category.
Examples.
Consider the endofunctor formula_23 that sends a set to its disjoint union with the singleton set formula_24. A coalgebra of this endofunctor is given by formula_25, where formula_26 is the so-called conatural numbers, consisting of the nonnegative integers and also infinity, and the function formula_27 is given by formula_28, formula_29 for formula_30 and formula_31. In fact, formula_32 is the terminal coalgebra of this endofunctor.
More generally, fix some set formula_10, and consider the functor formula_34 that sends formula_35 to formula_36. Then an formula_1-coalgebra formula_38 is a finite or infinite stream over the alphabet where formula_35 is the set of states and formula_27 is the state-transition function. Applying the state-transition function to a state may yield two possible results: either an element of formula_10 together with the next state of the stream, or the element of the singleton set formula_42 as a separate "final state" indicating that there are no more values in the stream.
In many practical applications, the state-transition function of such a coalgebraic object may be of the form formula_43, which readily factorizes into a collection of "selectors", "observers", "methods" formula_44. Special cases of practical interest include observers yielding attribute values, and mutator methods of the form formula_45 taking additional parameters and yielding states. This decomposition is dual to the decomposition of initial formula_1-algebras into sums of 'constructors'.
Let "P" be the power set construction on the category of sets, considered as a covariant functor. The "P"-coalgebras are in bijective correspondence with sets with a binary relation. 
Now fix another set, "A". Then coalgebras for the endofunctor "P"("A"×(-)) are in bijective correspondence with labelled transition systems, and homomorphisms between coalgebras correspond to functional bisimulations between labelled transition systems.
Applications.
In computer science, coalgebra has emerged as a convenient and suitably general way of specifying the behaviour of systems and data structures that are potentially infinite, for example classes in object-oriented programming, streams and transition systems. While algebraic specification deals with functional behaviour, typically using inductive datatypes generated by constructors, coalgebraic specification is concerned with behaviour modelled by coinductive process types that are observable by selectors, much in the spirit of automata theory. An important role is played here by final coalgebras, which are complete sets of possibly infinite behaviours, such as streams. The natural logic to express properties of such systems is coalgebraic modal logic.