1–LABEL:LastPageOct. 27, 2017Sep. 24, 2018

# Proper Functors and Fixed Points for Finite Behaviour

Stefan Milius  Lehrstuhl für Informatik 8 (Theoretische Informatik),
Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany  mail@stefan-
milius.eu

###### Abstract.

The rational fixed point of a set functor is well-known to capture the
behaviour of finite coalgebras. In this paper we consider functors on
algebraic categories. For them the rational fixed point may no longer be fully
abstract, i.e. a subcoalgebra of the final coalgebra. Inspired by Ésik and
Maletti’s notion of a proper semiring, we introduce the notion of a proper
functor. We show that for proper functors the rational fixed point is
determined as the colimit of all coalgebras with a free finitely generated
algebra as carrier and it is a subcoalgebra of the final coalgebra. Moreover,
we prove that a functor is proper if and only if that colimit is a
subcoalgebra of the final coalgebra. These results serve as technical tools
for soundness and completeness proofs for coalgebraic regular expression
calculi, e.g. for weighted automata.

###### Key words and phrases:

proper functor, proper semiring, coalgebra, rational fixed point

Supported by the Deutsche Forschungsgemeinschaft (DFG) under project MI
717/5-1

##  1\. Introduction

Coalgebras allow to model many types of systems within a uniform and
conceptually clear mathematical framework [33]. One of the key features of
this framework is _final semantics_ ; the final coalgebra provides a fully
abstract domain of system behaviour (i.e. it identifies precisely the
behaviourally equivalent states). For example, the standard coalgebraic
modelling of deterministic automata (without restricting to finite state sets)
yields the set of formal languages as final coalgebra. Restricting to finite
automata, one obtains precisely the regular languages [32]. It is well-known
that this correspondence can be generalized to locally finitely presentable
(lfp) categories [8], where _finitely presentable_ objects play the role of
finite sets. For a finitary functor $F$ (modelling a coalgebraic system type)
one then obtains the _rational fixed point_ $\varrho F$, which provides final
semantics to all coalgebras with a finitely presentable carrier [25].
Moreover, the rational fixed point is _fully abstract_ , i.e. $\varrho F$ is a
subcoalgebra of the final one $\nu F$, whenever the classes of finitely
presentable and finitely generated objects agree in the base category and $F$
preserves non-empty monomorphisms [27, Section 5]. While the latter assumption
on $F$ is very mild, the former one on the base category is more restrictive.
However, it is still true for many categories used in the construction of
coalgebraic system models (e.g. sets, posets, graphs, vector spaces,
commutative monoids, nominal sets and positively convex algebras). Hence, in
these cases the rational fixed point $\varrho F$ is the canonical domain of
_regular_ behaviour, i.e. the behaviour of ‘finite’ systems of type $F$.

In this paper we will consider rational fixed points in algebraic categories
(a.k.a. finitary varieties), i.e. categories of algebras specified by a
signature of operation symbols with finite arity and a set of equations
(equivalently, these are precisely the Eilenberg-Moore categories for finitary
monads on sets). Being the target of generalized determinization [36], these
categories provide a paradigmatic setting for coalgebraic modelling beyond
sets. For example, non-deterministic automata, weighted or probabilistic
automata [23], or context-free grammars [43] are coalgebraically modelled over
the categories of join-semilattices, modules for a semiring, positively convex
algebras, and idempotent semirings, respectively. In algebraic categories one
would like that the rational fixed point, in addition to being fully abstract,
is determined already by those coalgebras carried by free finitely generated
algebras, i.e. precisely those coalgebras arising by generalized
determinization. In particular, this feature is used in completeness proofs
for generalized regular expressions calculi [37, 36, 12]; there one proves
that the quotient of syntactic expressions modulo axioms of the calculus is
(isomorphic to) the rational fixed point by establishing its universal
property as a final object for that quotient. A key feature of the settings in
loc. cit. is that it suffices to verify the finality only w.r.t. coalgebras
with a free finitely generated carrier.

The purpose of the present paper is to provide sufficient conditions on the
algebraic base category and coalgebraic type functor that ensure that the
rational fixed point is fully abstract and that such finality proofs are
sound. To this end we form a coalgebra that serves as the semantics domain of
all behaviours of target coalgebras of generalized determinization (modulo
bisimilarity on the level of these coalgebra). More precisely, let
$T:{\mathsf{Set}}\to{\mathsf{Set}}$ be a finitary monad on sets and
$F:{\mathsf{Set}}^{T}\to{\mathsf{Set}}^{T}$ be a finitary endofunctor
preserving surjective $T$-algebra morphisms (note that the last assumption
always holds if $F$ is lifted from some endofunctor on ${\mathsf{Set}}$). Now
form the colimit $\varphi F$ of the inclusion functor of the full subcategory
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ formed by all $F$-coalgebras of the
form $TX\to FTX$, where $X$ is a finite set. Urbat [41] has shown that
$\varphi F$ is a fixed point of $F$. We first first provide a characterization
of $\varphi F$ that uniquely determines it up to isomorphism: based on Adámek
et al.’s notion of a Bloom algebra [2], we introduce the new notion of an
_ffg-Bloom algebra_ , and we prove that, considered as an algebra for $F$,
$\varphi F$ is the initial ffg-Bloom algebra (Theorem 19).

Then we turn to the full abstractness of the rational fixed point $\varrho F$
and the soundness of the above mentioned finality proofs. Inspired by Ésik and
Maletti’s notion of a proper semiring (which is in fact a notion concerning
weighted automata), we introduce _proper functors_ (Definition 5), and we
prove that for a proper functor on an algebraic category the rational fixed
point is determined by the coalgebras with a free finitely generated carrier.
More precisely, if $F$ is proper, then the rational fixed point $\varrho F$ is
(isomorphic to) initial Bloom algebra $\varphi F$. Moreover, we show that a
functor $F$ is proper if and only if $\varphi F$ is a subcoalgebra of the
final coalgebra $\nu F$ (Theorem 22). As a consequence we also obtain the
desired result that for a proper functor $F$ the finality property of $\varrho
F$ can be established by only verifying that property for all coalgebras from
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ (Corollary 25).

In addition, we provide more easily established sufficient conditions on
${\mathsf{Set}}^{T}$ and $F$ that ensure properness: $F$ is proper if finitely
generated algebras of ${\mathsf{Set}}^{T}$ are closed under kernel pairs and
$F$ maps kernel pairs to weak pullbacks in ${\mathsf{Set}}$. For a lifting $F$
this holds whenever the lifted functor on sets preserves weak pullbacks; in
fact, in this case the above conditions were shown to entail Corollary 25 in
previous work [12, Corollary 3.36]. However, the type functor (on the category
of commutative monoids) of weighted automata with weights drawn from the
semiring of natural numbers provides an example of a proper functor for which
the above condition on ${\mathsf{Set}}^{T}$ fails.

Another recent related work concerns the so-called _locally finite fixed
point_ $\vartheta F$ [27]; this provides a fully abstract behavioural domain
whenever $F$ is a finitary endofunctor on an lfp category preserving non-empty
monomorphisms. In loc. cit. it was shown that $\vartheta F$ captures a number
of instances that cannot be captured by the rational fixed point, e.g. context
free languages [43], constructively algebraic formal power-series [30, 44],
Courcelle’s algebraic trees [13, 6] and the behaviour of stack machines [22].
However, as far as we know, $\vartheta F$ is not amenable to the simplified
finality check mentioned above unless $F$ is proper.

Putting everything together, in an algebraic category we obtain the following
picture of fixed points of $F$ (where $\twoheadrightarrow$ denotes quotient
coalgebras and $\rightarrowtail$ a subcoalgebra):

$\varphi F\twoheadrightarrow\varrho F\twoheadrightarrow\vartheta
F\rightarrowtail\nu F.$ (1.1)

We exhibit an example, where all four fixed points are different. However, if
$F$ is proper and preserves monomorphisms, then $\varphi F$, $\varrho F$ and
$\vartheta F$ are isomorphic and fully abstract, i.e. they collapse to a
subcoalgebra of the final one: $\varphi F\cong\varrho F\cong\vartheta
F\rightarrowtail\nu F$.

At this point, note that Urbat’s above mentioned recent work [41] also
provides a framework which covers the four above fixed points as four
instances of one theory. This provides, for example, a uniform proof of the
fact that they are fixed points and their universal properties (in the case of
$\varrho F$, $\vartheta F$ and $\varphi F$). However, Urbat’s paper does not
study the relationship between the four fixed points.

The rest of the paper is structured as follows: in Section 2 we collect some
technical preliminaries and recall the rational and locally finite fixed
points more in detail. Section 3 introduces the new fixed point $\varphi F$
and establishes the picture in (1.1). Next, Section 4 provides the
characterization of $\varphi F$ as the initial ffg-Bloom algebra for $F$.
Section 5 introduces proper functors and presents our main results, while in
Section 6 we present the proof of Theorem 22. Finally, Section 7 concludes the
paper.

This paper is a reworked full version of the conference paper [26]. We have
included detailed proofs, and in addition, we have added the new results in
Section 4.

#### Acknowledgments

I would like to thank Jiří Adámek, Henning Urbat and Joost Winter for helpful
discussions. I am also grateful to the anonymous reviewers whose constructive
comments have helped to improve the presentation of this paper.

##  2\. Preliminaries

In this section we recall a few preliminaries needed for the subsequent
development. We assume that readers are familiar with basic concepts of
category theory.

We denote the coproduct of two objects $X$ and $Y$ of a category $\mathscr{A}$
by $X+Y$ with injections $\mathsf{inl}:X\to X+Y$ and $\mathsf{inr}:Y\to X+Y$.

######  Remark 1.

Recall that a _strong epimorphism_ in a category $\mathscr{A}$ is an
epimorphism $e:A\twoheadrightarrow B$ of $\mathscr{A}$ that has the _unique
diagonal property_ w.r.t. any monomorphism. More precisely, whenever the
outside of the following square

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\scriptstyle{f}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\scriptstyle{d}$$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{D}$

commutes, where $m:C\rightarrowtail D$ is a monomorphism, then there exists a
unique morphism $d:B\to C$ with $d\cdot e=f$ and $m\cdot d=g$.

Similarly, a jointly epimorphic family $e_{i}:A_{i}\to B$, $i\in I$, is
_strong_ if it has the following similar unique diagonal property: for every
monomorphism $m:C\rightarrowtail D$ and morphisms $g:B\to D$ and
$f_{i}:A_{i}\to C$, $i\in I$, such that $m\cdot f_{i}=g\cdot e_{i}$ holds for
all $i\in I$, there exists a unique $d:C\to D$ such that $m\cdot d=g$ and
$d\cdot e_{i}=f_{i}$ for all $i\in I$.

On several occasions we will make use of the following fact.

######  Lemma 2.

Let $D:\mathscr{D}\to\mathscr{C}$ be a diagram with a colimit cocone
$\mathsf{in}_{d}:Dd\to C$. Then the colimit injections $\mathsf{in}_{d}$ form
a strongly epimorphic family.

######  Proof 2.1.

First, it is easy to see that the $\mathsf{in}_{d}$ form a jointly epimorphic
family. To see that it is strong, suppose we have a monomorphism
$m:M\rightarrowtail N$ and morphisms $g:C\to N$ and $f_{d}:Dd\to M$ for every
object $d$ in $\mathscr{D}$ such that $m\cdot f_{d}=g\cdot\mathsf{in}_{d}$.
Then the $f_{d}:Dd\to M$ form a cocone of $D$. Indeed, for every morphism
$h:d\to d^{\prime}$ of $\mathscr{D}$ we have

$m\cdot f_{d^{\prime}}\cdot Dh=g\cdot\mathsf{in}_{d^{\prime}}\cdot
Dh=g\cdot\mathsf{in}_{d}=m\cdot f_{d},$

which implies that $f_{d^{\prime}}\cdot Dh=f_{d}$ since $m$ is a monomorphism.
Therefore there exists a unique $i:C\to M$ such that
$f_{d}=i\cdot\mathsf{in}_{d}$ for every $d$ in $\mathscr{D}$. It follows that
also $m\cdot i=g$ since this equation holds when extended by every
$\mathsf{in}_{d}$; then use that the $\mathsf{in}_{d}$ form an epimorphic
family.

###  2.1. Algebras and Coalgebras

We also assume that readers are familiar with algebras and coalgebras for an
endofunctor. Given an endofunctor $F$ on some category $\mathscr{A}$ we write
$(\nu F,t)$ for the final $F$-coalgebra (if it exists). Recall, that the final
$F$-coalgebra exists under mild assumptions on $\mathscr{A}$ and $F$, e.g.
whenever $\mathscr{A}$ is locally presentable and $F$ an accessible functor
(see [8]). For any coalgebra $c:C\to FC$ we will write $\dagger c:C\to\nu F$
for the unique coalgebra morphism. We write

$\mathop{\mathsf{Coalg}}F$

for the category of $F$-coalgebras and their morphisms. Recall that all
colimits in $\mathop{\mathsf{Coalg}}F$ are formed on the level of
$\mathscr{A}$, i.e. the canonical forgetful functor
$\mathop{\mathsf{Coalg}}F\to\mathscr{A}$ creates all colimits (see e.g. [1,
Prop. 4.3]).

If $\mathscr{A}$ is a concrete category, i.e. equipped with a faithful functor
$|\cdot|:\mathscr{A}\to{\mathsf{Set}}$, one defines _behavioural equivalence_
as the following relation $\sim$: given two $F$-coalgebras $(X,c)$ and $(Y,d)$
then $x\sim y$ holds for $x\in|X|$ and $y\in|Y|$ if there is another
$F$-coalgebra $(Z,e)$ and $F$-coalgebra morphisms $f:X\to Z$ and $g:Y\to Z$
with $|f|(x)=|g|(y)$.

The base categories $\mathscr{A}$ of interest in this paper are the _algebraic
categories_ , i.e. categories of Eilenberg-Moore algebras (or $T$-algebras,
for short) for a finitary monad $T$ on ${\mathsf{Set}}$. Recall that, for a
monad $T$ on ${\mathsf{Set}}$ with unit $\eta$ and multiplication $\mu$, a
$T$-algebra is a pair $(A,\alpha)$ where $\alpha:TA\to A$, called the _algebra
structure_ , is a map such that the diagram below commutes:

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{A}}$$\textstyle{TA\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha}$$\textstyle{TTA\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu_{A}}$$\scriptstyle{T\alpha}$$\textstyle{A}$$\textstyle{TA\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha}$

Morphisms of $T$-algebras are just the usual morphisms of functor algebra,
i.e. a $T$-algebra morphism $h:(A,\alpha)\to(B,\beta)$ is a map $h:A\to B$
such that the square below commutes:

$\textstyle{TA\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha}$$\scriptstyle{Th}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\textstyle{TB\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\beta}$$\textstyle{B}$

The category of $T$-algebras and their morphisms is denoted by
${\mathsf{Set}}^{T}$ as usual. Equivalently, those categories are precisely
the finitary varieties, i.e. category of $\Sigma$-algebras for a signature
$\Sigma$, whose operation symbols have finite arity, satisfying a set of
equations (e.g. the categories of monoids, groups, vector spaces, or join-
semilattices).

We will frequently make use of the fact that $(TX,\mu_{X})$ is the _free_
$T$-algebra on the set $X$ (of generators). This means that for every
$T$-algebra $(A,\alpha)$ and every map $f:X\to A$ there exists a unique
extension of $f$ to a $T$-algebra morphisms, i.e., there exists a unique
$T$-algebra morphism ${f}^{\star}$ such that ${f}^{\star}\cdot\eta_{X}=f$:

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{X}}$$\scriptstyle{f}$$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{f}^{\star}}$$\textstyle{TTX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu_{X}}$$\scriptstyle{T{f}^{\star}}$$\textstyle{A}$$\textstyle{TA\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha}$

Moreover, it is easy to verify that ${f}^{\star}=\mu_{A}\cdot Tf$ holds.

A free $T$-algebra $(TX,\mu_{X})$ where $X$ is a finite set is called _free
finitely generated_.

In the following we will often drop algebra structures when we discuss a
$T$-algebra $(A,\alpha)$ and simply speak of the algebra $A$.

  1. (1)

The leading example in this paper are weighted automata considered as
coalgebras. Let $(\mathds{S},+,\cdot,0,1)$ be a semiring, i.e.
$(\mathds{S},+,0)$ is a commutative monoid, $(\mathds{S},\cdot,1)$ a monoid
and the usual distributive laws hold: $r\cdot 0=0=0\cdot r$,
$r\cdot(s+t)=r\cdot s+r\cdot t$ and $(r+s)\cdot t=r\cdot t+s\cdot t$. We just
write $\mathds{S}$ to denote a semiring. As base category $\mathscr{A}$ we
consider the category $\mathds{S}\textsf{-Mod}$ of $\mathds{S}$-semimodules;
recall that a (left) _$\mathds{S}$ -semimodule_ is a commutative monoid
$(M,+,0)$ together with an action $\mathds{S}\times M\to M$, written as
juxtaposition $sm$ for $r\in\mathds{S}$ and $m\in M$, such that for every
$r,s\in\mathds{S}$ and every $m,n\in M$ the following laws hold:

$\begin{array}[]{r@{\ }c@{\ }l@{\qquad}r@{\ }c@{\ }l@{\qquad}r@{\ }c@{\
}l}(r+s)m&=&rm+sm&0m&=&0&1m&=&m\\\ r(m+n)&=&rm+rn&r0&=&0&r(sm)&=&(r\cdot
s)m\end{array}$

An $\mathds{S}$-semimodule morphism is a monoid homomorphism $h\colon M_{1}\to
M_{2}$ such that $h(rm)=rh(m)$ for each $r\in\mathds{S}$ and $m\in M_{1}$.

An $\mathds{S}$-weighted automaton over the fixed input alphabet $\Sigma$ is a
triple $(i,(M^{a})_{a\in\Sigma},o)$, where $i$ and $o$ are a row and a column
vector in $\mathds{S}^{n}$, respectively, of input and output weights,
respectively, and $M_{a}$ is an $n\times n$-matrix over $\mathds{S}$, for some
natural number $n$. This number $n$ is the number of states of the weighted
automaton and the matrices $M^{a}$ represent $\mathds{S}$-weighted
transitions; in fact, $M^{a}_{i,j}$ is the weight of the $a$-transition from
state $i$ to state $j$ (with a weight of $0$ meaning that there is no
$a$-transition). Every weighted automaton accepts a _formal power series_ (or
_weighted language_) $L:\Sigma^{*}\to\mathds{S}$ defined in the following way:
$L(w)=i\cdot M^{w}\cdot o$ where $M^{w}$ is the obvious inductive extension of
$a\mapsto M^{a}$ to words in $\Sigma^{*}$: $M^{\varepsilon}$ is the identity
matrix and $M^{av}=M^{a}\cdot M^{v}$ for every $a\in\Sigma$ and
$v\in\Sigma^{*}$.

Now consider the functor $FX=\mathds{S}\times X^{\Sigma}$ on
$\mathds{S}\textsf{-Mod}$. Clearly, a weighted automaton (without its initial
vector) on $n$ states is equivalently an $F$-coalgebra on $\mathds{S}^{n}$; in
fact, to give a coalgebra structure
$\mathds{S}^{n}\to\mathds{S}\times(\mathds{S}^{n})^{\Sigma}$ amount to
specifying two $\mathds{S}$-semimodule morphisms
$o:\mathds{S}^{n}\to\mathds{S}$ (equivalently, a column vector over in
$\mathds{S}$) and $t:\mathds{S}^{n}\to(\mathds{S}^{n})^{\Sigma}$
(equivalently, an $\Sigma$-indexed family of $\mathds{S}$-semimodule morphisms
on $\mathds{S}^{n}$ each of which can be represented by an $n\times
n$-matrix).

The final $F$-coalgebra is carried by the set $\mathds{S}^{\Sigma^{*}}$ of all
weighted languages over $\Sigma$ with the obvious (coordinatewise)
$\mathds{S}$-semimodule structure and with the $F$-coalgebra structure given
by $\langle
o,t\rangle:\mathds{S}^{\Sigma^{*}}\to\mathds{S}\times(\mathds{S}^{\Sigma^{*}})^{\Sigma}$
with $o(L)=L(\varepsilon)$ and $t(L)(a)=\lambda w.L(aw)$; it is
straightforward to verify that $o$ and $t$ are $\mathds{S}$-semimodule
morphisms and form a final coalgebra. Moreover, for every $F$-coalgebra on
$\mathds{S}^{n}$ the unique coalgebra morphism
$\mathds{S}^{n}\to\mathds{S}^{\Sigma^{*}}$ assigns to every element $i$ of
$\mathds{S}^{n}$ (perceived as the row input vector of the weighted automaton
associated to the given coalgebra) the weighted language accepted by that
automaton.

  2. (2)

An important special case of $\mathds{S}$-weighted automata are ordinary non-
deterministic automata. One takes $\mathds{S}=\\{0,1\\}$ the Boolean semiring
for which the category of $\mathds{S}$-semimodules is (isomorphic to) the
category of join-semilattices. Then $FX=\\{0,1\\}\times X^{\Sigma}$ is the
coalgebraic type functor of deterministic automata with input alphabet
$\Sigma$, and there is a bijective correspondence between an $F$-coalgebra on
a free join-semilattice and non-deterministic automata. In fact in one
direction one restricts
$\mathcal{P}_{\mathsf{f}}X\to\\{0,1\\}\times(\mathcal{P}_{\mathsf{f}}X)^{\Sigma}$
to the set $X$ of generators, and in the other direction one performs the
well-known subset construction. The final coalgebra is carried by the set of
all formal languages on $\Sigma$ in this case.

  3. (3)

Another special case is where $\mathds{S}$ is a field. In this case,
$\mathds{S}$-semimodules are precisely the vector spaces over the field
$\mathds{S}$. Moreover, since every field is freely generated by its basis, it
follows that the $\mathds{S}$-weighted automata are precisely those
$F$-coalgebras whose carrier is a finite dimensional vector space over
$\mathds{S}$.

We will now recall a few properties of algebraic categories
${\mathsf{Set}}^{T}$, where $T$ is a finitary set monad, needed for our
proofs.

######  Remark 3.

  1. (1)

Recall that every strong epimorphism $e$ in ${\mathsf{Set}}^{T}$ is _regular_
, i.e. $e$ is the coequalizer of some pair of $T$-algebra morphisms. It
follows that the classes of strong and regular epimorphisms coincide, and
these are precisely the surjective $T$-algebra morphisms. Similarly, jointly
strongly epimorphic families of morphisms are precisely the jointly surjective
families. Finally, monomorphisms in ${\mathsf{Set}}^{T}$ are precisely the
injective $T$-algebra morphisms since the canonical forgetful functor
${\mathsf{Set}}^{T}\to{\mathsf{Set}}$ creates all limits (and pullbacks in
particular).

  2. (2)

Every free $T$-algebra $TX$ is _(regular) projective_ , i.e. given any
surjective $T$-algebra morphism $q:A\twoheadrightarrow B$ then for every
$T$-algebra morphism $h:TX\to B$ there exists a $T$-algebra morphism $g:TX\to
A$ such that $q\cdot g=h$:

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\scriptstyle{h}$$\textstyle{B}$

  3. (3)

Furthermore, note that every finitely presentable $T$-algebra $A$ is a regular
($=$ strong) quotient of a free $T$-algebra $TX$ with a finite set $X$ of
generators. Indeed, $A$ is presented by finitely many generators and
relations. So by taking $X$ as a finite set of generators of $A$, the unique
extension of the embedding $X\hookrightarrow A$ yields a surjective
$T$-algebra morphism $TX\twoheadrightarrow A$.

###  2.2. The Rational Fixed Point

As we mentioned in the introduction the canonical domain of behaviour of
‘finite’ coalgebras is the rational fixed point of an endofunctor. Its theory
can be developed for every finitary endofunctor on a locally finitely
presentable category. We will now recall the necessary background material.

A _filtered colimit_ is the colimit of a diagram $\mathscr{D}\to\mathscr{C}$
where $\mathscr{D}$ is a filtered category (i.e. every finite subcategory
$\mathscr{D}_{0}\hookrightarrow\mathscr{D}$ has a cocone in $\mathscr{D}$),
and a _directed colimit_ is a colimit whose diagram scheme $\mathscr{D}$ is a
directed poset. A functor is called _finitary_ if it preserves filtered
(equivalently directed) colimits. An object $C$ is called _finitely
presentable_ (fp) if the hom-functor $\mathscr{C}(C,-)$ preserves filtered
(equivalently directed) colimits, and _finitely generated_ (fg) if
$\mathscr{C}(C,-)$ preserves directed colimits of monos (i.e. colimits of
directed diagrams $D:\mathscr{D}\to\mathscr{C}$ where all connecting morphisms
$Df$ are monic in $\mathscr{C}$). Clearly, every fp object is fg, but the
converse fails in general. In addition, fg objects are closed under strong
epis (quotients), which fails for fp objects in general.

A cocomplete category $\mathscr{C}$ is called _locally finitely presentable_
(lfp) if there is a set of finitely presentable objects in $\mathscr{C}$ such
that every object of $\mathscr{C}$ is a filtered colimit of objects from that
set. We refer to [8] for further details.

Examples of lfp categories are the categories of sets, posets and graphs, with
finitely presentable objects precisely the finite sets, posets, and graphs,
respectively. The category of vector spaces over the field $k$ is lfp with
finite-dimensional spaces being the fp-objects. Every algebraic category is
lfp. The finitely generated objects are precisely the finitely generated
algebras (in the sense of general algebra), and finitely presentable objects
are precisely those algebras specified by finitely many generators and
finitely many relations.

Finitary functors abound. We just mention a few examples of finitary functors
on ${\mathsf{Set}}$.

Constant functors and the identity functor are, of course, finitary. For every
finitary signature $\Sigma$, i.e. $\Sigma=(\Sigma_{n})_{n<\omega}$ is a
sequence of sets with $\Sigma_{n}$ containing operation symbols of the finite
arity $n$, the associated polynomial functor given by

$F_{\Sigma}X=\coprod_{n<\omega}\Sigma_{n}\times X^{n}$

is finitary. The finite power-set functor given by
$\mathcal{P}_{\mathsf{f}}X=\\{Y\mid Y\subseteq X,\text{Y finite}\\}$ is
finitary (while the full power-set functor is not) and so is the bag functor
mapping a set $X$ to the set of finite multisets on $X$. The class of finitary
functors enjoys good closure properties: it is closed under composition,
finite products, arbitrary coproducts, and, in fact, arbitrary colimits. As we
have mentioned already, the finitary monads (i.e. whose functor part is
finitary) on ${\mathsf{Set}}$ are precisely those monads whose Eilenberg-Moore
category ${\mathsf{Set}}^{T}$ is (isomorphic to) a finitary variety of
algebras.

######  Assumptions 4.

For the rest of this section we assume that $F$ denotes a finitary endofunctor
on the lfp category $\mathscr{A}$.

######  Remark 5.

Recall that an lfp category, besides being cocomplete, is complete and has
(strong epi, mono)-factorizations of morphisms [8], i.e. every morphism
$f:X\to Y$ can be decomposed as $f=m\cdot e$ where $e:X\twoheadrightarrow I$
is a strong epi and $m:I\rightarrowtail Y$ a mono. One should think of $I$ as
the image of $X$ in $Y$ under $f$.

The rational fixed point is a fully abstract model of behaviour for all
$F$-coalgebras whose carrier is an fp-object. We now recall its construction
[5]. Denote by $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ the full subcategory
of all $F$-coalgebras on fp carriers, and let $(\varrho F,r)$ be the colimit
of the inclusion functor of $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ into
$\mathop{\mathsf{Coalg}}F$:

$(\varrho
F,r)=\mathop{\mathrm{colim}}(\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F\hookrightarrow\mathop{\mathsf{Coalg}}F)$

with the colimit injections ${a}^{\sharp}:A\to\varrho F$ for every coalgebra
$a:A\to FA$ in $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$.

We call $(\varrho F,r)$ the _rational fixed point_ of $F$; indeed, it is a
fixed point:

######  Proposition 6 ([5]).

The coalgebra structure $r:\varrho F\to F(\varrho F)$ is an isomorphism.

The rational fixed point can be characterized by a universal property both as
a coalgebra and as an algebra for $F$: as a coalgebra $\varrho F$ is the
_final locally finitely presentable coalgebra_ [25], and as an algebra it is
the _initial iterative algebra_ [5]. We will not recall the latter notion as
it is not needed for the technical development in this paper. Locally finitely
presentable (locally fp, for short) coalgebras for $F$ can be characterized as
precisely those $F$-coalgebra obtained as a filtered colimit of a diagram of
coalgebras from $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$:

######  Proposition 7 ([25], Corollary III.13).

An $F$-coalgebra is locally fp if and only if it is a colimit of some filtered
diagram
$\mathscr{D}\to\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F\hookrightarrow\mathop{\mathsf{Coalg}}F$.

For $\mathscr{A}={\mathsf{Set}}$ an $F$-coalgebra $(X,c)$ is locally fp iff it
is _locally finite_ , i.e. every element of $X$ is contained in a finite
subcoalgebra. Analogously, for $\mathscr{A}$ the category of vector spaces
over the field $k$ an $F$-coalgebra $(X,c)$ is locally fp iff it is _locally
finite dimensional_ , i.e. every element of $X$ is contained in a finite
dimensional subcoalgebra.

Of course, there is a unique coalgebra morphism $\varrho F\to\nu F$. Moreover,
in many cases $\varrho F$ is _fully abstract_ for locally fp coalgebras, i.e.
besides being the final locally fp coalgebra the above coalgebra morphism is
monic; more precisely, if the classes of fp- and fg-objects coincide and $F$
preserves non-empty monos, then $\varrho F$ is fully abstract (cf. Theorem 11
below). The assumption that the two object classes coincide is often true:

  1. (1)

In the category of sets, posets, and graphs, fg-objects are fp and those are
precisely the finite sets, posets, and graphs, respectively.

  2. (2)

A _locally finite variety_ is a variety of algebras, where every free algebra
on a finite set of generators is finite. It follows that fp- and fg-objects
coincide and are precisely the finite algebras. Concrete examples are the
categories of Boolean algebras, distributive lattices and join-semilattices.

  3. (3)

In the category of $\mathds{S}$-semimodules for a semiring $\mathds{S}$ the
fp- and fg-objects need not coincide in general. However, if the semiring
$\mathds{S}$ is _Noetherian_ in the sense of Ésik and Maletti [18], i.e. every
subsemimodule of a finitely generated $\mathds{S}$-semimodule is itself
finitely generated, then fg- and fp-semimodules coincide. Examples of
Noetherian semirings are: every finite semiring, every field, every principal
ideal domain such as the ring of integers and therefore every finitely
generated commutative ring by Hilbert’s Basis Theorem. The tropical semiring
$(\mathds{N}\cup\\{\infty\\},\min,+,\infty,0)$ is not Noetherian [17]. The
usual semiring of natural numbers is also not Noetherian: the
$\mathds{N}$-semimodule $\mathds{N}\times\mathds{N}$ is finitely generated but
its subsemimodule generated by the infinite set $\\{(n,n+1)\mid n\geq 1\\}$ is
not. However, $\mathds{N}$-semimodules are precisely the commutative monoids,
and for them fg- and fp-objects coincide (this is known as Redei’s theorem
[31]; see Freyd [20] for a very short proof).

  4. (4)

The category ${\mathsf{PCA}}$ of _positively convex algebras_ [14, 15] is the
Eilenberg-Moore category for the monad $\mathcal{D}$ of finitely supported
subprobability distributions on sets. This monad maps a set $X$ to

$\mathcal{D}X=\\{d:X\to[0,1]\mid\text{$\mathop{\mathsf{supp}}d$ is finite and
$\sum\limits_{x\in X}d(x)\leq 1$}\\},$

where $\mathop{\mathsf{supp}}d=\\{x\in X\mid d(x)\neq 0\\}$, and a function
$f:X\to Y$ to $\mathcal{D}f:\mathcal{D}X\to\mathcal{D}Y$ with

$\mathcal{D}f(d)=\lambda y.\sum\limits_{fx=y}d(x).$

More concretely, a positively convex algebra is a set $X$ equipped with finite
convex sum operations: for every $n$ and $p_{1},\ldots,p_{n}\in[0,1]$ with
$\sum\limits_{i=1}^{n}p_{i}\leq 1$ we have an $n$-ary operation assigning to
$x_{1},\ldots,x_{n}\in X$ an element $\bigboxplus\limits_{i=1}^{n}p_{i}x_{i}$
subject to the following axioms:

    1. (a)

$\bigboxplus\limits_{i=1}^{n}p_{i}^{k}x_{i}=x_{k}$ whenever $p_{k}^{k}=1$ and
$p_{i}^{k}=0$ for $i\neq k$, and

    2. (b)

$\bigboxplus\limits_{i=1}^{n}p_{i}\left(\bigboxplus\limits_{j=1}^{k}q_{i,j}x_{j}\right)=\bigboxplus\limits_{j=1}^{k}\left(\sum\limits_{i=1}^{n}p_{i}q_{i,j}\right)x_{j}$.

For $n=1$ we write the convex sum operation for $p\in[0,1]$ simply as $px$.
The morphisms of ${\mathsf{PCA}}$ are maps preserving finite convex sums in
the obvious sense.

The point of mentioning this example at length is that ${\mathsf{PCA}}$ is
used for the coalgebraic modelling of the trace semantics of probabilistic
systems (see e.g. [38]), and recently, it was established by Sokolova and
Woracek [39] that in ${\mathsf{PCA}}$, the classes of fp- and fg-objects
coincide. We shall come back to this example in Section 5 when we introduce
and discuss proper functors.

We list a number of examples of rational fixed points for cases where they do
form subcoalgebras of the final coalgebra.

  1. (1)

For the functor $FX=\\{0,1\\}\times X^{A}$ on ${\mathsf{Set}}$ the finite
coalgebras are deterministic automata, and the rational fixed point is carried
by the set of regular languages on the alphabet $A$.

  2. (2)

For every finitary signature $\Sigma$, the final coalgebra for the associated
polynomial functor $F_{\Sigma}$ (see Example 2.2) is carried by the set of all
(finite and infinite) $\Sigma$-trees, i.e. rooted and ordered trees where each
node with $n$-children is labelled by an $n$-ary operation symbol. The
rational fixed point is the subcoalgebra given by _rational_ (or _regular_
[13]) $\Sigma$-trees, i.e. those $\Sigma$-trees that have only finitely many
different subtrees (up to isomorphism) – this characterization is due to
Ginali [21]. For example, for the signature $\Sigma$ with a binary operation
symbol $*$ and a constant $c$ the following infinite $\Sigma$-tree (here
written as an infinite term) is rational:

$c*(c*(c*\cdots)));$

in fact, its only subtrees are the whole tree and the single node tree
labelled by $c$.

  3. (3)

For the functor $FX=\mathds{R}\times X$ on ${\mathsf{Set}}$ the final
coalgebra is carried by the set $\mathds{R}^{\omega}$ of real streams, and the
rational fixed point is carried by its subset of eventually periodic streams
(or lassos). Considered as a functor on the category of vector spaces over
$\mathds{R}$, the final coalgebra $\nu F$ remains the same, but the rational
fixed point $\varrho F$ consists of all rational streams [34].

  4. (4)

For the functor $FX=\mathds{S}\times X^{A}$ on the category
$\mathds{S}\textsf{-Mod}$ of $\mathds{S}$-semimodules for the semiring
$\mathds{S}$ we already mentioned that $\nu F=\mathds{S}^{A^{*}}$ consists of
all formal power-series. Whenever the classes of fg- and fp-semimodules
coincide, e.g. for every Noetherian semiring $\mathds{S}$ or the semiring of
natural numbers, then $\varrho F$ is formed by the _recognizable_ formal
power-series; from the Kleene-Schützenberger theorem [35] (see also [11]) it
follows that these are, equivalently, the _rational_ formal power-series.

  5. (5)

On the category of presheaves ${\mathsf{Set}}^{\mathcal{F}}$, where
$\mathcal{F}$ is the category of all finite sets and maps between them,
consider the functor $FX=V+X\times X+\delta(X)$, where
$V:\mathcal{F}\hookrightarrow{\mathsf{Set}}$ is the embedding and
$\delta(X)(n)=X(n+1)$. This is a paradigmatic example of a functor arising
from a _binding signature_ for which initial semantics was studied by Fiore et
al. [19].

The final coalgebra $\nu F$ is carried by the presheaf of all $\lambda$-trees
modulo $\alpha$-equivalence: $\nu F(n)$ is the set of (finite and infinite)
$\lambda$-trees in $n$ free variables (note that such a tree may have
infinitely many bound variables). And $\varrho F$ is carried by the rational
$\lambda$-trees, where an $\alpha$-equivalence class is called _rational_ if
it contains at least one $\lambda$-tree which has (up to isomorphism) only
finitely many different subtrees (see [7] for details). Rational
$\lambda$-trees also appear as the rational fixed point of a very similar
functor on the category of nominal sets [29]. An analogous characterization
can be given for every functor on nominal sets arising from a binding
signature [28].

As we mentioned previously, whether fg- and fp-objects coincide is currently
unknown in some base categories used in the coalgebraic modelling of systems,
for example, in idempotent semirings (used in the treatment of context-free
grammars [43]), in algebras for the stack monad (used for modelling
configurations of stack machines [22]); or it even fails, for example in the
category of finitary monads on sets (used in the categorical study of
algebraic trees [6]) or in Eilenberg-Moore categories for a monad in general
(the target categories of generalized determinization [36]).

As a remedy, in recent joint work with Pattinson and Wißmann [27], we have
introduced the _locally finite fixed point_ which provides a fully abstract
model of finitely generated behaviour. Its construction is very similar to
that of the rational fixed point but based on fg- in lieu of fp-objects. In
more detail, one considers the full subcategory
$\mathop{\mathsf{Coalg}_{\mathsf{fg}}}F$ of all $F$-coalgebras carried by an
fg-object and takes the colimit of its inclusion functor:

$(\vartheta
F,\ell)=\mathop{\mathrm{colim}}(\mathop{\mathsf{Coalg}_{\mathsf{fg}}}F\hookrightarrow\mathop{\mathsf{Coalg}}F).$

######  Theorem 8 ([27], Theorems 3.10 and 3.12).

Suppose that the finitary functor $F:\mathscr{A}\to\mathscr{A}$ preserves non-
empty monos. Then $(\vartheta F,\ell)$ is a fixed point for $F$, and it is a
subcoalgebra of $\nu F$.

######  Remark 9.

  1. (1)

Note that for an arbitrary (not necessarily concrete) lfp category
$\mathscr{A}$ the notion of a non-empty monomorphisms needs explanation: a
monomorphism $m:X\rightarrowtail Y$ is said to be _empty_ if its domain $X$ is
a strict initial object of $\mathscr{A}$, where recall that the initial object
$0$ of $\mathscr{A}$ is _strict_ provided that every morphism $A\to 0$ is an
isomorphism. In particular, if the initial object of $\mathscr{A}$ is not
strict, then all monomorphisms are non-empty.

  2. (2)

For a functor $F:\mathscr{A}\to\mathscr{A}$ preserving non-empty monos the
category $\mathop{\mathsf{Coalg}}F$ of all $F$-coalgebras inherits the (strong
epi, mono)-factorization system from $\mathscr{A}$ (see Remark 5) in the
following sense: every coalgebra morphism $f:(X,c)\to(Y,d)$ can be factorized
into coalgebra morphisms $e$ and $m$ carried by a strong epi and a mono in
$\mathscr{A}$, respectively. In fact, one (strong epi, mono)-factorizes
$f=m\cdot e$ in $\mathscr{A}$ and obtains a unique coalgebra structure on the
‘image’ $I$ such that $e$ and $m$ are coalgebra morphisms:

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c}$$\scriptstyle{e}$$\textstyle{FX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Fe}$$\textstyle{I\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{FI\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Fm}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{d}$$\textstyle{FY}$

Indeed, if $m$ is a non-empty mono, we know that $Fm$ is monic by assumption
and we use the unique diagonal property. Otherwise, $m$ is an empty mono,
which implies that $e:X\twoheadrightarrow I$ is an isomorphism since $I$ is a
strict initial object. Then $Fe\cdot c\cdot e^{-1}$ is the desired coalgebra
structure on $I$.

Furthermore, like its brother, the rational fixed point, $\vartheta F$ is
characterized by a universal property both as a coalgebra and as an algebra:
it is the final locally finitely generated coalgebra and the initial fg-
iterative algebra [27, Theorem 3.8 and Corollary 4.7].

Under additional assumptions, which all hold in every algebraic category, we
have a close relation between $\varrho F$ and $\vartheta F$; in fact, the
following is a consequence of [27, Theorem 5.4]:

######  Theorem 10.

Suppose that $\mathscr{A}$ is an lfp category such that every fp-object is a
strong quotient of a strong epi projective fp-object, and let
$F:\mathscr{A}\to\mathscr{A}$ be finitary and preserving non-empty monos. Then
$\vartheta F$ is the image of $\varrho F$ in the final coalgebra.

More precisely, taking the (strong epi, mono)-factorization of the unique
$F$-coalgebra morphism $\varrho F\to\nu F$ yields $\vartheta F$, i.e. for $F$
preserving monos on an algebraic category we have the following picture:

$\varrho F\twoheadrightarrow\vartheta F\rightarrowtail\nu F.$

A sufficient condition under which $\varrho F$ and $\vartheta F$ coincide is
the following (cf. [27, Section 5]):

######  Theorem 11.

Suppose that in addition to the assumption in Theorem 10 the classes of fg-
and fp-objects coincide in $\mathscr{A}$. Then $\varrho F\cong\vartheta F$,
i.e. the left-hand morphism above is an isomorphism.

In the introduction we briefly mentioned a number of interesting instances of
$\vartheta F$ that are not (known to be) instances of the rational fixed
point; see [27] for details. A concrete example, where $\varrho F$ is not a
subcoalgebra of $\nu F$ (and hence not isomorphic to $\vartheta F$) was given
in [12, Example 3.15]. We present a new, simpler example based on similar
ideas:

  1. (1)

Let $\mathscr{A}$ be the category of algebras for the signature $\Sigma$ with
two unary operation symbols $u$ and $v$. The natural numbers $\mathds{N}$ with
the successor function as both operations $u^{\mathds{N}}$ and
$v^{\mathds{N}}$ form an object of $\mathscr{A}$. We consider the functor
$FX=\mathds{N}\times X$ on $\mathscr{A}$. Coalgebras for $F$ are automata
carried by an algebra $A$ in $\mathscr{A}$ equipped with two $\Sigma$-algebra
morphisms: an output morphism $A\to\mathds{N}$ and a next state morphism $A\to
A$. The final coalgebra is carried by the set $\mathds{N}^{\omega}$ of streams
of natural numbers with the coordinatewise algebra operations and with the
coalgebra structure given by the usual head and tail functions.

Note that the free $\Sigma$-algebra on a set $X$ of generators is
$TX\cong\\{u,v\\}^{*}\times X$; we denote its elements by $w(x)$ for
$w\in\\{u,v\\}^{*}$ and $x\in X$. The operations are given by prefixing words
by the letters $u$ and $v$, respectively: $s^{TX}:w(x)\mapsto sw(x)$ for $s=u$
or $v$.

Now one considers the $F$-coalgebra $a:A\to FA$, where $A=T\\{x\\}$ is free
$\Sigma$-algebra on one generator $x$ and $a$ is determined by
$a(x)=(0,u(x))$. Recall our notation $\dagger a:A\to\nu F$ for the unique
coalgebra morphism. Clearly, $\dagger a(x)$ is the stream $(0,1,2,3,\cdots)$
of all natural numbers, and since $\dagger a$ is a $\Sigma$-algebra morphism
we have

$\dagger a(u(x))=\dagger a(v(x))=(1,2,3,4,\cdots).$

Since $A$ is (free) finitely generated, it is of course, finitely presentable
as well. Thus, $(A,a)$ is a coalgebra in
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$. However, we shall now prove that the
(unique) $F$-coalgebra morphism ${a}^{\sharp}:A\to\varrho F$ maps $u(x)$ and
$v(x)$ to two distinct elements of $\varrho F$.

We prove this by contradiction. So suppose that
${a}^{\sharp}(u(x))={a}^{\sharp}(v(x))$. By the construction of $\varrho F$ as
a filtered colimit (see Notation 2.2) we know that there exists a coalgebra
$b:B\to FB$ in $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ and an $F$-coalgebra
morphism $h:A\to B$ with

$h(u(x))=h(v(x)).$ (2.1)

Since $B$ is a finitely presented $\Sigma$-algebra it is the quotient in
$\mathscr{A}$ of a free algebra $A^{\prime}$ via some surjective
$\Sigma$-algebra morphism $q:A^{\prime}\twoheadrightarrow B$, say. Next
observe, that there is a coalgebra structure $a^{\prime}:A^{\prime}\to
FA^{\prime}$ such that $q$ is an $F$-coalgebra morphism from
$(A^{\prime},a^{\prime})$ to $(B,b)$: for $Fq$ is a surjective
$\Sigma$-algebra morphism and so we obtain $q^{\prime}$ by using projectivity
of $A^{\prime}$ w.r.t. $b\cdot q:A^{\prime}\to FB$ (cf. Remark 3(2)):

$\textstyle{A^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a^{\prime}}$$\scriptstyle{q}$$\textstyle{FA^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Fq}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{b}$$\textstyle{FB}$

Now choose a term $t_{x}$ in $A^{\prime}$ with $q(t_{x})=h(x)$. Using that $q$
and $h$ are $\Sigma$-algebra morphisms we see that $q(u(t_{x}))=q(v(t_{x}))$
as follows:

$q(u(t_{x}))=u^{B}(q(t_{x}))=u^{B}(h(x))=h(u(x))=v^{B}(h(x))=v^{B}(q(t_{x}))=q(v(t_{x})).$
(2.2)

Since $h$ is an $F$-coalgebra morphism, we obtain from (2.1) that $h$ merges
the right-hand components of $a(u(x))$ and $a(v(x))$, in symbols:
$h(uu(x))=h(vu(x))$. It follows that $q$ satisfies $q(uu(t_{x}))=q(vu(t_{x}))$
using a similar argument as in (2.2) above.

Continuing to use that $h$ and $q$ are $F$-coalgebra morphisms, we obtain the
following infinite list of elements (terms) of $A^{\prime}$ that are merged by
$q$ (we write these pairs as equations):

$q(u^{n+1}(t_{x}))=q(vu^{n}(t_{x}))\qquad\text{for $n\in\mathds{N}$.}$ (2.3)

We need to prove that there exists no finite set of relations $E\subseteq
A^{\prime}\times A^{\prime}$ generating the above congruence on $A^{\prime}$
given by $q:A^{\prime}\twoheadrightarrow B$. So suppose the contrary, and let
$A_{0}^{\prime}$ be the $\Sigma$-subalgebra of $A^{\prime}$ generated by
$\\{t_{x}\\}$, i.e. $A_{0}^{\prime}\cong\\{u,v\\}^{*}\times\\{t_{x}\\}$. Since
$q(t_{x})=h(x)$ and $q$ and $h$ are both coalgebra morphisms we know that
$\dagger a^{\prime}=\dagger b\cdot q$ and $\dagger b\cdot h=\dagger a$ and
therefore

$\dagger a^{\prime}(t_{x})=\dagger b(q(t_{x}))=\dagger b(h(x))=\dagger
a(x)=(0,1,2,3,\cdots).$

Since $\dagger a^{\prime}$ is a $\Sigma$-algebra morphism it follows that for
a word $w\in\\{u,v\\}^{*}$ of length $n$ we have

$\dagger a^{\prime}(w(t_{x}))=(n,n+1,n+2,n+3,\cdots).$ (2.4)

Thus, when $w,w^{\prime}\in\\{u,v\\}^{*}$ are of different length, then the
pair $(w(t_{x}),w^{\prime}(t_{x}))$ cannot be in the congruence generated by
$E$; otherwise we would have $q(w(t_{x}))=q(w^{\prime}(t_{x}))$ which implies
$\dagger a^{\prime}(w(t_{x}))=\dagger a^{\prime}(w^{\prime}(t_{x}))$
contradicting (2.2).

Now let $\ell$ be the maximum length of words from $\\{u,v\\}^{*}$ occurring
in any pair contained in the finite set $E$. Then the pair
$(u^{\ell+2}(t_{x}),vu^{\ell+1}(t_{x}))$ obtained from the $\ell+1$-st
equation in (2.3) is not in the congruence generated by $E$; for if any pair
of terms of height greater then $\ell$ are related by that congruence, these
two terms must have the same head symbol. Thus we arrive at a contradiction as
desired.

  2. (2)

In this example we also have that $\vartheta F$ and $\nu F$ do not coincide.
To see this we use that $\vartheta F$ is the union of images of all $\dagger
c:TX\to\nu F$ where $(TX,c)$ ranges over those $F$-coalgebras whose carrier
$TX$ is free finitely generated (i.e. $TX\cong\\{u,v\\}^{*}\times X$ for some
finite set $X$) [27, Theorem 6.5]. Hence, each such algebra $TX$ is countable,
and there exist only countably many of them, up to isomorphism. Furthermore,
note that on every free finitely generated algebra $TX$ there exist only
countably many coalgebra structures $c:TX\to FTX$, since $FTX=\mathds{N}\times
TX$ is countable and $c$, being a $\Sigma$-algebra morphism, is determined by
its action on the finitely many generators. Thus, $\vartheta F$ is countable
because it is the above union of countably many countable coalgebras. However,
$\nu F$ being carried by the set $\mathds{N}^{\omega}$ of all streams over
$\mathds{N}$ is uncountable.

##  3\. A Fixed Point Based on Coalgebras Carried by Free Algebras

In this section we study coalgebras for a functor $F$ on an algebraic category
${\mathsf{Set}}^{T}$ whose carrier is a free finitely generated algebra. These
coalgebras are of interest because they are precisely those coalgebras arising
as the results of the generalized determinization [36].

We shall see that their colimit yields yet another fixed point of $F$ (besides
the rational fixed point and the locally finite one). Moreover, in the next
section we show that this fixed point is characterized by a universal property
as an algebra.

######  Assumptions 12.

Throughout the rest of the paper we assume that $\mathscr{A}$ is an _algebraic
category_ , i.e. $\mathscr{A}$ is (equivalent to) the Eilenberg-Moore category
${\mathsf{Set}}^{T}$ for a finitary monad $T$ on ${\mathsf{Set}}$.
Furthermore, we assume that $F:\mathscr{A}\to\mathscr{A}$ is a finitary
endofunctor preserving surjective $T$-algebra morphisms.

######  Remark 13.

  1. (1)

Note that we do not assume here that $F$ preserves non-empty monomorphisms
(cf. Theorems 8 and 10) as this assumption is not needed for our main result
Theorem 22. However, we will make this assumption at the end, in order to
obtain the picture in (1.1) (see Corollary 24).

  2. (2)

The most common instance of a functor $F$ on an algebraic category
$\mathscr{A}$ is a lifting of an endofunctor
$F_{0}:{\mathsf{Set}}\to{\mathsf{Set}}$, i.e. we have a commutative square

$\textstyle{{\mathsf{Set}}^{T}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F}$$\scriptstyle{U}$$\textstyle{{\mathsf{Set}}^{T}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{U}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F_{0}}$$\textstyle{\mathsf{Set}}$

where $U:\mathscr{A}\to{\mathsf{Set}}$ is the forgetful functor. Recall that
monomorphisms in ${\mathsf{Set}}^{T}$ are precisely the injective $T$-algebra
morphisms (see Remark 3(1)). Hence, a lifting $F$ preserves all non-empty
monos since the lifted set functor $F_{0}$ does so. Similarly, $F$ preserves
surjective $T$-algebra morphisms since $F_{0}$ preserves surjections (which
are split epis in ${\mathsf{Set}}$). Finally, $F$ is finitary whenever $F_{0}$
is so because filtered colimits in ${\mathsf{Set}}^{T}$ are created by $U$.

  3. (3)

It is well known that liftings $F:{\mathsf{Set}}^{T}\to{\mathsf{Set}}^{T}$ are
in bijective correspondence with distributive laws of the monad $T$ over the
functor $F_{0}$, i.e. natural transformations $\lambda:TF_{0}\to F_{0}T$
satisfying two obvious axioms w.r.t. the unit and multiplication of $T$ (see
e.g. Johnstone [24]):

$\textstyle{F_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F_{0}\eta}$$\scriptstyle{\eta
F_{0}}$$\textstyle{TF_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\lambda}$$\textstyle{F_{0}T}$
$\textstyle{TTF_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T\lambda}$$\scriptstyle{\mu
F_{0}}$$\textstyle{TF_{0}T\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\lambda
T}$$\textstyle{F_{0}TT\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F_{0}\mu}$$\textstyle{TF_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\lambda}$$\textstyle{F_{0}T}$

Moreover, coalgebras for the lifting $F$ are precisely the _$\lambda$
-bialgebras_, i.e. sets $X$ equipped with an Eilenberg-Moore algebra structure
$\alpha:TX\to X$ and a coalgebra structure $c:X\to F_{0}X$ subject to the
following commutativity condition

$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha}$$\scriptstyle{Tc}$$\textstyle{TF_{0}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\lambda_{X}}$$\textstyle{F_{0}TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F_{0}\alpha}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c}$$\textstyle{F_{0}X}$

which states that $c$ is a $T$-algebra morphism from $(X,\alpha)$ to
$F(X,\alpha)$.

  4. (4)

Let $F_{0}:{\mathsf{Set}}\to{\mathsf{Set}}$ have a lifting to
${\mathsf{Set}}^{T}$. _Generalized determinization_ [36] is the process of
turning a given coalgebra $c:X\to F_{0}TX$ in ${\mathsf{Set}}$ into the
coalgebra ${c}^{\star}:TX\to FTX$ in ${\mathsf{Set}}^{T}$. For example, for
the functor $F_{0}X=\\{0,1\\}\times X^{\Sigma}$ on ${\mathsf{Set}}$ and the
finite power-set monad $T=\mathcal{P}_{\mathsf{f}}$, $F_{0}T$-coalgebras are
precisely non-deterministic automata and generalized determinization is the
construction of a deterministic automaton by the well-known subset
construction. The unique $F$-coalgebra morphism $\dagger({c}^{\star})$ assigns
to each state $x\in X$ the language accepted by $x$ in the given non-
deterministic automaton (whereas the final semantics for $F_{0}T$ on
${\mathsf{Set}}$ provides a kind of process semantics taking the non-
deterministic branching into account).

Thus studying the behaviour of $F$-coalgebras whose carrier is a free finitely
generated $T$-algebra $TX$ is precisely the study of a _coalgebraic language
semantics_ of finite $F_{0}T$-coalgebras.

We denote by

$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$

the full subcategory of $\mathop{\mathsf{Coalg}}F$ given by all coalgebras
$c:TX\to FTX$ whose carrier is a free finitely generated $T$-algebra, i.e.
where $X$ is a finite set $X$.

The colimit of the inclusion functor of
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ into the category of all
$F$-coalgebras is denoted by

$(\varphi
F,\zeta)=\mathop{\mathrm{colim}}(\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F\hookrightarrow\mathop{\mathsf{Coalg}}F)$

with the colimit injections $\mathsf{in}_{c}:TX\to\varphi F$ for every
$c:TX\to FTX$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$.

Since every free finitely generated algebra $TX$ is clearly fp (being
presented by the finite set $X$ of generators and no relations),
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ is a full subcategory of
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$. Therefore, the universal property of
the colimit $\varphi F$ induces a coalgebra morphism denoted by $h:\varphi
F\to\varrho F$. Furthermore we write $m:\varphi F\to\nu F$ for the unique
$F$-coalgebra morphisms into the final coalgebra, respectively. We shall show
in Proposition 17 that $h$ is a strong epimorphism. Thus, whenever $F$
preserves non-empty monos, we have the picture (1.1) from the introduction.

######  Remark 14.

We will also use that the colimit $\varphi F$ is a sifted colimit.

  1. (1)

Recall that a small category $\mathscr{D}$ is called _sifted_ [9] if finite
products commute with colimits over $\mathscr{D}$ in ${\mathsf{Set}}$. More
precisely, $\mathscr{D}$ is sifted iff given any diagram
$D:\mathscr{D}\times\mathscr{J}\to{\mathsf{Set}}$, where $\mathscr{J}$ is a
finite discrete category, the canonical map

$\mathop{\mathrm{colim}}\limits_{d\in\mathscr{D}}\Big{(}\prod\limits_{j\in\mathscr{J}}D(d,j)\Big{)}\to\prod\limits_{j\in\mathscr{J}}(\mathop{\mathrm{colim}}\limits_{d\in\mathscr{D}}D(d,j))$

is an isomorphism. A _sifted colimit_ is a colimit of a diagram with a sifted
diagram scheme.

  2. (2)

It is well-known that the forgetful functor
${\mathsf{Set}}^{T}\to{\mathsf{Set}}$ preserves and reflects sifted colimits;
this follows from [9, Corollary 11.9].

  3. (3)

Further recall [9, Example 2.16] that every small category $\mathscr{D}$ with
finite coproducts is sifted. Thus, from Lemma 15 below it follows that
$\mathscr{D}=\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ is sifted, and therefore
$\varphi F$ is a sifted colimit.

######  Lemma 15.

The category $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ is closed under finite
coproducts in $\mathop{\mathsf{Coalg}}F$.

######  Proof 3.1.

The empty map $0\to FT0$ extends uniquely to a $T$-algebra morphism $T0\to
FT0$, i.e. an $F$-coalgebra, and this coalgebra is the initial object of
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$.

Given coalgebras $c:TX\to FTX$ and $d:TY\to FTY$ one uses that $T(X+Y)$
together with the injections $T\mathsf{inl}:TX\to T(X+Y)$ and
$T\mathsf{inr}:TY\to T(X+Y)$ form a coproduct in ${\mathsf{Set}}^{T}$. This
implies that forming the coproduct of $(TX,c)$ and $(TY,d)$ in
$\mathop{\mathsf{Coalg}}F$ we obtain an $F$-coalgebra on $T(X+Y)$, and this is
an object of $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ since $X+Y$ is finite.

######  Theorem 16 (Urbat [41], Lemma 4.5).

If $F$ preserves sifted colimits, then $\varphi F$ is a fixed point of $F$,
i.e. $\zeta:\varphi F\to F(\varphi F)$ is an isomorphism.

Recall that every finitary endofunctor on ${\mathsf{Set}}$ preserves sifted
colimits (this follows from [9, Corollary 6.30]). Thus, so does every lifting
$F:{\mathsf{Set}}^{T}\to{\mathsf{Set}}^{T}$ of a finitary endofunctor on
${\mathsf{Set}}$, using Remark 14(2). In general, finitary functors need not
preserve sifted colimits [9, Example 7.11].

One might now expect that $\varphi F$ is characterized as a coalgebra by a
universal property similar to finality properties that characterize $\varrho
F$ and $\vartheta F$. However, Urbat [41] shows that this is not the case. In
fact, he provides the following example of a coalgebra $c:TX\to FTX$ where
$\mathsf{in}_{c}:TX\to\varphi F$ is not the only $F$-coalgebra morphism:

  1. (1)

Let $\mathscr{A}$ be the category of algebras for the signature with one unary
operation symbol $u$ (and no equations), and let $F=\mathsf{Id}$ be the
identity functor on $\mathscr{A}$. Let $A$ be the free (term) algebra on one
generator $x$, and let $B$ be the free algebra on one generator $y$ (i.e. both
$A$ and $B$ are isomorphic to $\mathds{N}$). We equip $A$ and $B$ with the
$F$-coalgebra structures $a=\mathsf{id}:A\to A$ and $b:B\to B$ given by
$b(y)=u(y)$. Then the mapping $t\mapsto u(t)$ clearly is an $F$-coalgebra
morphism from $B$ to itself, i.e. a morphism in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$. Therefore we have
$\mathsf{in}_{b}(y)=\mathsf{in}_{b}(u(y))$.

Now define a morphism $g:A\to\varphi F$ in $\mathscr{A}$ by
$g(x)=\mathsf{in}_{b}(y)$. Then $g$ is an $F$-coalgebra morphism since

$g\cdot
a(x)=g(x)=\mathsf{in}_{b}(y)=\mathsf{in}_{b}(u(y))=\mathsf{in}_{b}(b(y))=\zeta(\mathsf{in}_{b}(y))=\zeta(g(x)),$

where $\zeta:\varphi F\to F(\varphi F)$ is the coalgebra structure on $\varphi
F$.

We prove the following property: for every morphism $f$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ from $\alpha:TX\to TX$ to
$\beta:TY\to TY$, any $t\in TX$ reaches finitely many states iff $f(t)$ does
so, more precisely:

$\\{\alpha^{n}(t)\mid n\in\mathds{N}\\}\text{ is
finite}\qquad\iff\qquad\\{\beta^{n}(f(t))\mid n\in\mathds{N}\\}\text{ is
finite}.$

Indeed, if $t$ reaches finitely many states, then the $f(\alpha^{n}(t))$, for
$n\in\mathds{N}$, form a finite set, and $\beta^{n}(f(t))$, $n\in\mathds{N}$
is the same set since $f$ is a coalgebra morphism.

Conversely, suppose that $t$ reaches infinitely many states. Since $f$ is a
morphism in $\mathscr{A}$, we know that if $\alpha^{n}(t)$ is $u^{k}(x)$ for
some $x\in X$ then $f(\alpha^{n}(t))=\beta^{n}(f(t))$ must be $u^{l}(y)$ with
$l\geq k$ for some $y\in Y$. Thus, $f(t)$ must also reach infinitely many
states.

We can now conclude that $g,\mathsf{in}_{a}:A\to\varphi F$ are different
coalgebra morphisms. Indeed, $\mathsf{in}_{a}(x)$ reaches only itself since
$x$ does so, but $g(x)=\mathsf{in}_{b}(y)$ reaches infinitely many states
since $y$ does so. Thus, $g(x)\neq\mathsf{in}_{a}(x)$.

It follows that $|\varphi F|\geq 2$, while $\varrho F=\vartheta F=\nu F=1$; to
see the latter equation use that $\mathsf{id}:1\to 1$ is a coalgebra in
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ since $1$ is the object of
$\mathscr{A}$ presented by one generator $z$ and one relation $z=u(z)$.

  2. (2)

Using similar ideas as in the previous point one can show that, for the
category $\mathscr{A}$ and $FX=\mathds{N}\times X$ from Example 2.2, $\varphi
F$ and $\varrho F$ do not coincide. Consequently, in this example, none of the
arrows in (1.1) is an isomorphism.

In order to see that $\varphi F$ and $\varrho F$ do not coincide, consider the
two coalgebras $a:A\to FA$ and $b:B\to FB$ with $A=T\\{x\\}$ and $B=T\\{y\\}$
and with the coalgebra structure given by $a(x)=(0,u(x))$ and $b(y)=(0,v(y))$.
These coalgebras both lie in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$.
Consider also the coalgebra $p:P\to FP$ where $P$ is presented by one
generator $z$ and one relation $u(z)=v(z)$, i.e. $P=T\\{z\\}/\mathord{\sim}$,
where $\sim$ is the smallest congruence with $u(z)\sim v(z)$. Hence, $w(z)\sim
w^{\prime}(z)$ for $w,w^{\prime}\in\\{u,v\\}^{*}$ iff $w$ and $w^{\prime}$
have the same length. The coalgebra structure is defined by
$p([w(x)])=(0,[uw(x)])$. The coalgebra $(P,p)$ lies in
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$. Now $f:A\to P$ and $g:B\to P$
determined by $f(x)=z=g(y)$ are easily seen to be $F$-coalgebra morphisms, and
therefore ${a}^{\sharp}={p}^{\sharp}\cdot f$ and
${b}^{\sharp}={p}^{\sharp}\cdot g$. Therefore

${a}^{\sharp}(x)={p}^{\sharp}(f(x))={p}^{\sharp}(z)={p}^{\sharp}(g(y))={b}^{\sharp}(y).$

However, we will prove that $\mathsf{in}_{a}(x)\neq\mathsf{in}_{b}(x)$. For
any $(TX,c)$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ and $t\in TX$, we
say that _$t$ -reachable states are $u$-bounded_ if there exists a natural
number $k$ such that, for any state $s=w(x)$ reachable from $t$ via the next
state function, the number $|w|_{u}$ of $u$’s in $w$ is at most $k$. Now we
prove for any morphism $f:(TX,c)\to(TY,d)$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ and any $t\in TX$ the following
claim:

$t$-reachable states are $u$-bounded iff $f(t)$-reachable states are
$u$-bounded.

Indeed, a state $s=w(x)$ is reachable from $t$ iff $f(s)=wf(x)$ is reachable
from $f(t)$. Then the ’only if’ direction is clear: if $t$-reachable states
are not $u$-bounded, then neither are $f(t)$-reachable states. For the ’if’
direction suppose $t$-reachable states are $u$-bounded by $k$. Then
$f(t)$-reachable states are bounded by $k+\max\\{|f(x)|_{u}\mid x\in X\\}$.

Coming back to the discussion of properties that $\varphi F$ does have, the
following proposition shows that $\varrho F$ is always a strong quotient of
$\varphi F$. Recall from Notation 3 the canonical coalgebra morphism $h$ from
$\varphi F$ to $\varrho F$:

######  Proposition 17.

The morphism $h:\varphi F\twoheadrightarrow\varrho F$ is a strong epimorphism
in $\mathscr{A}$.

The following proof is set theoretic and makes explicit use of the fact that
$\mathscr{A}$ is algebraic over ${\mathsf{Set}}$, i.e. we use that strong
epimorphisms in $\mathscr{A}$ are precisely surjective $T$-algebra morphisms.
In the appendix we provide a purely category theoretic proof, which is
somewhat longer, however. That proof shows that the above result holds for
more general base categories than sets.

######  Proof 3.2.

We first prove the following fact:

every coalgebra in $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ is a regular
quotient of some coalgebra in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$.

Indeed, given any $a:A\to FA$ in $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ we
know that its carrier is a regular quotient of some free $T$-algebra $TX$ with
$X$ finite, via $q:TX\twoheadrightarrow A$, say (see Remark 3.3). Since $F$
preserves regular epis ($=$ surjections) we can use projectivity of $TX$ (see
Remark 3.2) to obtain a coalgebra structure $c$ on $TX$ making $q$ an
$F$-coalgebra morphism:

$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c}$$\scriptstyle{q}$$\textstyle{FTX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Fq}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\textstyle{FA}$

This implies that we have ${c}^{\sharp}={a}^{\sharp}\cdot q$.

Now let $p\in\varrho F$. Since $\varrho F$ is the colimit of all coalgebras in
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$, we know from Lemma 2 that there
exists some coalgebra $a:A\to FA$ in $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$
and $r\in A$ such that ${a}^{\sharp}(r)=p$. By the above fact, we have
$(TX,c)$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ and the surjective
coalgebra morphism $q:TX\twoheadrightarrow A$. Hence there exists some $s\in
TX$ with $q(s)=r$. By the finality of $\varrho F$ we have the commuting square
below:

$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\scriptstyle{\mathsf{in}_{c}}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{a}^{\sharp}}$$\textstyle{\varphi
F\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\textstyle{\varrho
F}$

Thus we have $p={a}^{\sharp}(q(s))=h(\mathsf{in}_{c}(s))$, which shows that
$h$ is surjective as desired.

######  Corollary 18.

If $F$ preserves non-empty monomorphisms, then we obtain the situation
displayed in (1.1):

$\varphi F\twoheadrightarrow\varrho F\twoheadrightarrow\vartheta
F\rightarrowtail\nu F.$

Indeed, this follows from Proposition 17 and Theorem 10.

##  4\. A Universal Property of $\varphi F$

We have seen in Example 3(1) that $\varphi F$, unlike $\varrho F$ and
$\vartheta F$, does not enjoy a finality property as a coalgebra. In this
section we will prove that, as an algebra for $F$, $\varphi F$ is
characterized by a universal property. This property then determines $\varphi
F$ uniquely up to isomorphism. To this end we make the In addition to
Assumptions 12 we assume in this section that $F$ preserves sifted colimits
(cf. Remark 14). By Theorem 16, we know that $\varphi F$ is then a fixed point
of $F$ so that by inverting its coalgebra structure we may regard it as the
$F$-algebra $\zeta^{-1}:F(\varphi F)\to\varphi F$.

We have already mentioned that both $\varrho F$ and $\vartheta F$ are
characterized by universal properties as $F$-algebras: they are the initial
iterative and initial fg-iterative algebras, respectively. However, those
properties entail that there exists a unique $F$-coalgebra morphism from every
coalgebra in $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ to $\varrho F$, and from
every coalgebra in $\mathop{\mathsf{Coalg}_{\mathsf{fg}}}F$ to $\vartheta F$,
respectively. That means that simply adjusting the definition of the notion of
iterative algebra does not yield the desired universal property of $\varphi
F$, again due to Example 3(1).

The key to establishing a universal property of $\varphi F$ is to consider
algebras which admit canonical (rather than unique) coalgebra-to-algebra
homomorphisms. The following notion is inspired by the Bloom algebras
introduced by Adámek et al. [2]. An _ffg-Bloom algebra_ for the functor $F$ is
a triple $(A,a,\dagger)$ where $a:FA\to A$ is an $F$-algebra and $\dagger$ is
an operation

$\frac{TX\xrightarrow{c}FTX,\text{$X$
finite}}{TX\xrightarrow{{c}^{\dagger}}A}$

subject to the following axioms:

  1. (1)

solution: ${c}^{\dagger}$ is a coalgebra-to-algebra morphism, i.e. the diagram
below commutes:

$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{c}^{\dagger}}$$\scriptstyle{c}$$\textstyle{A}$$\textstyle{FTX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F{c}^{\dagger}}$$\textstyle{FA\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$

  2. (2)

functoriality: for every coalgebra morphism $m:(TX,c)\to(TY,d)$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ we have
${c}^{\dagger}={d}^{\dagger}\cdot m$:

$\vbox{ \lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
12.14609pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
20.59126pt\raise 4.50694pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{c}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 35.15103pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{m}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-27.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
35.15103pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{FTX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
50.21179pt\raise-18.41666pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.39166pt\hbox{$\scriptstyle{Fm}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 50.21179pt\raise-27.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{TY\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
20.1375pt\raise-42.26385pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\hbox{$\scriptstyle{d}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
39.28818pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
39.28818pt\raise-36.83331pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{FY}$}}}}}}}\ignorespaces}}}}\ignorespaces}\qquad\implies\qquad\vbox{
\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
12.14609pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
17.93481pt\raise-4.20245pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.20139pt\hbox{$\scriptstyle{{c}^{\dagger}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
35.15103pt\raise-15.80768pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{m}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-27.83331pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern
35.15103pt\raise-18.83331pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{A}$}}}}}}}{\hbox{\kern-10.63022pt\raise-37.66663pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{TY\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
19.78343pt\raise-33.48732pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-3.125pt\hbox{$\scriptstyle{{d}^{\dagger}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
35.2272pt\raise-21.83331pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces}}}}\ignorespaces}$

A _morphism of ffg-Bloom algebras_ from $(A,a,\dagger)$ to $(B,b,\ddagger)$ is
an $F$-algebra morphism preserving solutions, i.e. an $F$-algebra morphism
$h:(A,a)\to(B,b)$ such that for every $c:TX\to FTX$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ we have

$c^{\ddagger}=(TX\xrightarrow{{c}^{\dagger}}A\xrightarrow{h}B).$

The algebra $\zeta^{-1}:F(\varphi F)\to\varphi F$ together with the operation
$\ddagger$ given by the colimit injections, i.e.
$c^{\ddagger}=\mathsf{in}_{c}:TX\to\varphi F$ for every $c:TX\to FTX$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$, clearly is an ffg-Bloom algebra.
Indeed, the solution axiom holds since $\mathsf{in}_{c}$ is a coalgebra
morphisms from $(TX,c)$ to $(\varphi F,\zeta)$ and functoriality holds since
the $\mathsf{in}_{c}$ form a compatible cocone of the diagram
$D:\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F\hookrightarrow\mathop{\mathsf{Coalg}}F$.

######  Theorem 19.

The above Bloom algebra on $\varphi F$ is the initial ffg-Bloom algebra.

######  Proof 4.1.

It remains to prove the universal property. Let $(A,a,\dagger)$ be any ffg-
Bloom algebra. Then the morphisms ${c}^{\dagger}:TX\to A$, for $c:TX\to FTX$
ranging over $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$, form a compatible
cocone on the diagram $D$ by functoriality. Therefore we have a unique
morphism $h:\varphi F\to A$ such that the triangles below commute

$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{in}_{c}}$$\scriptstyle{{c}^{\dagger}}$$\textstyle{\varphi
F\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\textstyle{A}$
for every $c:TX\to FTX$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$.

In order to see that $h$ is an $F$-algebra morphism consider the diagram
below:

$TX$$\scriptstyle{c}$$\scriptstyle{\mathsf{in}_{c}}$$FTX$
$\scriptstyle{F\mathsf{in}_{c}}$$\textstyle{\varphi
F\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\zeta}$$\scriptstyle{h}$$\textstyle{F(\varphi
F)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\zeta^{-1}}$$\scriptstyle{Fh}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{c}^{\dagger}}$$\textstyle{FA\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\scriptstyle{F{c}^{\dagger}}$
(4.1)

Its outside commutes, for every $c:TX\to FTX$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$, by the solution axiom for $A$, and
the left-hand and right-hand parts by the definition of $h$. The upper square
commutes by the solution axiom for $\varphi F$. Therefore, for every $c:TX\to
FTX$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ we have

$h\cdot\mathsf{in}_{c}=a\cdot Fh\cdot\zeta\cdot\mathsf{in}_{c}.$

Use that the colimit injections $\mathsf{in}_{c}$ form an epimorphic family to
conclude that $h$ is an $F$-algebra morphism, i.e. $h\cdot\zeta^{-1}=a\cdot
Fh$. This proves existence of a morphism of ffg-Bloom algebras from $\varphi
F$ to $A$.

For the uniqueness suppose that $g:\varphi F\to A$ is any morphism of ffg-
Bloom algebras. Then

$g\cdot\mathsf{in}_{c}=g\cdot c^{\ddagger}={c}^{\dagger}$

holds for every $c:TX\to FTX$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$.
Thus, $g=h$ by the universal property of the colimit $\varphi F$.

The following result provides a simple alternative characterization of the
category of ffg-Bloom algebras for $F$ without mentioning $\dagger$ and its
axioms. This result is similar to [2, Prop. 3.4] for ordinary Bloom algebras.
Here denotes the category of all $F$-algebras.

######  Proposition 20.

The category of ffg-Bloom algebras is isomorphic to the slice category
$(\varphi F,\zeta^{-1})/\\!$.

######  Proof 4.2.

(1) Given an ffg-Bloom algebra $(A,a,\dagger)$, initiality of $\varphi F$
provides an $F$-algebra morphism $h:\varphi F\to A$, i.e. an object of the
slice category. Moreover, this object assignment clearly gives rise to a
functor using the initiality of $\varphi F$.

(2) In the reverse direction, suppose we are given any $F$-algebra $(A,a)$ and
$F$-algebra morphism $h:(\varphi F,\zeta^{-1})\to(A,a)$. Then we define for
every $c:TX\to FTX$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$,

${c}^{\dagger}=(TX\xrightarrow{\mathsf{in}_{c}}\varphi F\xrightarrow{h}A).$

Then using diagram (4.1) we see that ${c}^{\dagger}$ satisfies the solution
axiom: indeed, the outside of the diagram commutes since all its inner parts
do. Moreover, functoriality of $\dagger$ follows from that of $\ddagger$:
given any $m:(TX,c)\to(TY,d)$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ we
have

${d}^{\dagger}\cdot m=h\cdot\mathsf{in}_{d}\cdot
m=h\cdot\mathsf{in}_{c}={c}^{\dagger}.$

Furthermore, given a morphism in the slice category, i.e. we have $h:(\varphi
F,\zeta^{-1})\to(A,a)$, $g:(\varphi F,\zeta^{-1})\to(B,b)$ and
$m:(A,a)\to(B,b)$ such that $m\cdot h=g$, we see that $m$ is a morphism of
ffg-Bloom algebras from $(A,a,\dagger)$ to $(B,b,\ddagger)$, where
$c^{\ddagger}:TX\to B$ is defined as $g\cdot\mathsf{in}_{c}$: indeed, $m$ is
an $F$-algebra morphism and we have

$m\cdot{c}^{\dagger}=m\cdot
h\cdot\mathsf{in}_{c}=g\cdot\mathsf{in}_{c}=c^{\ddagger}.$

That this gives a functor from the slice category to the category of ffg-Bloom
algebras is again straightforward.

(3) We have defined two identity-on-morphisms functors and it remains to show
that they are mutually inverse on objects.

From ffg-Bloom algebras to the slice category and back we form for the given
ffg-Bloom algebra $(A,a,\dagger)$ the ffg-Bloom algebra $(A,a,\ddagger)$ where
$c^{\ddagger}=h\cdot\mathsf{in}_{c}$ for the unique morphism $h:\varphi F\to
A$ of ffg-Bloom algebras. Hence, since $h$ preserves solutions we thus have
$c^{\ddagger}=h\cdot\mathsf{in}_{c}={c}^{\dagger}$ for every $c:TX\to FTX$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$.

From the slice category to ffg-Bloom algebras and back we take for a given
$F$-algebra morphism $h:(\varphi F,\zeta^{-1})\to(A,a)$ the Bloom algebra
$(A,a,\dagger)$ with ${c}^{\dagger}=h\cdot\mathsf{in}_{c}$, which shows that
$h$ is a morphism of ffg-Bloom algebras. Thus, going back to the slice
category we get back to $h$.

##  5\. Proper Functors and Full Abstractness of $\varphi F$

In this section we are going to investigate when the three left-hand fixed
points in (1.1) collapse to one, i.e. $\varphi F\cong\varrho F\cong\vartheta
F$. We introduce proper functors and show that a functor is proper if and only
if $\varphi F$ is fully abstract, i.e. a subcoalgebra of the final one. This
also entails that the rational fixed point $\varrho F$ is fully abstract and
at the same time it is determined by the coalgebras with free finitely
generated carrier. More precisely, the finality of a given locally fp
coalgebra for $F$ can be established by checking the universal property only
for the coalgebras in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ (Corollary
25). Here we continue to work under Assumptions 12.

######  Remark 21.

  1. (1)

Recall that a _zig-zag_ in a category $\mathscr{A}$ is a diagram of the form

---
$\textstyle{Z_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{0}}$$\textstyle{Z_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{1}}$$\scriptstyle{f_{2}}$$\textstyle{\cdots\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{3}}$$\scriptstyle{f_{n-2}}$$\textstyle{Z_{n}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{n-1}}$$\textstyle{Z_{1}}$$\textstyle{Z_{3}}$$\textstyle{\cdots}$$\textstyle{Z_{n-1}}$

For $\mathscr{A}={\mathsf{Set}}^{T}$, we say that the zig-zag _relates_
$z_{0}\in Z_{0}$ and $z_{n}\in Z_{n}$ if there exist $z_{i}\in Z_{i}$,
$i=1,\ldots,n-1$ such that $f_{i}(z_{i})=z_{i+1}$ for $i$ even and
$f_{i}(z_{i+1})=z_{i}$ for $i$ odd.

  2. (2)

Ésik and Maletti [17] introduced the notion of a proper semiring in order to
obtain the decidability of the (language) equivalence of weighted automata. A
semiring $\mathds{S}$ is called _proper_ provided that for every two
$\mathds{S}$-weighted automata $A$ and $B$ whose initial states $x$ and $y$,
respectively, accept the same weighted language there exists a zig-zag

---
$\textstyle{A=M_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{M_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{M_{n}=B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{M_{1}}$$\textstyle{M_{3}}$$\textstyle{\cdots}$$\textstyle{M_{n-1}}$

of simulations that _relates_ $x$ and $y$. Recall here that a _simulation_
from a weighted automaton $(i,(M^{a})_{a}{a\in A},o)$ with $n$ states to
another one $(j,(N^{a})_{a\in A},p)$ with $m$ states is an
$\mathds{S}$-semimodule morphism represented by an $n\times m$ matrix $H$ over
$\mathds{S}$ such that $i\cdot H=j$, $o\cdot H=p$ and $M_{a}\cdot H=H\cdot
N_{a}$.

Ésik and Maletti show that every Noetherian semiring is proper as well as the
semiring $\mathds{N}$ of natural numbers, which is not Noetherian. However,
the tropical semiring $(\mathds{N}\cup\\{\infty\\},\min,+,\infty,0)$ is not
proper.

Recall from Example 2.1 that $\mathds{S}$-weighted automata with input
alphabet $\Sigma$ are equivalently coalgebras with carrier $\mathds{S}^{n}$,
where $n\geq 1$ is the number of states, for the functor $FX=\mathds{S}\times
X^{\Sigma}$ on the category $\mathds{S}\textsf{-Mod}$. Note that the
$\mathds{S}^{n}$ are precisely the free finitely generated
$\mathds{S}$-semimodules, whence $\mathds{S}$-weighted automata are precisely
the coalgebras in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$, which explains
why we are interested in collecting precisely their behaviour in the form of
the fixed point $\varphi F$. Moreover, since simulations of
$\mathds{S}$-weighted automata are clearly in one to one correspondence with
$F$-coalgebra morphisms, one easily generalizes the notion of a proper
semiring as follows. Recall that $\eta_{X}:X\to TX$ denotes the unit of the
monad $T$.

We call the functor $F:\mathscr{A}\to\mathscr{A}$ _proper_ whenever for every
pair of coalgebras $c:TX\to FTX$ and $d:TY\to FTY$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ and every $x\in X$ and $y\in Y$ such
that $\eta_{X}(x)\sim\eta_{Y}(y)$ are behaviourally equivalent there exists a
zig-zag in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ relating $\eta_{X}(x)$
and $\eta_{Y}(y)$.

A semiring $\mathds{S}$ is proper iff the functor $FX=\mathds{S}\times
X^{\Sigma}$ on $\mathds{S}\textsf{-Mod}$ is proper for every input alphabet
$\Sigma$. We know that Noetherian semirings are proper (cf. Example 2.2.3),
and the semiring $\mathds{N}$ of natural numbers is proper. Recently, Sokolova
and Woracek [40] have shown that the non-negative rationals $\mathds{Q}_{+}$
and non-negative reals $\mathds{R}_{+}$ form proper semirings.

Constant functors are always proper. Indeed, suppose that $F$ is the constant
functor on some algebra $A$. Then we have $\nu F=A$, and for any $F$-coalgebra
$B$ its coalgebra structure $c:B\to FB=A$ is also the unique $F$-coalgebra
morphism from $B$ to $\nu F=A$.

Now given any $c:TX\to FTX=A$ and $d:TY\to FTY=A$ and $x\in TX$, $y\in TY$ as
in Definition 5. Then $\eta_{X}(x)\sim\eta_{Y}(y)$ is equivalent to
$c(\eta_{X}(x))=d(\eta_{Y}(y))$. Let $a$ be this element of $A$, and extend
$x:1\to X$, $y:1\to Y$ and $a:1\to A$ to $T$-algebra morphisms $Tx:T1\to TX$,
$Ty:T1\to TY$ and

${a}^{\star}:T1\to A=FT1$ (the latter yielding an $F$-coalgebra). Then

---
$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T1\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Tx}$$\scriptstyle{Ty}$$\textstyle{TY\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}$$\textstyle{TY}$

is the required zig-zag in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ relating
$\eta_{X}(x)$ and $\eta_{Y}(y)$. Sokolova and Woracek [40] have recently
proved that the functor $FX=[0,1]\times X^{\Sigma}$ on the category
${\mathsf{PCA}}$ of positively convex algebras (see Example 2.2.4) is proper.
In addition, its subfunctor $\hat{F}$ given by

$\displaystyle\hat{F}X=\\{(o,f)\in[0,1]\times X^{\Sigma}\mid\ $
$\displaystyle\forall s\in\Sigma:\exists p_{s}\in[0,1],x_{s}\in X:$
$\displaystyle o+\sum\limits_{s\in\Sigma}p_{s}\leq 1,f(s)=p_{s}x_{s}\\}$

is proper. The latter functor was used as coalgebraic type functor for the
axiomatization of probabilistic systems in [38]. In fact, the completeness
proof of the expression calculus in loc. cit. makes use of our Corollary 25
below.

In general, it seems to be non-trivial to establish that a given functor is
proper (even for the identity functor this may fail; in the light of Theorem
22 below this follows from Example 3(1)). However, we will provide in
Proposition 26 sufficient conditions on $\mathscr{A}$ and $F$ the entail
properness using our main result:

######  Theorem 22.

The functor $F$ is proper iff the coalgebra $\varphi F$ is a subcoalgebra of
$\nu F$.

The latter condition states that the unique coalgebra morphism $m:\varphi
F\to\nu F$ is a monomorphism in $\mathscr{A}$.

We present the proof of this theorem in Section 6. Here we continue with a
discussion of the consequences of this result.

######  Corollary 23.

If $F$ is proper, then $\varphi F$ is the rational fixed point of $F$.

######  Proof 5.1.

Let $u:\varrho F\to\nu F$ be the unique $F$-coalgebra morphism. Then we have a
commutative triangle of $F$-coalgebra morphisms due to finality of $\nu F$:

$\textstyle{\varphi
F\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\textstyle{\varrho
F\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{u}$$\textstyle{\nu
F.\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$

Since $F$ is proper, $m$ is a monomorphism in $\mathscr{A}$, hence so is $h$.
Since $h$ is also a strong epimorphism by Proposition 17, it is an
isomorphism. Thus, $\varphi F\cong\varrho F$ is the rational fixed point of
$F$.

######  Corollary 24.

Suppose that $F$ preserves non-empty monomorphisms. Then the functor $F$ is
proper iff $\varphi F\cong\varrho F\cong\vartheta F\rightarrowtail\nu F$.

######  Proof 5.2.

If the three fixed points are isomorphic, then $F$ is proper by Theorem 22.

Conversely, since $F$ preserves non-empty monomorphisms, we have the situation
displayed in (1.1) (see Corollary 18). Now if $F$ is proper we know from
Corollary 23 that $\varphi F\cong\varrho F$. Thus, $\varrho F$ is a
subcoalgebra of $\nu F$, i.e. the composition of the last two morphisms in
(1.1) is a monomorphism. Thus, so is $\varrho F\twoheadrightarrow\vartheta F$.
Since this is also a strong epimorphism, we conclude that $\varrho
F\cong\vartheta F$.

Note that this result also entails full abstractness of $\varphi F\cong\varrho
F$.

A key result for establishing soundness and completeness of coalgebraic
regular expression calculi is the following corollary (cf. [12, Corollary
3.36] and its applications in Sections 4 and 5 of loc. cit.).

######  Corollary 25.

Suppose that $F$ is proper. Then an $F$-coalgebra $(R,r)$ is a final locally
fp coalgebra if and only if $(R,r)$ is locally fp and for every coalgebra
$(TX,c)$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ there exists a unique
$F$-coalgebra morphism from $TX$ to $R$.

######  Proof 5.3.

The implication “$\Rightarrow$” clearly holds

For “$\Leftarrow$” it suffices to prove that for every $a:A\to FA$ in
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ there exists a unique $F$-coalgebra
morphism from $A$ to $R$. In fact, it then follows that $R$ is the final
locally fp coalgebra. To see this write an arbitrary locally fp coalgebra $A$
as a filtered colimit of a diagram
$D:\mathscr{D}\to\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F\hookrightarrow\mathop{\mathsf{Coalg}}F$
with colimit injections $h_{d}:Dd\to A$ ($d$ an object in $\mathscr{D}$). Then
the unique $F$-coalgebra morphisms $u_{d}:Dd\to R$ form a compatible cocone,
and so one obtains a unique $u:A\to R$ such that $u\cdot h_{d}=u_{d}$ holds
for every object $d$ of $\mathscr{D}$. It is now straightforward to prove that
$u$ is a unique $F$-coalgebra morphism from $A$ to $R$.

Now let $a:A\to FA$ be a coalgebra in
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$. For every $(TX,c)$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ denote by $c^{\ddagger}:TX\to R$ the
unique $F$-coalgebra morphism that exists by assumption. These morphisms
$c^{\ddagger}$ form a compatible cocone of the diagram
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F\hookrightarrow\mathop{\mathsf{Coalg}}F$.
Thus, we obtain a unique $F$-coalgebra morphism $m^{\prime}:\varphi
F\cong\varrho F\to R$ such that the following diagram commutes for every
$c:TX\to FTX$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$:

$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{in}_{c}}$$\scriptstyle{{c}^{\sharp}}$$\scriptstyle{c^{\ddagger}}$$\textstyle{\varphi
F\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\cong}$$\textstyle{\varrho
F\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m^{\prime}}$$\textstyle{R}$

Therefore we have an $F$-coalgebra morphism

$h=(A\xrightarrow{{a}^{\sharp}}\varrho F\xrightarrow{m^{\prime}}R).$

To prove it is unique, assume that $g:A\to R$ is any $F$-coalgebra morphism.
As in the proof of Proposition 17, we know that $A$ is the quotient of some
$TX$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ via $q:TX\twoheadrightarrow
A$, say. Then we have

$m^{\prime}\cdot{a}^{\sharp}\cdot q=g\cdot q$

because there is only one $F$-coalgebra morphism from $TX$ to $R$ by
hypothesis. It follows that $h=m^{\prime}\cdot{a}^{\sharp}=g$ since $q$ is
epimorphic.

The next result provides sufficient conditions for properness of $F$. It can
be seen as a category-theoretic generalization of Ésik’s and Maletti’s result
[17, Theorem 4.2] that Noetherian semirings are proper.

######  Proposition 26.

Suppose that finitely generated algebras in $\mathscr{A}$ are closed under
kernel pairs and that $F$ maps kernel pairs to weak pullbacks in
${\mathsf{Set}}$. Then $F$ is proper.

######  Proof 5.4.

First, since $F$ maps kernel pairs to weak pullbacks in ${\mathsf{Set}}$ we
see that $F$ preserves monomorphisms; indeed, $m:A\rightarrowtail B$ is a mono
in $\mathscr{A}$ iff and only if its kernel pair is
$\mathsf{id}_{A},\mathsf{id}_{A}$. Thus $F\mathsf{id}_{A},F\mathsf{id}_{A}$
form a weak pullback in ${\mathsf{Set}}$, which is in fact a pullback, whence
$Fm$ is monomorphic.

Now let $(TX,c)$ and $(TY,d)$ be in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$,
$x\in X$ and $y\in Y$ such that $\dagger c(\eta_{X}(x))=\dagger
d(\eta_{Y}(y))$. It is our task to construct a zig-zag relating $\eta_{X}(x)$
and $\eta_{Y}(y)$.

Form $Z=X+Y$ and let $e:TZ\to FTZ$ be the coproduct of the coalgebras $(TX,c)$
and $(TY,d)$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ (see Lemma 15). Take
the factorization of $\dagger e:TZ\to\nu F$ into a strong epi
$q:TZ\twoheadrightarrow A$ followed by a monomorphism $m:A\rightarrowtail\nu
F$. Since $F$ preserves non-empty monos, we obtain a unique coalgebra
structure $a:A\to FA$ such that $q$ and $m$ are coalgebra morphisms (see
Remark 9(2)). Now take the kernel pair
$f,g:K\mathbin{\raisebox{2.0pt}{$\rightarrow$}\raisebox{-2.0pt}{$\rightarrow$}}TZ$
of $q$. Since $TZ$ and its quotient $A$ are finitely generated $T$-algebras,
so is $K$ because finitely generated $T$-algebras are closed under taking
kernel pairs by assumption. Now $F$ maps the kernel pair $f,g$ to a weak
pullback $Ff,Fg$ of $Fq$ along itself in ${\mathsf{Set}}$. Thus, we have a map
$k\colon K\to FK$ such that the diagram below commutes:

$\textstyle{K\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{k}$$\textstyle{FK\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Fg}$$\scriptstyle{Ff}$$\textstyle{TZ\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\scriptstyle{e}$$\textstyle{FTZ\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Fq}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\textstyle{FA}$
(5.1)

Notice that we do not claim that $k$ is a $T$-algebra morphism. However, since
$K$ is a finitely generated $T$-algebra, it is the quotient of some free
finitely generated $T$-algebra $TR$ via $p\colon TR\twoheadrightarrow K$, say.
Now we choose some splitting $s\colon K\to TR$ of $p$ in ${\mathsf{Set}}$, i.
e., $s$ is a map such that $p\cdot s=\mathsf{id}$. Next we extend the map
$r_{0}=Fs\cdot k\cdot p\cdot\eta_{R}$ to a $T$-algebra morphism $r\colon TR\to
FTR$; it follows that the outside of the diagram below commutes:

$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{R}}$$\scriptstyle{r_{0}}$$\textstyle{TR\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{r}$$\scriptstyle{p}$$\textstyle{FTR\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Fp}$$\textstyle{K\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{k}$$\textstyle{FK}$
(5.2)

(Notice that to obtain $r$ we cannot simply use projectivity of $TR$ since $k$
is not necessarily a $T$-algebra homomorphism.)

We do not claim that this makes $p$ a coalgebra morphism (i. e., we do not
claim the lower square in (5.2) commutes). However, $f\cdot p$ and $g\cdot p$
are coalgebra morphisms from $(TR,r)$ to $(TZ,e)$; in fact, to see that

$e\cdot(f\cdot p)=F(f\cdot p)\cdot r$

it suffices that this equation of $T$-algebra morphisms holds when both sides
are precomposed with $\eta_{R}$. To this end we compute

$\begin{array}[]{rcl@{\qquad}p{3cm}}e\cdot f\cdot p\cdot\eta_{R}&=&Ff\cdot
k\cdot p\cdot\eta_{R}&see~{}\eqref{diag:kappa},\\\ &=&Ff\cdot Fp\cdot
r_{0}&outside of~{}\eqref{diag:d},\\\ &=&Ff\cdot Fp\cdot
r\cdot\eta_{R}&definition of $d$.\end{array}$

Similarly, $g\cdot p$ is a coalgebra morphism.

Now consider the following zig-zag in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ (recall that the algebra $TZ$ is the
coproduct of $TX$ and $TY$ with coproduct injections $T\mathsf{inl}$ and
$T\mathsf{inr}$):

---
$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T\mathsf{inl}}$$\textstyle{TR\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f\cdot
p}$$\scriptstyle{g\cdot
p}$$\textstyle{TY\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T\mathsf{inr}}$$\textstyle{TZ}$$\textstyle{TZ}$

We now show that this zig-zag relates $\eta_{X}(x)$ and $\eta_{Y}(y)$. Let
$x^{\prime}=T\mathsf{inl}(\eta_{X}(x))$ and
$y^{\prime}=T\mathsf{inr}(\eta_{Y}(y))$. Then we have

$\dagger e(x^{\prime})=\dagger e\cdot T\mathsf{inl}(\eta_{X}(x))=\dagger
c(\eta_{X}(x))=\dagger d(\eta_{Y}(y))=\dagger e\cdot
T\mathsf{inr}(\eta_{Y}(y))=\dagger e(y^{\prime}).$

Hence, since $\dagger e=m\cdot q$ and $m$ is monomorphic, we obtain
$q(x^{\prime})=q(y^{\prime})$. Thus, there exists some $k\in K$ such that
$f(k)=x^{\prime}$ and $g(k)=y^{\prime}$ by the universal property of the
kernel pair. Finally, since $p:TR\twoheadrightarrow K$ is surjective we obtain
some $z\in TR$ such that $p(z)=k$ whence $f\cdot p(z)=x^{\prime}$ and $g\cdot
p(z)=y^{\prime}$. This completes the proof.

######  Remark 27.

  1. (1)

Note that closure of finitely generated algebras under kernel pairs can
equivalently be stated in general algebra terms as follows: every congruence
$R$ of a finitely generated algebra $A$ is finitely generated as a subalgebra
$R\hookrightarrow A\times A$ (observe that this is _not_ equivalent to stating
that $R$ is a finitely generated congruence).

  2. (2)

For a lifting $F$ of a set functor $F_{0}$, the condition that $F$ maps kernel
pairs to weak pullbacks in ${\mathsf{Set}}$ holds whenever $F_{0}$ preserves
weak pullbacks. Hence, all the functors on algebraic categories mentioned in
Example 2.2 satisfy this assumption.

  3. (3)

For the special case of a lifting, a variant of the argument in the proof of
Proposition 26 was used in [12, Proposition 3.34] in order to prove that every
coalgebra in $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ is a coequalizer of a
parallel pair of morphisms in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$. This
has inspired Winter [42, Proposition 7] who uses a very similar argument to
prove that, for a distributive law $\lambda$, $\lambda$-bisimulations (see
Bartels [10]) are sound and complete for $\lambda$-bialgebras (see Remark 13).
It turns out that, for a lifting $F$, Proposition 26 is a consequence of
Winter’s result, or, in other words, our result can be understood as a slight
generalization of Winter’s one.

  1. (1)

The first condition in Proposition 26 is not necessary for properness of $F$.
In fact, it fails in the category of semimodules for $\mathds{N}$, viz. the
category of commutative monoids: in fact, consider the finitely generated
commutative monoid $\mathds{N}\times\mathds{N}$ and its submonoid infinitely
generated by

$\\{(n,n+1)\mid n\in\mathds{N}\\},$

which is easily seen not be finitely generated. However, as we mentioned in
Example 5, $FX=\mathds{N}\times X^{\Sigma}$ is proper on the category of
commutative monoids.

  2. (2)

In Example 2.2(4) we mentioned that, in the category ${\mathsf{PCA}}$ of
positively convex algebras, fg- and fp-objects coincide. However, fg-objects
are not closed under kernel pairs. In fact, the interval $[0,1]$ is the free
positively convex algebra on two generators, but
$\\{(0,0),(1,1)\\}\cup(0,1)\times(0,1)$ is a congruence on $[0,1]$ that is not
an fg-object (i.e. a polytope) [39, Example 4.13]. Thus, properness of the
functors in Example 5 does not follow from Proposition 26.

##  6\. Proof of Theorem 22

In this section we will present the proof of our main result Theorem 22. We
start with two technical lemmas.

######  Remark 28.

Recall [9, Proposition 11.28.2] that every free $T$-algebra $TX$ is _perfectly
presentable_ , i.e. the hom-functor ${\mathsf{Set}}^{T}(TX,-)$ preserves
sifted colimits (cf. Remark 14). It follows that for every sifted diagram
$D:\mathscr{D}\to{\mathsf{Set}}^{T}$ and every $T$-algebra morphism
$h:TX\to\mathop{\mathrm{colim}}D$ there exists some $d\in\mathscr{D}$ and
$h^{\prime}:TX\to Dd$ such that

$\textstyle{Dd\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{in}_{d}}$$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h^{\prime}}$$\scriptstyle{h}$$\textstyle{\mathop{\mathrm{colim}}D.}$

######  Lemma 29.

For every finite set $X$ and map $f:X\to\varphi F$ there exists an object
$(TY,d)$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ and a map $g:X\to Y$
such that the triangle below commutes:

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{g}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{Y}}$$\textstyle{TY\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{in}_{d}}$$\textstyle{\varphi
F}$

######  Proof 6.1.

We begin by extending $f$ to a $T$-algebra morphism
$h={f}^{\star}:TX\to\varphi F$. By Remark 28, there exists some $c:TZ\to FTZ$
in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ and a $T$-algebra morphism
$h^{\prime}:TX\to TZ$ such that $h=\mathsf{in}_{c}\cdot h^{\prime}$. Let
$f^{\prime}=h^{\prime}\cdot\eta_{X}$, let $Y=X+Z$ and consider the $T$-algebra
morphism ${[f^{\prime},\eta_{Z}]}^{\star}:TY\to TZ$. This is a split
epimorphism in ${\mathsf{Set}}^{T}$; we have $T\mathsf{inr}:TZ\to TY$ with

${[f^{\prime},\eta_{Z}]}^{\star}\cdot
T\mathsf{inr}={\eta_{Z}}^{\star}=\mathsf{id}_{TZ},$

where the last equation follows from the uniqueness property of
${\eta_{Z}}^{\star}$ (see Section 2.1) by the laws of ${(-)}^{\star}$. We
therefore get a coalgebra structure

$d=(TY\xrightarrow{{[f^{\prime},\eta_{Z}]}^{\star}}TZ\xrightarrow{c}FTZ\xrightarrow{T\mathsf{inr}}FTY)$

such that ${[f^{\prime},\eta_{Z}]}^{\star}$ is an $F$-coalgebra morphism from
$(TY,d)$ to $(TZ,c)$. Since $Y$ is a finite set, $(TY,d)$ is an $F$-coalgebra
in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$, and hence
$\mathsf{in}_{c}\cdot{[f^{\prime},\eta_{Z}]}^{\star}=\mathsf{in}_{d}$. Thus we
see that $g=\mathsf{inl}:X\to Y$ is the desired morphism due to the
commutative diagram below:

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g=\mathsf{inl}}$$\scriptstyle{f^{\prime}}$$\scriptstyle{f}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{Y}}$$\scriptstyle{[f^{\prime},\eta_{Z}]}$$\textstyle{TY\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{[f^{\prime},\eta_{Z}]}^{\star}}$$\textstyle{TZ\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{in}_{c}}$$\textstyle{\varphi
F\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{in}_{d}}$

######  Remark 30.

Recall that a colimit of a diagram $D:\mathscr{D}\to{\mathsf{Set}}$ is
computed as follows:

$\mathop{\mathrm{colim}}D=\big{(}\\!\coprod\limits_{d\in\mathscr{D}}Dd\big{)}/\mathord{\sim},$

where $\sim$ is the least equivalence on the coproduct (i.e. the disjoint
union) of all $Dd$ with $x\sim Df(x)$ for every $f:d\to d^{\prime}$ in
$\mathscr{D}$ and every $x\in Dd$. In other words, for every pair of objects
$c,d$ of $\mathscr{D}$ and $x\in Dc$, $y\in Dd$ we have $x\sim y$ iff there is
a zig-zag in $\mathscr{D}$ whose $D$-image

---
$\textstyle{Dc=Dz_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Df_{0}}$$\textstyle{Dz_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Df_{1}}$$\scriptstyle{Df_{2}}$$\textstyle{\cdots\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Df_{3}}$$\scriptstyle{Df_{n-2}}$$\textstyle{z_{n}=Dd\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Df_{n-1}}$$\textstyle{Dz_{1}}$$\textstyle{Dz_{3}}$$\textstyle{\cdots}$$\textstyle{Dz_{n-1}}$

relates $x$ and $y$ (cf. Remark 21).

######  Lemma 31.

Let $(TX,c)$ and $(TY,d)$ be coalgebras in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$, $x\in TX$, and $y\in TY$. Then the
following are equivalent:

  1. (1)

$\mathsf{in}_{c}(x)=\mathsf{in}_{d}(y)\in\varphi F$, and

  2. (2)

there is a zig-zag in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ relating $x$
and $y$.

######  Proof 6.2.

By Remark 14(3), $\varphi F$ is a sifted colimit. Hence, the forgetful functor
$\mathop{\mathsf{Coalg}}F\to{\mathsf{Set}}^{T}\to{\mathsf{Set}}$ preserves
this colimit. Thus the colimit $\varphi F$ is formed as recalled in Remark 30:

$\varphi F\cong\big{(}\coprod_{c}TX_{c}\big{)}/\mathord{\sim},$

where $c:TX_{c}\to FTX_{c}$ ranges over the objects of
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$. Therefore, we have the desired
equivalence.

######  Proof 6.3 (Proof of Theorem 22).

“$\Rightarrow$” Suppose that for $m:\varphi F\to\nu F$ we have $x,y\in\varphi
F$ with $m(x)=m(y)$. We apply Lemma 29 to

$1\xrightarrow{x}\varphi F\qquad\text{and}\qquad 1\xrightarrow{y}\varphi F,$

respectively, to obtain two objects $c:TX\to FTX$ and $d:TY\to FTY$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ with $x^{\prime}\in X$ and
$y^{\prime}\in Y$ such that $\mathsf{in}_{c}(\eta_{X}(x^{\prime}))=x$ and
$\mathsf{in}_{d}(\eta_{Y}(y^{\prime}))=y$. By the uniqueness of coalgebra
morphisms into $\nu F$ we have

$\dagger c=m\cdot\mathsf{in}_{c}\qquad\text{and}\qquad\dagger
d=m\cdot\mathsf{in}_{d}.$ (6.1)

Thus we compute:

$\dagger
c(\eta_{X}(x^{\prime}))=m\cdot\mathsf{in}_{c}\cdot\eta_{X}(x^{\prime})=m(x)=m(y)=m\cdot\mathsf{in}_{d}\cdot\eta_{Y}(y^{\prime})=\dagger
d(\eta_{Y}(y^{\prime})).$

Since $F$ is proper by assumption, we obtain a zig-zag in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ relating $\eta_{X}(x^{\prime})$ and
$\eta_{Y}(y^{\prime})$. By Lemma 31, these two elements are merged by the
colimit injections, and we have
$x=\mathsf{in}_{c}(\eta_{X}(x^{\prime}))=\mathsf{in}_{d}(\eta_{Y}(y^{\prime})=y$.
We conclude that $m$ is monomorphic.

“$\Leftarrow$” Suppose that $m:\varphi F\rightarrowtail\nu F$ is a
monomorphism. Let $c:TX\to FTX$ and $d:TY\to FTY$ be objects of
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$, and let $x\in X$ and $y\in Y$ be
such that $\dagger c(\eta_{X}(x))=\dagger d(\eta_{Y}(y))$. Using (6.1) and the
fact that $m$ is monomorphic we get
$\mathsf{in}_{c}(\eta_{X}(x))=\mathsf{in}_{d}(\eta_{Y}(y))$. By Lemma 31, we
thus obtain a zig-zag in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ relating
$\eta_{X}(x)$ and $\eta_{Y}(y)$. This proves that $F$ is proper.

##  7\. Conclusions and Further Work

Inspired by Ésik and Maletti’s notion of a proper semiring, we have introduced
the notion of a proper functor. We have shown that, for a proper endofunctor
$F$ on an algebraic category preserving regular epis and monos, the rational
fixed point $\varrho F$ is fully abstract and moreover determined by those
coalgebras with a free finitely generated carrier (i.e. the target coalgebras
of generalized determinization).

Our main result also shows that properness is necessary for this kind of full
abstractness. For categories in which fg-objects are closed under kernel pairs
we saw that when $F$ maps kernel pairs to weak pullbacks in ${\mathsf{Set}}$,
then it is proper. This provides a number of examples of proper functors.
However, in several categories of interest the condition on kernel pairs
fails, e.g. in $\mathds{N}$-semimodules (commutative monoids) and positively
convex algebras. There can still be proper functors, e.g. $FX=\mathds{N}\times
X^{\Sigma}$ on the former and $FX=[0,1]\times X^{\Sigma}$ on the latter. But
establishing properness of a functor without using Proposition 26 seems non-
trivial, and we leave the task of finding more examples of proper functors for
further work.

One immediate consequence of our results is that the soundness and
completeness proof for the expression calculi for weighted automata [12]
extends from Noetherian to proper semirings. In fact, Ésik and Kuich [16,
Theorems 7.1 and 8.5] already provide sound and complete axiomatizations of
weighted language equivalence for (certain subclasses of) proper semirings
$\mathds{S}$ by showing that $\mathds{S}$-rational weighted languages form
certain free algebras.

In the future, when additional proper functors are known, it will be
interesting to study regular expression calculi for their coalgebras and use
the technical machinery developed in the present paper for soundness and
completeness proofs.

Another task for future work is to study the new fixed point $\varphi F$ in
its own right. Here we have already proven that $\varphi F$ is characterized
uniquely (up to isomorphism) as the initial ffg-Bloom algebra. In the future,
it might be interesting to investigate _free_ (rather than initial) ffg-Bloom
algebras. Moreover, related to ordinary Bloom algebras [2] there is the notion
of an Elgot algebra [4]. It is known that for every object $Y$ of an lfp
category, the parametric rational fixed point $\varrho(F(-)+Y)$ yields a free
Elgot algebra on $Y$. In addition, the category of algebras for the ensuing
monad is isomorphic to the category of Elgot algebras for $F$. In [3], the new
notion of an ffg-Elgot algebra for $F$ is introduced, and it is shown that for
free finitely generated algebras $Y$ the parametric fixed point
$\varphi(F(-)+Y)$ forms a free ffg-Elgot algebra for $F$ on $Y$, and
furthermore the category of ffg-Elgot algebras for $F$ is monadic over our
algebraic base category $\mathscr{A}$. It remains an open question whether
ffg-Elgot algebras (or ffg-Bloom algebras) are monadic over ${\mathsf{Set}}$.

## References

  * [1] J. Adámek.  Introduction to coalgebra.  Theory Appl. Categ., 14:157–199, 2005.
  * [2] J. Adámek, M. Haddadi, and S. Milius.  Corecursive algebras, corecursive monads and Bloom monads.  Log. Methods Comput. Sci., 10(3:19):51 pp., 2014.
  * [3] J. Adámek, S. Milius, and H. Urbat.  On algebras with effectful iteration.  In C. Cîrstea, editor, Proc. Coalgebraic Methods in Computer Science (CMCS’18), Lecture Notes Comput. Sci., 2018.  To appear.
  * [4] J. Adámek, S. Milius, and J. Velebil.  Elgot algebras.  Log. Methods Comput. Sci., 2(5:4):31 pp., 2006.
  * [5] J. Adámek, S. Milius, and J. Velebil.  Iterative algebras at work.  Math. Structures Comput. Sci., 16(6):1085–1131, 2006.
  * [6] J. Adámek, S. Milius, and J. Velebil.  On second-order iterative monads.  Theoret. Comput. Sci., 412:4969–4988, 2011.  http://dx.doi.org/10.1016/j.tcs.2011.04.027.
  * [7] J. Adámek, S. Milius, and J. Velebil.  Semantics of higher-order recursion schemes.  Log. Methods Comput. Sci., 7(1:15):43 pp., 2011.
  * [8] J. Adámek and J. Rosický.  Locally presentable and accessible categories.  Cambridge University Press, 1994.
  * [9] J. Adámek, J. Rosický, and E. Vitale.  Algebraic Theories.  Cambridge University Press, 2011.
  * [10] F. Bartels.  On generalized coinduction and probabilistic specification formats.  PhD thesis, Vrije Universiteit Amsterdam, 2004.
  * [11] J. Berstel and C. Reutenauer.  Rational Series and Their Languages.  Springer-Verlag, 1988.
  * [12] M. M. Bonsangue, S. Milius, and A. Silva.  Sound and complete axiomatizations of coalgebraic language equivalence.  ACM Trans. Comput. Log., 14(1:7), 2013.
  * [13] B. Courcelle.  Fundamental properties of infinite trees.  Theoret. Comput. Sci., 25:95–169, 1983.
  * [14] E. Doberkat.  Eilenberg-moore algebras for stochastic relations.  Inf. Comput., 204(12):1756–1781, 2006.
  * [15] E. Doberkat.  Erratum and addendum: Eilenberg-moore algebras for stochastic relations.  Inf. Comput., 206(12):1476–1484, 2008.
  * [16] Z. Ésik and W. Kuich.  Free iterative and iteration $k$-semialgebras.  Algebra Univ., 67(2):141–162, 2012.
  * [17] Z. Ésik and A. Maletti.  Simulation vs. equivalence.  In H. R. Arabnia, G. A. Gravvanis, and A. M. G. Solo, editors, Proc. 6th Int. Conf. Foundations of Computer Science, pages 119–122. CSREA Press, 2010.
  * [18] Z. Ésik and A. Maletti.  Simulations of weighted tree automata.  In M. Domaratzki and K. Salomaa, editors, Proc. 15th International Conference on Implementation and Application of Automata (CIAA), volume 6482 of Lecture Notes Comput. Sci., pages 321–330. Springer, 2011.
  * [19] M. Fiore, G. D. Plotkin, and D. Turi.  Abstract syntax and variable binding.  In Proc. Logic in Computer Science 1999, pages 193–202. IEEE Press, 1999.
  * [20] P. Freyd.  Rèdei’s finiteness theorem for commutative semigroups.  Proc. Amer. Math. Soc., 19(4), 1968.
  * [21] S. Ginali.  Regular trees and the free iterative theory.  J. Comput. System Sci., 18:228–242, 1979.
  * [22] S. Goncharov, S. Milius, and A. Silva.  Towards a coalgebraic Chomsky hierarchy (extended abstract).  In J. Diaz, I. Lanese, and D. Sangiorgi, editors, Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS’14), volume 8705 of Lecture Notes Comput. Sci., pages 265–280. Springer, 2014.
  * [23] B. Jacobs, A. Silva, and A. Sokolova.  Trace semantics via determinization.  J. Comput. System Sci., 2015.
  * [24] P. T. Johnstone.  Adjoint lifting theorems for categories of algebras.  Bull. London Math. Soc., 7:294–297, 1975.
  * [25] S. Milius.  A sound and complete calculus for finite stream circuits.  In Proc. 25th Annual Symposium on Logic in Computer Science (LICS’10), pages 449–458. IEEE Computer Society, 2010.
  * [26] S. Milius.  Proper functors and their rational fixed point.  In F. Bonchi and B. König, editors, Proc. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO’17), volume 72 of LIPIcs, pages 18:1–18:15. Schloss Dagstuhl, 2017.  To appear.
  * [27] S. Milius, D. Pattinson, and T. Wißmann.  A new foundation for finitary corecursion and iterative algebras.  submitted; available at https://arxiv.org/abs/1802.08070, 2017.
  * [28] S. Milius, L. Schröder, and T. Wißmann.  Regular behaviours with names: On rational fixpoints of endofunctors on nominal sets.  Appl. Categ. Structures, 24(5):663–701, 2016.  http://link.springer.com/article/10.1007/s10485-016-9457-8.
  * [29] S. Milius and T. Wißmann.  Finitary corecursion for the infinitary lambda calculus.  In L. S. Moss and P. Sobocinski, editors, Proc. Coalgebraic and Algebraic Methods in Computer Science (CALCO’15), volume 35 of LIPICS, pages 336–351, 2015.
  * [30] I. Petre and A. Salomaa.  Algebraic systems and pushdown automata.  In Handbook of Weighted Automata, pages 257–289. Springer, 2009\.
  * [31] L. Rèdei.  The Theory of Finitely Generated Commutative Semigroups.  Pergamon, Oxford-Edinburgh-New York, 1965.
  * [32] J. J. M. M. Rutten.  Automata and coinduction (an exercise in coalgebra).  In D. Sangiorgi and R. de Simone, editors, Proc. CONCUR 1998, volume 1466 of Lecture Notes Comput. Sci., pages 194–218. Springer, 1998\.
  * [33] J. J. M. M. Rutten.  Universal coalgebra: a theory of systems.  Theoret. Comput. Sci., 249(1):3–80, 2000.
  * [34] J. J. M. M. Rutten.  Rational streams coalgebraically.  Log. Methods Comput. Sci., 4(3:9):22 pp., 2008.
  * [35] M. P. Schützenberger.  On the definition of a family of automata.  Inform. and Control, 4(2–3):275–270, 1961.
  * [36] A. Silva, F. Bonchi, M. M. Bonsangue, and J. J. M. M. Rutten.  Generalizing determinization from automata to coalgebras.  Log. Methods Comput. Sci, 9(1:9), 2013.
  * [37] A. Silva, M. M. Bonsangue, and J. J. M. M. Rutten.  Non-deterministic Kleene coalgebras.  Log. Methods Comput. Sci., 6(3:23):39 pp., 2010.
  * [38] A. Silva and A. Sokolova.  Sound and complete axiomatization of trace semantics for probabilistic systems.  Electr. Notes Theor. Comput. Sci., 276:291–311, 2011.
  * [39] A. Sokolova and H. Woracek.  Congruences of convex algebras.  J. Pure Appl. Algebra, 219(8):3110–3148, 2015.
  * [40] A. Sokolova and H. Woracek.  Proper semirings and proper convex functors.  Technical Report 22/2017, Institute for Analysis and Scientific Computing – Vienna University of Technology, TU Wien, 2017.  Available at http://www.asc.tuwien.ac.at/preprint/2017/asc22x2017.pdf.
  * [41] H. Urbat.  Finite behaviours and finitary corecursion.  In F. Bonchi and B. König, editors, Proc. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017), volume 72 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1–24:15, 2017.
  * [42] J. Winter.  A completeness result for finite $\lambda$-bisimulations.  In Proc. Foundations of Software Science and Computation Structures (FoSSaCS), volume 9034 of Lecture Notes Comput. Sci., pages 117–132, 2015.
  * [43] J. Winter, M. Bonsangue, and J. Rutten.  Coalgebraic Characterizations of Context-Free Languages.  Log. Methods Comput. Sci., 9(3), September 2013.
  * [44] J. Winter, M. M. Bonsangue, and J. J. Rutten.  Context-free coalgebras.  J. Comput. System Sci., 81(5):911–939, 2015.

## Appendix: Category Theoretic Proof of Proposition 17

Note first that for every $c:TX\to FTX$ in
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ we clearly have

${c}^{\sharp}=(TX\xrightarrow{\mathsf{in}_{c}}\varphi F\xrightarrow{h}\varrho
F)$

by the finality of $\varrho F$. Recall that for strong epis the same
cancellation law as for epis holds: if $e\cdot e^{\prime}$ is a strong epi,
then so is $e$; a similar law holds for strongly epimorphic families. Hence,
we are done if we show that the ${c}^{\sharp}$ where $c:TX\to FTX$ ranges over
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ forms a jointly strongly epimorphic
family, too. This is done by using that the ${a}^{\sharp}$, where $a:A\to FA$
ranges over $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$, form a strongly
epimorphic family (to see this use Lemma 2 once again).

The key observation is as follows: given any $a:A\to FA$ in
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ we know that its carrier is a regular
quotient of some free $T$-algebra $TX$ with $X$ finite, via
$q:TX\twoheadrightarrow A$, say. Since $F$ preserves regular epis ($=$
surjections) we can use projectivity of $TX$ (see Remark 3(2)) to obtain a
coalgebra structure $c$ on $TX$ making $q$ an $F$-coalgebra morphism:

$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c}$$\scriptstyle{q}$$\textstyle{FTX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Fq}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\textstyle{FA}$

This implies that we have ${c}^{\sharp}={a}^{\sharp}\cdot q$.

Now suppose that we have two parallel morphisms $f,g$ such that for every
$c:TX\to FTX$ in $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ we have
$f\cdot{c}^{\sharp}=g\cdot{c}^{\sharp}$. Then for every $a:A\to FA$ in
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ we obtain

$f\cdot{a}^{\sharp}\cdot
q=f\cdot{c}^{\sharp}=g\cdot{c}^{\sharp}=g\cdot{a}^{\sharp}\cdot q,$

which implies that $f\cdot{a}^{\sharp}=g\cdot{a}^{\sharp}$ since $q$ is
epimorphic. Hence $f=g$ since the ${a}^{\sharp}$ form a jointly epimorphic
family. This proves that the ${c}^{\sharp}$ form a jointly epimorphic family.

To see that they form a strongly jointly epimorphic family, assume that we are
given a monomorphism $m:M\rightarrowtail N$ and morphisms $g:\varrho F\to N$
and $f_{c}:TX\to M$ for every $c:TX\to FTX$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ such that $m\cdot
f_{c}=g\cdot{c}^{\sharp}$. We extend the family $(f_{c})$ to one indexed by
all $a:A\to FA$ in $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$ as follows. We
have that any such $(A,a)$ is a quotient coalgebra of some $(TX,c)$ via
$q:TX\twoheadrightarrow A$, which is the coequalizer of some parallel pair
$k_{1},k_{2}:K\to TX$ in $\mathscr{A}$. Thus we have

$\displaystyle m\cdot f_{c}\cdot k_{1}$ $\displaystyle=g\cdot{c}^{\sharp}\cdot
k_{1}$ $\displaystyle=g\cdot{a}^{\sharp}\cdot q\cdot k_{1}$
$\displaystyle=g\cdot{a}^{\sharp}\cdot q\cdot k_{2}$
$\displaystyle=g\cdot{c}^{\sharp}\cdot k_{2}$ $\displaystyle=m\cdot f_{c}\cdot
k_{2},$

which implies that $f_{c}\cdot k_{1}=f_{c}\cdot k_{2}$ since $m$ is
monomorphic. Therefore we obtain a unique $f_{a}:A\to M$ such that $f_{a}\cdot
q=f_{c}$ using the universal property of the coequalizer $q$. Hence we can
compute

$m\cdot f_{a}\cdot q=m\cdot f_{c}=g\cdot{c}^{\sharp}=g\cdot{a}^{\sharp}\cdot
q,$

which implies $m\cdot f_{a}=g\cdot{a}^{\sharp}$ since $q$ is epimorphic. Now
we use that the ${a}^{\sharp}$ are jointly strongly epimorphic (cf. Lemma 2)
to obtain a unique morphism $d:\varrho F\to M$ with $d\cdot{a}^{\sharp}=f_{a}$
and $m\cdot d=g$ for all $a:A\to FA$ in
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$. In particular, $d$ is the desired
diagonal fill-in since $\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ is a full
subcategory of $\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$. As for the uniqueness
of the fill-in $d$ we still need to check that any $d$ with
$d\cdot{c}^{\sharp}=f_{c}$ for all $c:TX\to FTX$ in
$\mathop{\mathsf{Coalg}_{\mathsf{ffg}}}F$ and $m\cdot d=g$ also fulfils
$d\cdot{a}^{\sharp}=f_{a}$ for every $a:A\to FA$ in
$\mathop{\mathsf{Coalg}_{\mathsf{fp}}}F$. Indeed, this follows from

$d\cdot{a}^{\sharp}\cdot q=d\cdot{c}^{\sharp}=f_{c}=f_{a}\cdot q$

using that $q$ is epimorphic. ∎