Radboud University, Nijmegen, The Netherlands and https://thorsten-
wissmann.dethorsten.wissmann@ru.nlhttps://orcid.org/0000-0001-8993-6486
Thorsten Wißmann <ccs2012> <concept>
<concept_id>10003752.10003766</concept_id> <concept_desc>Theory of computation
Formal languages and automata theory</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Formal languages and automata theory
https://arxiv.org/abs/2106.07233 Supported by the NWO TOP project 612.001.852

###### Acknowledgements.

The author thanks Stefan Milius and Jurriaan Rot for inspiring discussions and
thanks the referees for their helpful comments. Fabio Gadducci and Alexandra
Silva 2 9th Conference on Algebra and Coalgebra in Computer Science (CALCO
2021) CALCO 2021 CALCO 2021 August 31–September 3, 2021 Salzburg, Austria 211
24

# Minimality Notions via Factorization Systems

Thorsten Wißmann

###### Abstract

For the minimization of state-based systems (i.e. the reduction of the number
of states while retaining the system’s semantics), there are two obvious
aspects: removing unnecessary states of the system and merging redundant
states in the system. In the present article, we relate the two aspects on
coalgebras by defining an abstract notion of minimality.

The abstract notion minimality and minimization live in a general category
with a factorization system. We will find criteria on the category that ensure
uniqueness, existence, and functoriality of the minimization aspects. The
proofs of these results instantiate to those for reachability and
observability minimization in the standard coalgebra literature. Finally, we
will see how the two aspects of minimization interact and under which criteria
they can be sequenced in any order, like in automata minimization.

###### keywords:

Coalgebra, Reachability, Observability, Minimization, Factorization System

###### category:

(Co)algebraic pearls Full Version

##  1 Introduction

Minimization is a standard task in computer science that comes in different
aspects and lead to various algorithmic challenges. The task is to reduce the
size of a given system while retaining its semantics, and in general there are
two aspects of making the system smaller: 1. merge redundant parts of the
system that exhibit the same behaviour (_observability_) and 2. omit
unnecessary parts (_reachability_). Hopcroft’s automata minimization algorithm
[21] is an early example: in a given deterministic automaton, 1. states
accepting the same language are identified and 2\. unreachable states are
removed. Moreover, Hopcroft’s algorithm runs in quasilinear time; for an
automaton with $n$ states, reachability is computed in $\mathcal{O}(n)$ and
observability in $\mathcal{O}(n\log n)$.

Since the reachability is a simple depth-first search, it is straightforward
to apply it to other system types. On the other hand, it took decades until
quasilinear minimization algorithms for observability were developed for other
system types such as transition systems [29], labelled transition systems [14,
34], or Markov chains [12, 35]. Though their differences in complexity, the
aspects of observability and reachability have very much in common when
modelling state-based systems as coalgebras. Then, observability is the task
to find the greatest coalgebra quotient and reachability is the task of
finding the smallest subcoalgebra containing the initial state, or generally,
a distinguished point of interest.

In the present article, we define an abstract notion of minimality and
minimization in a category with an $(\mathcal{E},\mathcal{M})$-factorization
system. Such a factorization systems gives rise to a generalized notion of
quotients and subobjects, and the minimization is the task of finding the
least quotient resp. subobject. To make this general setting applicable to
coalgebras, we show that the category of coalgebras inherits the factorization
system from the base category under a mild assumption (namely that the functor
preserves $\mathcal{M}$). Dually, a factorization system also lifts to
algebras, and even to the Eilenberg-Moore category.

Then, we will present different characterizations of minimality (Figure 4) and
then study properties of minimizations, e.g. under which criteria they exist
and are unique, rediscovering the respective proofs for reachability and
observability for coalgebras in the literature [4, 22]. When combining the two
minimization aspects, we discuss under which criteria reachability and
observability can be computed in arbitrary order.

The goal of the present work is not only to show the connections between
existing minimality notions, but also to provide a series of basic results
that can be used when developing new minimization techniques or even new
notions of minimality.

##### Related Work

There is a series of works [10, 9, 11, 30] that studies the minimization of
coalgebras by their duality to algebras. In those works, the correspondence
between observability in coalgebras and reachability in algebras is used. For
instance, Rot [30] relates the final sequence (for observability in
coalgebras) with the initial sequence (for reachability in algebras). In the
present paper however, we consider both observability and reachability on an
abstract level that work for a general factorization system and discuss their
instance in coalgebras. The paper is based on Chapter 7 of the author’s PhD
dissertation [38].

If not included in the main text, detailed proofs of all results can be found
in the appendix, both for the standard results recalled in the preliminaries
and the new results of the main sections.

##  2 Preliminaries

In the following, we assume basic knowledge of category theory (cf. standard
textbooks [2, 5]).

Given a diagram $D\colon\mathcal{D}\to\mathcal{C}$ (i.e. a functor $D$ from a
small category $\mathcal{D}$), we denote its limit by $\lim D$ and colimit by
$\operatorname{colim}D$ – if they exist. The limit projections, resp. colimit
injections, are denoted by

$\mathsf{pr}_{i}\colon\lim D\to Di\qquad\mathsf{inj}_{i}\colon
Di\to\operatorname{colim}D\qquad\text{for }i\in\mathcal{D}.$

###  2.1 Coalgebra

We model state-based systems as coalgebras for an endofunctor
$F\colon\mathcal{C}\to\mathcal{C}$ on a category $\mathcal{C}$:

######  Definition 2.1.

An _$F$ -coalgebra_ (for an endofunctor $F\colon\mathcal{C}\to\mathcal{C}$) is
a pair $(C,c)$ consisting of an object $C$ (of $\mathcal{C}$) and a morphism
$c\colon C\to FC$ (in $\mathcal{C}$). An $F$-coalgebra morphism
$h\colon(C,c)\to(D,d)$ between $F$-coalgebras $(C,c)$ and $(D,d)$ is a
morphism $h\colon C\to D$ with $d\cdot h=Fh\cdot c$ (see 1(a) on p. 1(a) for
the corresponding commuting diagram).

Intuitively, the _carrier_ $C$ of a coalgebra $(C,c)$ is the state space and
the morphism $c\colon C\to FC$ sends states to their possible next states. The
functor of choice $F$ defines how these possible next states $FC$ are
structured.

######  Example 2.2.

Many well-known system-types can be phrased as coalgebras:

  * •

Deterministic automata (without an explicit initial state) are coalgebras for
the $\mathsf{Set}$-functor $FX=2\times X^{A}$, where $A$ is the set of input
symbols. In an $F$-coalgebra $(C,c)$, the first component of $c(x)$ denotes
the finality of the state $x\in C$ and the second component is the transition
function $A\to C$ of the automaton.

  * •

Labelled transition systems are coalgebras for the $\mathsf{Set}$-functor
$FX=\mathcal{P}(A\times X)$ and the coalgebra morphisms preserve bisimilarity.

  * •

Weighted systems with weights in a commutative monoid $(M,+,0)$ (and finite
branching) are coalgebras for the _monoid-valued functor_ [18, Def. 5.1]

$M^{(X)}=\\{\mu\colon X\to M\mid\mu(x)=0\text{ for all but finitely many }x\in
X\\}$

which sends a map $f\colon X\to Y$ to the map

$M^{(f)}\colon M^{(X)}\to M^{(Y)}\qquad M^{(f)}(\mu)(y)=\sum\\{\mu(x)\mid x\in
X,f(x)=y\\}$

In an $M^{(-)}$-coalgebra $(C,c)$, the transition weight from state $x\in C$
to $y\in C$ is given by $c(x)(y)\in M$. E.g. one obtains real-valued weighted
systems as coalgebras for the functor $(\mathbb{R},+,0)^{(-)}$.

  * •

The _bag_ functor is defined by $\mathcal{B}X=(\mathbb{N},+,0)^{(X)}$.
Equivalently, $\mathcal{B}X$ is the set of finite multisets on $X$. Its
coalgebras can be viewed as weighted systems or as transition systems in which
there can be more than one transition between two states.

  * •

A wide range of probabilistic and weighted systems can be obtained as
coalgebras for respective distribution functors, see e.g. Bartels et al. [8].

######  Definition 2.3.

The category of $F$-coalgebras and their morphisms is denoted by
$\mathsf{Coalg}(F)$.

Intuitively, the coalgebra morphisms preserve the behaviour of states:

######  Definition 2.4.

In $\mathsf{Set}$, two states $x,y\in C$ in an $F$-coalgebra $(C,c)$ are
_behaviourally equivalent_ if there is a coalgebra homomorphism
$h\colon(C,c)\to(D,d)$ with $h(x)=h(y)$.

######  Example 2.5.

  * •

For deterministic automata ($FX=2\times X^{A}$), states are behaviourally
equivalent iff they accept the same language [31, Example 9.5]. Indeed, for
sufficiency, if two states $x,y$ in an $F$-coalgebra are identified by a
coalgebra homomorphism, then one can show by induction over input words $w\in
A^{*}$ that either both states or neither of them accepts $w$. For necessity,
note that the map sending states to their semantics $C\to\mathcal{P}(A^{*})$
is a coalgebra homomorphism.

  * •

For labelled transition systems ($FX=\mathcal{P}(A\times X)$), states are
behaviourally equivalent iff they are bisimilar [1].

  * •

For weighted systems, i.e. coalgebras for $M^{(-)}$, the coalgebraic
behavioural equivalence captures weighted bisimilarity [23].

  * •

Further semantic notions can be modelled with coalgebras by changing the base
category from $\mathcal{C}=\mathsf{Set}$ to the Eilenberg-Moore [33] or
Kleisli category [20] of a monad, to nominal sets [26, 28], or to partially
ordered sets [6].

The category of coalgebras inherits many properties from the base-category
$\mathcal{C}$. For instance, we have the following standard result:

######  Corollary 2.6.

The forgetful functor $\mathsf{Coalg}(F)\to\mathcal{C}$ creates all colimits.
That is, the colimit of a diagram $D\colon\mathcal{D}\to\mathsf{Coalg}(F)$
exists, if $U\cdot D\colon\mathcal{D}\to\mathcal{C}$ has a colimit, and
moreover, there is a unique coalgebra structure on $\operatorname{colim}(UD)$
making it the colimit of $D$ and making the colimit injections of
$\operatorname{colim}D$ coalgebra morphisms.

On the other hand, we do not necessarily have all limits in
$\mathsf{Coalg}(F)$. If $F$ preserves a limit of a diagram
$D\colon\mathcal{D}\to\mathcal{C}$, then the limit also exists in
$\mathsf{Coalg}(F)$.

Coalgebras model systems with a transition structure, and pointed coalgebras
extend this by a notion of initial state:

######  Definition 2.7.

For an object $I\in\mathcal{C}$, an $I$-_pointed_ $F$-coalgebra $(C,c,i_{C})$
is an $F$-coalgebra $(C,c)$ together with a morphism $i_{C}\colon I\to C$. A
pointed coalgebra morphism $h\colon(C,c,i_{C})\to(D,d,i_{D})$ is a coalgebra
morphism $h\colon(C,c)\to(D,d)$ that preserves the point: $i_{D}=h\cdot
i_{C}$.

The category of $I$-pointed $F$-coalgebras is denoted by
$\mathsf{Coalg}_{I}(F)$.

######  Example 2.8.

For $I:=1$ in $\mathsf{Set}$, a pointed coalgebra $(C,c,i_{C})$ for
$FX=2\times X^{A}$ is a deterministic automaton, where the initial state is
given by the map $i_{C}\colon 1\to C$.

The point can also be understood as an algebraic flavour. In general,
coalgebras are dual to $F$-algebras in the following sense.

######  Definition 2.9.

An $F$-algebra (for a functor $F\colon\mathcal{C}\to\mathcal{C}$) is a
morphism $a\colon FA\to A$, an algebra homomorphism $h\colon(A,a)\to(B,b)$ is
a morphism $h\colon A\to B$ fulfilling $b\cdot Fh=h\cdot a$ (1(b)). The
category of $F$-algebras is denoted by $\mathsf{Alg}(F)$.

In other words,
$\mathsf{Alg}(F)=\mathsf{Coalg}(F^{\operatorname{\mathsf{op}}})^{\operatorname{\mathsf{op}}}$
for
$F^{\operatorname{\mathsf{op}}}\colon\mathcal{C}^{\operatorname{\mathsf{op}}}\to\mathcal{C}^{\operatorname{\mathsf{op}}}$.
The $I$-pointed coalgebras thus are also algebras for the constant $I$
functor. Most of the results of the present paper also apply to algebras for a
functor $F\colon\mathcal{C}\to\mathcal{C}$.

###  2.2 Factorization Systems

The process of minimizing a system constructs a quotient or subobject of the
state space, where the notions of quotient and subobject respectively stem
from a factorization system in the category of interest. This generalizes the
well-known image factorization of a map into a surjective and an injective
map:

${C}$${FC}$${D}$${FD}$$\scriptstyle{h}$$\scriptstyle{c}$$\scriptstyle{Fh}$$\scriptstyle{d}$
(a) $F$-Coalgebras

${FA}$${A}$${FB}$${B}$$\scriptstyle{a}$$\scriptstyle{Fh}$$\scriptstyle{h}$$\scriptstyle{b}$
(b) $F$-Algebras

Figure 1: A homomorphism between $\ldots$

${A}$${B}$${\mathsf{Im}(f)}$$\scriptstyle{e}$$\scriptstyle{f}$$\scriptstyle{m}$
(c) Factorization

${A}$${B}$${C}$${D}$$\scriptstyle{e}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{\exists!d}$$\scriptstyle{m}$
(d) Diagonal fill-in

Figure 2: Diagrams for 2.10

######  Definition 2.10 ([2, Definition 14.1]).

Given classes of morphisms $\mathcal{E}$ and $\mathcal{M}$ in $\mathcal{C}$,
we say that $\mathcal{C}$ has an _$(\mathcal{E},\mathcal{M})$ -factorization
system_ provided that:

  1. 1.

$\mathcal{E}$ and $\mathcal{M}$ are closed under composition with
isomorphisms.

  2. 2.

Every morphism $f\colon A\to B$ in $\mathcal{C}$ has a factorization $f=m\cdot
e$ with $e\in\mathcal{E}$ and $m\in\mathcal{M}$ (1(c)). We write
$\mathsf{Im}(f)$ for the intermediate object, $\twoheadrightarrow$ for
morphisms $e\in\mathcal{E}$, and $\rightarrowtail$ for morphisms
$m\in\mathcal{M}$.

  3. 3.

For each commutative square $g\cdot e=m\cdot f$ with $m\in\mathcal{M}$ and
$e\in\mathcal{E}$, there exists a unique diagonal fill-in $d$ with $m\cdot
d=g$ and $d\cdot e=f$ (1(d)).

######  Example 2.11.

In $\mathsf{Set}$, we have an $(\mathsf{Epi},\mathsf{Mono})$-factorization
system where $\mathsf{Epi}$ is the class of surjective maps, and
$\mathsf{Mono}$ the class of injective maps. The image of a map $f\colon A\to
B$ is given by

$\mathsf{Im}(f)=\\{b\in B\mid\text{there exists $a\in A$ with $f(a)=b$}\\}.$

canonically yielding maps $e\colon A\twoheadrightarrow\mathsf{Im}(f)$ and
$m\colon\mathsf{Im}(f)\rightarrowtail B$. Note that one can also regard
$\mathsf{Im}(f)$ as a set of equivalence classes of $A$:

$\mathsf{Im}(f)\cong\big{\\{}\\{a^{\prime}\in A\mid
f(a^{\prime})=f(a)\\}\,\mid a\in A\big{\\}}.$

Intuitively, the diagonal fill-in property (2.10.3, also called _diagonal
lifting_) provides a way of defining a map $d$ on equivalence classes (given
by the surjective map at the top) and with a restricted codomain (given by the
injective map at the bottom).

######  Example 2.12.

In general, the elements of $\mathcal{E}$ are not necessarily epimorphisms and
the elements of $\mathcal{M}$ are not necessarily monomorphisms. In
particular, every category has an $(\mathcal{E},\mathcal{M})$-factorization
system with $\mathcal{E}:=\mathsf{Iso}$ being the class of isomorphisms and
$\mathcal{M}:=\mathsf{Mor}$ being the class of all morphisms (and also vice-
versa).

######  Definition 2.13.

An $(\mathcal{E},\mathcal{M})$-factorization system is called _proper_ if
$\mathcal{E}\subseteq\mathsf{Epi}$ and $\mathcal{M}\subseteq\mathsf{Mono}$.

These two conditions of properness are independent. In fact,
$\mathcal{M}\subseteq\mathsf{Mono}$ is equivalent to every split-epimorphism
being in $\mathcal{E}$ [2, Prop. 14.11]. In the literature, it is often
required that the factorization system is proper, and in fact a proper
factorization system arises in complete or cocomplete categories:

######  Example 2.14.

Every complete category has a
$(\mathsf{StrongEpi},\mathsf{Mono})$-factorization system [2, Thm. 14.17 and
14C(d)] and also an $(\mathsf{Epi},\mathsf{StrongMono})$-factorization system
[2, Thm. 14.19, and 14C(f)]. By duality, every cocomplete category has so as
well.

######  Remark 2.15.

$(\mathcal{E},\mathcal{M})$-factorization systems have many properties known
from surjective and injective maps on $\mathsf{Set}$ [2, Chp. 14]:

  1. 1.

$\mathcal{E}\cap\mathcal{M}$ is the class of isomorphisms of $\mathcal{C}$.

  2. 2.

If $f\cdot g\in\mathcal{M}$ and $f\in\mathcal{M}$, then $g\in\mathcal{M}$. If
$\mathcal{M}\subseteq\mathsf{Mono}$, then $f\cdot g\in\mathcal{M}$ implies
$g\in\mathcal{M}$.

  3. 3.

$\mathcal{E}$ and $\mathcal{M}$ are respectively closed under composition.

  4. 4.

$\mathcal{M}$ is stable under pullbacks, $\mathcal{E}$ is stable under
pushouts.

The stability generalizes as follows to wide pullbacks and pushouts:

######  Lemma 2.16.

$\mathcal{M}$ is stable under wide pullbacks: for a family $(f_{i}\colon
A_{i}\to B)_{i\in I}$ and its wide pullback $(\mathsf{pr}_{i}\colon P\to
A_{i})_{i\in I}$, a projection $\mathsf{pr}_{j}\colon P\to A_{j}$ is in
$\mathcal{M}$ if $f_{i}$ is in $\mathcal{M}$ for all $i\in I\setminus\\{j\\}$.

A factorization system also provides notions of subobjects and quotients,
generalizing the notions of subset and quotient sets:

######  Definition 2.17.

For a class $\mathcal{M}$ of morphisms, an _$\mathcal{M}$ -subobject_ of an
object $X$ is a pair $(S,s)$ where $s\colon S\rightarrowtail X$ is in
$\mathcal{M}$. Two $\mathcal{M}$-subobjects $(s,S)$, $(s^{\prime},S^{\prime})$
are called _isomorphic_ if there is an isomorphism $\phi\colon S\to
S^{\prime}$ with $\phi\cdot s=s^{\prime}$. We write
$(s,S)\leq(s^{\prime},S^{\prime})$ if there is a morphism $h\colon S\to
S^{\prime}$ with $s^{\prime}\cdot h=s$. Dually, an _$\mathcal{E}$ -quotient_
of $X$ is pair $(Q,q)$ for a morphism $q\colon X\twoheadrightarrow Q$
($q\in\mathcal{E}$). If $(\mathcal{E},\mathcal{M})$ is fixed from the context,
we simply speak of subobjects and quotients.

For subobjects, it is often required that $\mathcal{M}$ is a class of
monomorphisms [2, Def. 7.77], but many of the results in the present work hold
without this assumption. If $\mathcal{M}$ is so, then the subobjects of a
given object $X$ form a preordered class. Moreover, the subobjects form a
preordered set iff $\mathcal{C}$ is $\mathcal{M}$-wellpowered. This is in fact
the definition: $\mathcal{C}$ is $\mathcal{M}$-wellpowered if for each
$X\in\mathcal{C}$ there is (up to isomorphism) only a set of
$\mathcal{M}$-subobjects. On $\mathsf{Set}$, the isomorphism classes of
($\mathsf{Mono}$-)subobjects of $X$ correspond to subsets of $X$ and the
isomorphism classes of ($\mathsf{Epi}$-)quotients of $X$ correspond to
partitions on $X$.

If $(\mathcal{E},\mathcal{M})$ forms a factorization system, then its axioms
provide us with methods to construct and work with subobjects and quotients,
e.g. the image factorization means that for every morphism, we obtain a
quotient on its domain and a subobject of its codomain. The minimization of
coalgebras amounts to the construction of certain subobjects or quotients with
respect to a suitable factorization system in the category of coalgebras
$\mathsf{Coalg}(F)$.

##  3 Factorization System for Coalgebras

If we have an $(\mathcal{E},\mathcal{M})$-factorization system on the base
category $\mathcal{C}$ on which we consider coalgebras for
$F\colon\mathcal{C}\to\mathcal{C}$, then it is natural to consider coalgebra
morphisms whose underlying $\mathcal{C}$-morphism is in $\mathcal{E}$, resp.
$\mathcal{M}$:

######  Definition 3.1.

Given a class of $\mathcal{C}$-morphisms $\mathcal{E}$, we say that an
$F$-coalgebra morphism $h\colon(C,c)\to(D,d)$ is _$\mathcal{E}$ -carried_ if
$h\colon C\to D$ is in $\mathcal{E}$.

This induces the standard notions of subcoalgebra and quotient coalgebras as
instances of $\mathcal{M}$-subobjects and $\mathcal{E}$-quotients in
$\mathsf{Coalg}(F)$: an $\mathcal{M}$-subcoalgebra of $(C,c)$ is an
($\mathcal{M}$-carried)-subobject of $(C,c)$ (in $\mathsf{Coalg}(F)$), i.e. is
represented by an $\mathcal{M}$-carried homomorphism
$m\colon(S,s)\rightarrowtail(C,c)$. Likewise, a _quotient_ of a coalgebra
$(C,c)$ is an ($\mathcal{E}$-carried)-quotient of $(C,c)$ (in
$\mathsf{Coalg}(F)$), i.e. is represented by a coalgebra morphism
$e\colon(C,c)\twoheadrightarrow(Q,q)$ carried by an epimorphism.

Note that for the case where $\mathcal{M}$ is the class of monomorphisms, the
monomorphisms in $\mathsf{Coalg}(F)$ coincide with the $\mathsf{Mono}$-carried
homomorphisms only under additional assumptions:

######  Lemma 3.2.

If weak kernel pairs exist in $\mathcal{C}$ and are preserved by
$F\colon\mathcal{C}\to\mathcal{C}$, then the monomorphisms in
$\mathsf{Coalg}(F)$ are precisely the $\mathsf{Mono}$-carried coalgebra
homomorphisms.

This is a commonly known criterion, and Gumm and Schröder [19, Example 3.5]
present a functor not preserving kernel pairs and a monic coalgebra
homomorphism that is not carried by a monomorphism.

For the construction of quotient coalgebras and subcoalgebras, it is handy to
have the factorization system directly in $\mathsf{Coalg}(F)$. It is a
standard result that the image factorization of homomorphisms lifts (see e.g.
[27, Lemma 2.5]). Under assumptions on $\mathcal{E}$ and $\mathcal{M}$, Kurz
shows that the factorization system lifts to $\mathsf{Coalg}$(F) [25, Theorem
1.3.7] (and to other categories with a forgetful functor to the base category
$\mathcal{C}$).

In fact, the factorization system always lifts to $\mathsf{Coalg}(F)$ under
the condition that $F$ preserves $\mathcal{M}$. By this condition, we mean
that $m\in\mathcal{M}$ implies $Fm\in\mathcal{M}$.

######  Lemma 3.3.

If $F\colon\mathcal{C}\to\mathcal{C}$ preserves $\mathcal{M}$, then the
$(\mathcal{E},\mathcal{M})$-factorization system lifts from $\mathcal{C}$ to
an ($\mathcal{E}$-carried, $\mathcal{M}$-carried)-factorization system in
$\mathsf{Coalg}(F)$. The factorization of an $F$-coalgebra homomorphism
$h\colon(C,c)\to(D,d)$ is given by that of the underlying morphism $h\colon
C\to D$.

######  Proof 3.4.

We verify 2.10:

  1. 1.

The $\mathcal{E}$\- and $\mathcal{M}$-carried morphisms are closed under
composition with isomorphisms, respectively.

  2. 2.

Given an $F$-coalgebra morphism $f\colon(A,a)\to(B,b)$, consider its
factorization $f=m\cdot e$ in $\mathcal{C}$. Since $F$ preserves
$\mathcal{M}$, we have $Fm\in\mathcal{M}$ and thus can apply the diagonal
fill-in property (2.10.3) to the coalgebra morphism square of $f$ (3(a)). This
defines a unique coalgebra structure $d$ on $\mathsf{Im}(f)$ making $e$ and
$m$ coalgebra morphisms.

${A}$${\mathsf{Im}(f)}$${B}$${FA}$${F\mathsf{Im}(f)}$${FB}$$\scriptstyle{f}$$\scriptstyle{e}$$\scriptstyle{a}$$\scriptstyle{m}$$\scriptstyle{\exists!d}$$\scriptstyle{b}$$\scriptstyle{Fe}$$\scriptstyle{Ff}$$\scriptstyle{Fm}$
(a) Factorization

${(A,a)}$${(B,b)}$${(C,c)}$${(D,d)}$$\scriptstyle{e}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{m}$
(b) Premise in $\mathsf{Coalg}(F)$

${A}$${B}$${C}$${D}$$\scriptstyle{e}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{\exists!h}$$\scriptstyle{m}$
(c) Fill-in in $\mathcal{C}$

Figure 3: Diagrams for the proof of 3.3

  3. 3.

In order to check the diagonal-lifting property of the ($\mathcal{E}$-carried,
$\mathcal{M}$-carried)-factorization system, consider a commutative square
$g\cdot e=m\cdot f$ in $\mathsf{Coalg}(F)$ with $m\in\mathcal{M}$,
$e\in\mathcal{E}$ as depicted in 3(b). In $\mathcal{C}$, there exists a unique
$h\colon B\to C$ with $h\cdot e=f$ and $m\cdot h=g$ (3(c)). We only need to
prove that $h\colon B\to C$ is a coalgebra homomorphism $(B,b)\to(C,c)$, i.e.
that $c\cdot h=Fh\cdot b$. We prove this equality by showing that both $c\cdot
h$ and $Fh\cdot b$ are diagonals in a commutative square of the form of
2.10.3. Indeed, we have the commutative squares:

${A}$${B}$${FA}$${C}$${D}$${FB}$${FC}$${FD}$$\scriptstyle{a}$$\scriptstyle{f}$$\scriptstyle{e}$$\scriptstyle{h}$$\scriptstyle{g}$$\scriptstyle{b}$$\scriptstyle{Ff}$
f hom. $\scriptstyle{m}$$\scriptstyle{c}$ m hom. g hom.
$\scriptstyle{d}$$\scriptstyle{Fg}$$\scriptstyle{Fm}$ and
${A}$${B}$${FA}$${FB}$${FB}$${FC}$${Fm}$$\scriptstyle{e}$$\scriptstyle{a}$ e
hom.
$\scriptstyle{b}$$\scriptstyle{b}$$\scriptstyle{Ff}$$\scriptstyle{Fe}$$\scriptstyle{Fh}$$\scriptstyle{Fg}$
trivial $\scriptstyle{Fg}$$\scriptstyle{Fm}$

By the uniqueness of the diagonal in 2.10.3, $c\cdot h=Fh\cdot b$.

######  Remark 3.5.

The condition that $F$ preserves $\mathcal{M}$ is commonly met. For
$\mathsf{Set}$ and $\mathcal{M}$ being the class of injective maps, it can be
assumed wlog for coalgebraic purposes that $F$ preserves injective maps: every
set functor preserves injective maps with non-empty domain and only needs to
be modified on $\emptyset$ in order to preserve all injective maps [32]. The
resulting functor has an isomorphic category of coalgebras.

We have the dual result for $F$-algebras:

######  Lemma 3.6.

If $F\colon\mathcal{C}\to\mathcal{C}$ preserves $\mathcal{E}$, then the
$(\mathcal{E},\mathcal{M})$-factorization system lifts from $\mathcal{C}$ to
$\mathsf{Alg}(F)$.

######  Proof 3.7.

We have an $(\mathcal{M},\mathcal{E})$-factorization system in
$\mathcal{C}^{\operatorname{\mathsf{op}}}$. By 3.3, this factorization system
lifts to $\mathsf{Coalg}(F^{\operatorname{\mathsf{op}}})$ since
$F^{\operatorname{\mathsf{op}}}\colon\mathcal{C}^{\operatorname{\mathsf{op}}}\to\mathcal{C}^{\operatorname{\mathsf{op}}}$
preserves $\mathcal{E}$. Thus, we have an ($\mathcal{E}$-carried,
$\mathcal{M}$-carried)-factorization system in
$\mathsf{Alg}(F)=\mathsf{Coalg}(F^{\operatorname{\mathsf{op}}})^{\operatorname{\mathsf{op}}}$.

This lifting result even holds for Eilenberg-Moore algebras for a monad
$T\colon\mathcal{C}\to\mathcal{C}$. The Eilenberg-Moore category of a monad
$T$ is a full subcategory of $\mathsf{Alg}(T)$ containing those algebras that
interact coherently with the structure of the monad $T$, see e.g. Awodey [5]
for details:

######  Lemma 3.8.

If a monad $T\colon\mathcal{C}\to\mathcal{C}$ preserves $\mathcal{E}$, then
the $(\mathcal{E},\mathcal{M})$-factorization system lifts from $\mathcal{C}$
to the Eilenberg-Moore category of $T$.

The factorization system lifts further also to pointed coalgebras:

######  Lemma 3.9.

If $F\colon\mathcal{C}\to\mathcal{C}$ preserves $\mathcal{M}$, then the
$(\mathcal{E},\mathcal{M})$-factorization system lifts from $\mathcal{C}$ to
$\mathsf{Coalg}_{I}(F)$.

######  Proof 3.10.

A combination of 3.3 and 3.6, using that the constant functor preserves
$\mathcal{E}$-morphisms.

##  4 Minimality in a Category

Having seen multiple categories with an
$(\mathcal{E},\mathcal{M})$-factorization system, we can now define the
minimality of objects abstractly.

######  Definition 4.1.

Given a category $\mathcal{K}$ with an
$(\mathcal{E},\mathcal{M})$-factorization system, an object $C$ of
$\mathcal{K}$ is called _$\mathcal{M}$ -minimal_ if every morphism $h\colon
D\rightarrowtail C$ in $\mathcal{M}$ is an isomorphism.

######  Remark 4.2.

Every $(\mathcal{E},\mathcal{M}$)-factorization system on $\mathcal{K}$ is an
$(\mathcal{M},\mathcal{E})$-factorization system on
$\mathcal{K}^{\operatorname{\mathsf{op}}}$, and thus induces a dual notion of
$\mathcal{E}$-minimality: an object $C$ of $\mathcal{K}$ is called
_$\mathcal{E}$ -minimal_ if every $h\colon C\twoheadrightarrow D$ in
$\mathcal{E}$ is an isomorphism.

In the following, $\mathcal{K}$ will denote the category in which we consider
the minimal objects, e.g. a category of coalgebras for a functor
$F\colon\mathcal{C}\to\mathcal{C}$.

######  Assumption 4.3.

In the following, assume that the category $\mathcal{K}$ has an
$(\mathcal{E},\mathcal{M})$-factorization system. Whenever we consider a
category of coalgebras for a functor $F\colon\mathcal{C}\to\mathcal{C}$ in the
following, we achieve this by assuming that $\mathcal{C}$ has an
$(\mathcal{E},\mathcal{M})$-factorization system and that $F$ preserves
$\mathcal{M}$.

The leading examples of the minimality notion in the present work are the
following two instances in coalgebras:

######  Instance 4.4.

For $\mathcal{K}:=\mathsf{Coalg}_{I}(F)$, the ($\mathcal{M}$-carried-)minimal
objects are the _reachable_ coalgebras, as introduced by Adámek et al. [4].
Concretely, an $I$-pointed $F$-coalgebra $(C,c,i_{C})$ is reachable if it has
no (proper) pointed subcoalgebra, equivalently, if every $\mathcal{M}$-carried
coalgebra morphism $m\colon(S,s,i_{S})\rightarrowtail(C,c,i_{C})$ is
necessarily an isomorphism [4].

In $\mathsf{Set}$, this corresponds to the usual notion of reachability: if a
state $x\in C$ is contained in a subcoalgebra
$m\colon(S,s,i_{S})\rightarrowtail(C,c,i_{C})$, then all successors of $x$
need to be contained in the subcoalgebra as well, since $m$ is a coalgebra
homomorphism. Moreover, the subcoalgebra has to contain the point $i_{C}\colon
I\to C$, and thus also all its successors, and in total all states reachable
from $i_{C}$ in finitely many steps. Hence, $(C,c,i_{C})$ is reachable if it
is not possible to omit any state in a pointed subcoalgebra $(S,s,i_{S})$,
i.e. if any such injective $m$ is a bijection.

######  Instance 4.5.

For $\mathcal{K}:=\mathsf{Coalg}(F)^{\operatorname{\mathsf{op}}}$, the
($\mathcal{E}$-carried-)minimal objects are called _simple_ coalgebras, as
mentioned by Gumm [22]. Usually, a simple coalgebra is defined as a coalgebra
that does not have any proper quotient [36].111Gumm [22, p. 34] defines a
simple coalgebra as the quotient of a coalgebra on $\mathsf{Set}$ modulo
behavioural equivalence.

In $\mathsf{Set}$, a coalgebra is simple iff all states have different
behaviour – this characterization follows directly the following equivalent
characterization of minimal objects as we will see in 4.8:

######  Lemma 4.6.

An object $C$ in $\mathcal{K}$ is $\mathcal{M}$-minimal iff every $h\colon
D\to C$ is in $\mathcal{E}$.

######  Proof 4.7.

In the ‘if’ direction, consider some $\mathcal{M}$-morphism $h\colon D\to C$.
By the assumption, $h$ is also in $\mathcal{E}$ and thus an isomorphism. In
the ‘only if’ direction, take some morphism $h\colon D\to C$ and consider its
$(\mathcal{E},\mathcal{M})$-factorization $e\colon
D\twoheadrightarrow\mathsf{Im}(h)$ and $m\colon\mathsf{Im}(h)\rightarrowtail
C$ with $h=m\cdot e$. Since $C$ is $\mathcal{M}$-minimal, $m$ is an
isomorphism and thus $h=m\cdot e$ is in $\mathcal{E}$.

######  Instance 4.8.

For $\mathcal{K}:=\mathsf{Coalg}(F)^{\operatorname{\mathsf{op}}}$, an
$F$-coalgebra $(C,c)$ is simple iff every $F$-coalgebra homomorphism
$h\colon(C,c)\to(D,d)$ is $\mathcal{M}$-carried.

In $\mathsf{Set}$, this equivalence shows that the simple coalgebras are
precisely those coalgebras for which behavioural equivalence coincides with
behavioural equivalence:

  * •

If states $x,y\in C$ are behaviourally equivalent, then there is some
$h\colon(C,c)\to(D,d)$ with $h(x)=h(y)$. By 4.8, $h$ must be injective and
thus $x=y$.

  * •

Conversely, if all states in $(C,c)$ have different behaviour, then every
$h\colon(C,c)\to(D,d)$ is necessarily injective by 2.4. Thus, by 4.8, $(C,c)$
is simple.

Gumm already noted that in $\mathsf{Set}$, every outgoing coalgebra morphism
from a simple coalgebra is injective [22, Hilfssatz 3.6.3] – but it was not
used to characterize simplicity. If $\mathcal{E}$, resp. $\mathcal{M}$,
happens to be the class of epimorphisms, resp. monomorphisms, another
characterization of minimality exists:

######  Lemma 4.9.

Assume $\mathcal{E}=\mathsf{Epi}$ and weak equalizers in $\mathcal{K}$, then
$X$ is $\mathcal{M}$-minimal iff there is at most one morphism $u\colon C\to
D$ for every $D\in\mathcal{K}$.

Dually, given $\mathcal{M}=\mathsf{Mono}$ and weak coequalizers, $C$ is
$\mathcal{E}$-minimal iff $C$ is _subterminal_ , that is, iff there is a most
one $u\colon D\to C$ for every $D\in\mathcal{K}$.

The name _subterminal_ stems from the fact that if $\mathcal{K}$ has a
terminal object, its subobjects are the subterminal objects.

######  Instance 4.10.

For $\mathcal{K}:=\mathsf{Coalg}(F)^{\operatorname{\mathsf{op}}}$, assume
$\mathcal{M}=\mathsf{Mono}$ and that $F$ preserves weak kernel pairs and that
the base category $\mathcal{C}$ has coequalizers. Hence, the monomorphisms in
$\mathsf{Coalg}(F)$ are precisely the $\mathsf{Mono}$-carried homomorphisms
(3.2) and the assumption of 4.9 is met. Consequently, the simple coalgebras
are precisely the _subterminal_ coalgebras. If the final coalgebra exists,
then its subcoalgebras are precisely the simple coalgebras. For a non-example,
Gumm and Schröder [19, Example 3.5] provide a functor not preserving weak
kernel pairs and a subterminal coalgebra that is not simple.

$X$ is $\mathcal{M}$-minimal |  |  $X$ is $\mathcal{E}$-minimal
---|---|---
$\Leftrightarrow$ | every $Y\rightarrowtail X$ is an isomorphism |  | $\Leftrightarrow$ | every $X\twoheadrightarrow Y$ is an isomorphism
$\Leftrightarrow$ | every $Y\to X$ is in $\mathcal{E}$ |  | $\Leftrightarrow$ | every $X\to Y$ is in $\mathcal{M}$
|  if $\mathcal{E}=\mathsf{Epi}$ and $\mathcal{K}$ has weak equalizers: |  |  |  if $\mathcal{M}=\mathsf{Mono}$ and $\mathcal{K}$ has weak coequalizers:
$\Leftrightarrow$ | all parallel $X\rightrightarrows Y$ equal |  | $\Leftrightarrow$ | all parallel $Y\rightrightarrows X$ equal (‘X subterminal’)
Figure 4: Equivalent characterizations of $\mathcal{M}$-minimality and
$\mathcal{E}$-minimality in a category $\mathcal{K}$

We have now established a series of equivalent characterizations of minimality
(Figure 4) and will now discuss how to construct minimal objects. This process
of minimization – i.e. of constructing the reachable part or the simple
quotient of a coalgebra – is abstracted as follows:

######  Definition 4.11.

An _$\mathcal{M}$ -minimization_ of $C\in\mathcal{K}$ is a morphism $m\colon
D\rightarrowtail C$ in $\mathcal{M}$ where $D$ is $\mathcal{M}$-minimal.

In fact, we will show that an $\mathcal{M}$-minimization is unique, so we can
speak of _the_ $\mathcal{M}$-minimization.

######  Instance 4.12.

The task of finding an $\mathcal{M}$-minimization of a given $C\in\mathcal{K}$
instantiates to the standard minimization tasks on coalgebras:

  * •

For $\mathcal{K}:=\mathsf{Coalg}_{I}(F)$, an $\mathcal{M}$-minimization of a
given pointed coalgebra $(C,c,i_{C})$ is called its _reachable subcoalgebra_
[4]. This is a subcoalgebra obtained by removing all unreachable states. The
explicit definition is: the reachable subcoalgebra of $(C,c,i_{C})$ is a
(pointed) subcoalgebra $h\colon(R,r,i_{R})\rightarrowtail(C,c,i_{C})$ where
$(R,r,i_{R})$ itself has no proper (pointed) subcoalgebras.

  * •

For $\mathcal{K}:=\mathsf{Coalg}(F)^{\operatorname{\mathsf{op}}}$, an
$\mathcal{E}$-minimization of a given coalgebra $(C,c)$ is called the _simple
quotient_ of $(C,c)$ [22]. The explicit definition is: the simple quotient of
$(C,c)$ is a quotient $h\colon(C,c)\twoheadrightarrow(Q,q)$ where $(Q,q)$
itself has no proper quotient coalgebra.

In $\mathsf{Set}$, this is a quotient in which all behaviourally equivalent
states are identified, in other words, the simple quotient of $(C,c)$ is the
unique coalgebra structure on $C/\mathord{\sim}$. Examples of simple quotients
can be found in Figure 5. Since all states in the codomain of the surjective
homomorphisms are behaviourally inequivalent, the respective codomains are
simple.

$\bullet$$\bullet$$\bullet$

$\bullet$$\bullet$

(a) For $FX=\mathcal{P}X$

$\bullet$$\bullet$$\bullet$4-755

$\bullet$$\bullet$-35

(b) For $FX=(\mathbb{R},+,0)^{(X)}$

Figure 5: Examples of simple quotients in $F$-coalgebras

######  Example 4.13.

For the trivial factorization systems (2.12), we have:

  * •

For the $(\mathsf{Iso},\mathsf{Mor})$-factorization system, the
$\mathsf{Iso}$-minimization of an object $X$ is $X$ itself.

  * •

For the $(\mathsf{Mor},\mathsf{Iso})$-factorization system on category, if a
strict initial object $0$ exist, then it is the $\mathsf{Mor}$-minimization of
every $X\in\mathcal{C}$. Recall that an initial object $0$ is called _strict_
if every morphism with codomain $0$ is an isomorphism.

It is well-defined to speak of _the_ $\mathcal{M}$-minimization of an object
$C$, because it is unique:

######  Lemma 4.14.

Consider $h\colon M\to C$ with $\mathcal{M}$-minimal $M$ and an
$\mathcal{M}$-subobject $s\colon S\rightarrowtail C$. The pullback of $s$
along $h$ exists iff $h$ factors uniquely through $s$, that is, iff there is a
unique $u\colon M\to S$ with $s\cdot u=h$.

${C}$${M}$${S}$$\scriptstyle{h}$$\scriptstyle{\exists!u}$$\scriptstyle{\forall
s\in\mathcal{M}}$ (in $\mathcal{K}$)
${C}$${M}$${Q}$$\scriptstyle{h}$$\scriptstyle{\exists!u}$$\scriptstyle{\forall
q\in\mathcal{E}}$ (in $\mathcal{K}^{\operatorname{\mathsf{op}}}$)

######  Proof 4.15.

In the ‘if’-direction, let $d\colon M\to S$ be the unique morphism with
$s\cdot d=h$. The pullback is simply given by $M$ itself with projections
$\mathsf{id}_{M}\colon M\to M$ and $d\colon M\to S$. To verify its universal
property, consider $e\colon E\to M$, $f\colon E\to S$ with $h\cdot e=s\cdot f$
(6(a)). Since $M$ is $\mathcal{M}$-minimal, $e\colon E\to M$ is in
$\mathcal{E}$ (4.6). Thus, we can apply the diagonal lifting property to
$h\cdot e=s\cdot f$ yielding a diagonal $u$ with $s\cdot u=h$ and $u\cdot
e=f$. Thus, $d=u$ and $d\cdot e=f$, showing that
$e\colon(E,e,f)\to(M,\mathsf{id}_{M},d)$ is the mediating cone morphism. Its
uniqueness is clear because $\mathsf{id}_{M}$ is isomorphic.

${M}$${C}$${E}$${S}$$\scriptstyle{h}$$\scriptstyle{u}$$\scriptstyle{e}$$\scriptstyle{f}$$\scriptstyle{s}$
(a) ‘If’-direction

${P}$${M}$${S}$${C}$$\scriptstyle{\phi}$$\scriptstyle{d}$$\scriptstyle{h}$$\scriptstyle{s}$
(b) Premise of ‘only if’

${M}$${P}$${M}$${S}$${C}$$\scriptstyle{\mathsf{id}_{M}}$$\scriptstyle{v}$$\scriptstyle{u}$$\scriptstyle{\phi}$$\scriptstyle{d}$$\scriptstyle{h}$$\scriptstyle{s}$
(c) Uniqueness for ‘only if’

Figure 6: Diagrams for the proof of 4.14

In the ‘only if’-direction, consider the pullback $(P,\phi,d)$ (6(b)). Since
$\mathcal{M}$-morphisms are stable under pullback (2.15.4), $\phi$ is in
$\mathcal{M}$, too. By the minimality of $M$, the $\mathcal{M}$-morphism
$\phi$ is an isomorphism and we have $d\cdot\phi^{-1}\colon M\to S$.

In order to see that $d\cdot\phi^{-1}$ is indeed the unique morphism $M\to S$
making the triangle commute, consider an arbitrary $v\colon M\to S$ with
$s\cdot v=h=h\cdot\mathsf{id}_{M}$. Thus, $M$ is a competing cone for the
pullback $P$ and thus induces a morphism $u\colon M\to P$ with $d\cdot u=v$
and $\phi\cdot u=\mathsf{id}_{M}$ (6(c)). Since $\phi$ is an isomorphism, we
have $u=\phi^{-1}$ and thus $v=d\cdot\phi^{-1}$ as desired.

######  Corollary 4.16.

If $\mathcal{K}$ has pullbacks of $\mathcal{M}$-morphisms along
$\mathcal{M}$-morphisms and if there is an $\mathcal{M}$-minimization $M$ of
$C$, then $M$ is the least $\mathcal{M}$-subobject of $C$ and it is unique (up
to unique isomorphism).

######  Proof 4.17.

Consider 4.14 first for $h\in\mathcal{M}$ and then also with $S$ being
$\mathcal{M}$-minimal.

######  Instance 4.18.

Not only the result but also the proof instantiates to the uniqueness results
in the instances of reachable subcoalgebras and simple quotients:

  1. 1.

If $\mathcal{C}$ has pullbacks of $\mathcal{M}$-morphisms (i.e. finite
intersections) and $F\colon\mathcal{C}\to\mathcal{C}$ preserves them, then
$\mathsf{Coalg}_{I}(F)$ has pullbacks of $\mathcal{M}$-carried homomorphisms.
Given a reachable subcoalgebra $(D,d,i_{D})$ of $(C,c,i_{C})$, then it is the
least $I$-pointed subcoalgebra of $(C,c,i_{C})$ (cf. [4, Notation 3.18]) and
is unique up to isomorphism.

  2. 2.

If $\mathcal{C}$ has pushouts of $\mathcal{E}$-morphisms, then
$\mathsf{Coalg}(F)$ has pushouts of $\mathcal{E}$-carried homomorphisms.
Hence, the simple quotient of a coalgebra $(C,c)$ is the greatest quotient of
$(C,c)$ and unique up to isomorphism (e.g. [36, Lemma 2.9]).

There are instances where a minimization $M$ exists, but where a mediating
morphism in the sense of 4.14 is not unique:

######  Example 4.19 (Tree unravelling).

Let $\mathsf{Coalg}_{I}(F)_{\mathsf{reach}}$ be the category of reachable
pointed $F$-coalgebras, i.e. the full subcategory
$\mathsf{Coalg}_{I}(F)_{\mathsf{reach}}\subseteq\mathsf{Coalg}_{I}(F)$ such
that $(C,c,i_{C})\in\mathsf{Coalg}_{I}(F)_{\mathsf{reach}}$ iff it is
reachable. For simplicity, restrict to $F\colon\mathsf{Set}\to\mathsf{Set}$
with the $(\mathsf{Epi},\mathsf{Mono})$-factorization system. Thus, all
morphisms in $\mathsf{Coalg}_{I}(F)_{\mathsf{reach}}$ are surjective (4.6).
Considering the (trivial) $(\mathsf{Mor},\mathsf{Iso})$-factorization system
on $\mathsf{Coalg}_{I}(F)_{\mathsf{reach}}$, a coalgebra $(C,c,i_{C})$ is
($\mathsf{Mor}$-)minimal iff every coalgebra morphism
$h\colon(D,d,i_{D})\to(C,c,i_{C})$ (with $(D,d,i_{D})$ also reachable) is an
isomorphism. If $(C,c,i_{C})$ is $\mathsf{Mor}$-minimal, then it is a tree: to
see this, take $h$ to be its tree unravelling (see e.g. Figure 7), and by the
$\mathsf{Mor}$-minimality, $h$ is an isomorphism, so $(C,c,i_{C})$ is already
a tree.

This implies that if the ($\mathsf{Mor}$-)minimization of a coalgebra exists,
then it is its tree unravelling. For example, for $I=1$ and the bag functor
$FX=\mathcal{B}X$, we have the minimizations as illustrated in Figure 7. It is
easy to see that for $FX=\mathcal{P}X$ however, no coalgebra (with at least
one transition) has a $\mathsf{Mor}$-minimization, because one can always
duplicate successor states.222It can be conjectured that
$\mathsf{Mor}$-minimization of reachable $F$-coalgebras exist if $F$ admits
precise factorizations [37, Def. 3.1, 3.4].

For $FX=\mathcal{B}X$, all $\mathsf{Mor}$-minimizations exist, but they are
not unique up to unique isomorphism. Consider the tree unravelling $m\colon
M\twoheadrightarrow X$ in 7(a). There is an isomorphism $\phi\colon M\to M$
that swaps the two successors of the initial state. Hence,
$\phi\neq\mathsf{id}_{B}$, but $m\cdot\phi=m\cdot\mathsf{id}_{M}$, so $M$ is
unique up to isomorphism, but not unique up to unique isomorphism.

$\bullet$$\bullet$$\bullet$

$\bullet$$\bullet$

(a) Unravelling of siblings

$\bullet$$\bullet$$\cdots$

$\bullet$

(b) Unravelling of a loop

Figure 7: Tree unravelling for $FX=\mathcal{B}X$

For proving the existence of an $\mathcal{M}$-minimization, we need to require
that $\mathcal{M}$ is a subclass of the monomorphisms in $\mathcal{K}$. Under
this assumption, we first establish the converse of 4.16:

######  Lemma 4.20.

If $\mathcal{M}\subseteq\mathsf{Mono}$ and if the least
$\mathcal{M}$-subobject $M$ of $X$ exists, then $M$ is the
$\mathcal{M}$-minimization of $X$.

######  Proof 4.21.

Let $m\colon M\rightarrowtail X$ be the least $\mathcal{M}$-subobject of $X$,
and consider $s\colon S\rightarrowtail M$ in $\mathcal{M}$. Since $m\cdot
s\in\mathcal{M}$, there is some $u\colon M\to S$ with $(m\cdot s)\cdot u=m$.
Since $m$ is monic, we obtain $s\cdot u=\mathsf{id}_{M}$. Hence, $s$ is a
split-epimorphism, and together with $s\in\mathcal{M}\subseteq\mathsf{Mono}$,
$s$ is an isomorphism.

######  Proposition 4.22.

If $\mathcal{M}\subseteq\mathsf{Mono}$, $\mathcal{K}$ has wide pullbacks of
$\mathcal{M}$-morphisms, and is $\mathcal{M}$-wellpowered, then every object
$C$ of $\mathcal{K}$ has an $\mathcal{M}$-minimization.

######  Proof 4.23.

Since $\mathcal{K}$ is $\mathcal{M}$-wellpowered, all the
$\mathcal{M}$-carried morphisms $m\colon M\rightarrowtail C$ form up to
isomorphism a set $S$. The wide pullback of all $m\in S$ exists in
$\mathcal{K}$ by assumption, denote it by $\mathsf{pr}_{m}\colon P\to M$ for
$m\colon M\rightarrowtail C$. All $m^{\prime}\in S$ are in $\mathcal{M}$ and
so are all $\mathsf{pr}_{m}$ by 2.16. Hence, $p:=m\cdot\mathsf{pr}_{m}\colon
P\rightarrowtail C$ for an arbitrary $m\in S$ represents an
$\mathcal{M}$-subobject, and moreover the least $\mathcal{M}$-subobject of
$C$, as witnessed by the projections $\mathsf{pr}_{m}$. By 4.20, $P$ is the
minimization of $C$.

######  Instance 4.24.

This proof directly instantiates to the proofs of the existence of the
reachable subcoalgebra and simple quotient:

  1. 1.

In the reachability case, let $\mathcal{M}$ be a subclass of the
monomorphisms, let the base category $\mathcal{C}$ have all
$\mathcal{M}$-intersections, and let $F\colon\mathcal{C}\to\mathcal{C}$
preserve all intersections. Then the reachable part of a given pointed
coalgebra $(C,c,i_{C})$ is obtained as the intersection of all pointed
subcoalgebras of $(C,c,i_{C})$ [4].

For $\mathcal{C}=\mathsf{Set}$, and $\mathcal{M}$ being the class of injective
maps, all intersections exist. The condition that
$F\colon\mathsf{Set}\to\mathsf{Set}$ preserves all intersections is mild: all
finitary functors preserve all intersections ([3, Proof of Lem. 8.8] or [38,
Lem. 2.6.10]) and many non-finitary functors do as well, e.g. the powerset
functor. An example of a functor that does not preserve all intersections is
the filter functor [16, Sect. 5.3].

  2. 2.

For the existence of simple quotients, let $\mathcal{E}$ be a subclass of the
epimorphisms and let the base category $\mathcal{C}$ be cocomplete and
$\mathcal{E}$-cowellpowered. Then every $F$-coalgebra (C,c) has a simple
quotient given by the wide pushout of all quotient coalgebras ([4, Proposition
3.7], and [17] for $\mathcal{C}=\mathsf{Set}$).

Every set has only a set of outgoing surjective maps, so all assumptions are
met for $\mathcal{C}=\mathsf{Set}$, $\mathcal{E}$ the surjective maps, and
every $\mathsf{Set}$-functor $F$.

######  Remark 4.25.

All observations on simple quotients also apply to pointed coalgebras: An
$I$-pointed $F$-coalgebra is simple iff it is $\mathcal{E}$-carried-minimal in
$\mathcal{K}:=\mathsf{Coalg}_{I}(F)^{\operatorname{\mathsf{op}}}$. The
forgetful functor

$\mathsf{Coalg}_{I}(F)\longrightarrow\mathsf{Coalg}(F)$

preserves and reflects simple coalgebras and simple quotients (note that for
every pointed coalgebra $(C,c,i_{C})$, the slice categories
$(C,c,i_{C})/\mathsf{Coalg}_{I}(F)$ and $(C,c)/\mathsf{Coalg}(F)$ are
isomorphic). For the sake of simplicity, we will not state the results
explicitly for simple coalgebras in $\mathsf{Coalg}_{I}(F)$.

######  Definition 4.26.

We denote by $J\colon\mathcal{K}_{\min}\hookrightarrow\mathcal{K}$ the full
subcategory formed by the $\mathcal{M}$-minimal objects of $\mathcal{K}$.

In the existence proof of minimal objects (4.22) we only required (wide)
pullbacks where all morphisms in the diagram are in $\mathcal{M}$. We obtain
additional properties if we assume the pullback along $\mathcal{M}$-morphisms,
i.e. pullbacks where only one of the two morphisms is in $\mathcal{M}$:

######  Proposition 4.27.

Suppose that pullbacks along $\mathcal{M}$-morphisms exist in $\mathcal{K}$
and that every object of $\mathcal{K}$ has an $\mathcal{M}$-minimization. Then
$J\colon\mathcal{K}_{\min}\hookrightarrow\mathcal{K}$ is a coreflective
subcategory. Its right-adjoint $R\colon\mathcal{K}\to\mathcal{K}_{\min}$
($J\dashv R$) sends an object to its $\mathcal{M}$-minimization; in
particular, minimization is functorial.

######  Proof 4.28.

The universal property of $J$ follows directly from 4.14: To this end, it
suffices to consider $R$ as an object assignment. Given a morphism $h\colon
M\to X$ where $M$ is $\mathcal{M}$-minimal, we need to show that it factorizes
uniquely through the $\mathcal{M}$-minimization $s\colon S\rightarrowtail X$
of $D$, that is $RD:=S$. Since the pullback of $h$ along $s$ exists by
assumption, 4.14 yields us the desired unique factorization $u\colon M\to S$
with $s\cdot u=h$.

######  Instance 4.29.

For both of our main instances, this adjunction has been observed before:

  1. 1.

If $F\colon\mathcal{C}\to\mathcal{C}$ preserves inverse images (w.r.t.
$\mathcal{M}$), then pullbacks along $\mathcal{M}$-carried homomorphisms exist
in $\mathsf{Coalg}_{I}(F)$. Hence, the reachable $I$-pointed $F$-coalgebras
form a coreflective subcategory of $\mathsf{Coalg}_{I}(F)$, where the
coreflector maps a pointed coalgebra to its reachable part [39, Thm 5.23]

  2. 2.

The simple coalgebras form a reflective subcategory of $\mathsf{Coalg}(F)$,
and the reflector sends a coalgebra to its simple quotient, under the
assumption that the base category has pushouts along $\mathcal{E}$-morphisms.
For coalgebras in $\mathsf{Set}$, the adjunction $J\vdash R$ has been shown by
Gumm [17, Theorem 2.3].

######  Corollary 4.30.

If pullbacks along $\mathcal{M}$-morphisms exist in $\mathcal{K}$ and all
$\mathcal{M}$-minimizations exist, then $\mathcal{M}$-minimal objects are
closed under $\mathcal{E}$-quotients.

######  Proof 4.31.

Consider an $\mathcal{E}$-morphism $e\colon C\twoheadrightarrow D$ where $C$
is $\mathcal{M}$-minimal. Take the adjoint transpose $f\colon C\to RD$ with
$m\cdot f=e$ where $m\colon RD\rightarrowtail D$ is the
$\mathcal{M}$-minimization of $D$:

${C}$${RD}$${D}$$\scriptstyle{e}$$\scriptstyle{f}$$\scriptstyle{m}$

Since $RD$ is $\mathcal{M}$-minimal, $f$ is in $\mathcal{E}$ (4.6). Moreover,
$f\in\mathcal{E}$ and $m\cdot f\in\mathcal{E}$ imply $m\in\mathcal{E}$
(2.15.2), hence $m\in\mathcal{E}\cap\mathcal{M}$ is an isomorphism.

######  Example 4.32.

  1. 1.

If $F$ preserves inverse images, then reachable $F$-coalgebras are closed
under quotients [39, Cor. 5.24]. Note that if $F$ does not preserve inverse
images, then a quotient of a reachable $F$-coalgebra may not be reachable. For
example, in (pointed) coalgebras for the monoid-valued functor
$(\mathbb{R},+,0)^{(-)}$ there is the coalgebra quotient with
$h(b_{1})=h(b_{2})=b$:

$a$$b_{1}$$b_{2}$3-3$\scriptstyle{h}$$a$$b$

Since transition weights may cancel out each other ($-3+3=0$), the codomain of
$h$ is not reachable even though its domain is.

  2. 2.

If the base category $\mathcal{C}$ has pushouts along $\mathcal{E}$-morphisms,
then simple $F$-coalgebras are closed under subcoalgebras. For
$\mathcal{C}=\mathsf{Set}$, this is obvious: if in a coalgebra $(C,c)$, all
states are of pairwise different behaviour, then so they are in every
subcoalgebra of $(C,c)$.

##  5 Interplay of minimality notions

The two main aspects of minimization we have seen – reachability and
minimization for observability – are closely connected on an abstract level
and also interact well as we see in the following. In order to minimize a
pointed coalgebra under both aspects, we have two options: first construct the
reachable part and then the simple quotient, or we first form the simple
quotient and then construct its reachable part. Given the existence of
pullbacks of $\mathcal{M}$-morphisms along arbitrary morphisms, we can show
that any order is fine.

In the abstract setting of a category $\mathcal{K}$ with an
$(\mathcal{E},\mathcal{M})$-factorization system we are transforming an object
$C\in\mathcal{K}$ into an object $C^{\prime}$ that is $\mathcal{M}$-minimal in
$\mathcal{K}$ and $\mathcal{E}$-minimal in
$\mathcal{K}^{\operatorname{\mathsf{op}}}$.

######  Proposition 5.1.

Suppose $\mathcal{K}$ has an $(\mathcal{E},\mathcal{M})$-factorization system
such that all $\mathcal{M}$-minimizations in $\mathcal{K}$ and all
$\mathcal{E}$-minimizations in $\mathcal{K}^{\operatorname{\mathsf{op}}}$
exist. If $\mathcal{K}$ has pullbacks along $\mathcal{M}$-morphisms and
pushouts along $\mathcal{E}$-morphisms, then for every $C$ in $\mathcal{K}$
the following two constructions yield the same object:

  1. 1.

The $\mathcal{M}$-minimization of $C$ in $\mathcal{K}$ followed by its
$\mathcal{E}$-minimization in $\mathcal{K}^{\operatorname{\mathsf{op}}}$.

  2. 2.

The $\mathcal{E}$-minimization of $C$ in
$\mathcal{K}^{\operatorname{\mathsf{op}}}$ followed by its
$\mathcal{M}$-minimization in $\mathcal{K}$.

######  Proof 5.2.

In the first approach, denote the $\mathcal{M}$-minimization of $C$ by
$m\colon R\rightarrowtail C$ and its $\mathcal{E}$-minimization by $s\colon
R\twoheadrightarrow V$. In the other approach, denote the
$\mathcal{E}$-minimization of $C$ by $e\colon C\twoheadrightarrow Q$ and its
$\mathcal{M}$-minimization by $t\colon W\rightarrowtail Q$:

${R}$${C}$${V}$${W}$${Q}$$\scriptstyle{m}$$\scriptstyle{s}$$\scriptstyle{e}$$\scriptstyle{t}$

We need to prove that $V$ and $W$ are isomorphic, making the above (then-
closed) square commute. The $\mathcal{M}$-minimal objects form a coreflective
subcategory (4.27), so $e\cdot m$, whose domain is $\mathcal{M}$-minimal,
factorizes through the $\mathcal{M}$-minimization of the codomain of $e\cdot
m$, i.e. we have $h\colon R\to W$ with $t\cdot h=e\cdot m$. Since $Q$ is
$\mathcal{E}$-minimal, its $\mathcal{M}$-subobject $W$ is also
$\mathcal{E}$-minimal in $\mathcal{K}^{\operatorname{\mathsf{op}}}$ (4.30).
The $\mathcal{E}$-minimal objects form a reflective subcategory (4.27).
Applying the reflection to $h\colon R\to W$, we obtain $\phi\colon V\to W$
with $h=\phi\cdot s$. Since $V$ is $\mathcal{E}$-minimal (in
$\mathcal{K}^{\operatorname{\mathsf{op}}}$), $\phi$ is in $\mathcal{M}$, and
since $W$ is $\mathcal{M}$-minimal, $\phi$ is in $\mathcal{E}$, and thus
$\phi$ is an isomorphism.

In the concrete case of $F$-coalgebras, a coalgebra that is both simple and
reachable is called a _well-pointed_ coalgebra (see [4, Section 3.2]).

######  Instance 5.3.

If $F\colon\mathcal{C}\to\mathcal{C}$ fulfils all assumptions from the
previous 4.29 (and in particular preserves inverse images), then the
construction of the simple quotient and the reachability construction for
$F$-coalgebras can be performed in any order, yielding the same well-pointed
coalgebra.

If $F$ does not preserve inverse images, then in the construction of the
simple quotient, transitions may cancel out each other and this may affect the
reachability of states. We have seen an example for this in 4.32.1 where
performing reachability first and observability second leads to a simple
coalgebra in which states are unreachable, i.e. the result is not well-
pointed. Hence, in contrast to the well-known automata minimization procedure,
the minimization of a coalgebra in general has to be performed by first
computing its simple quotient and secondly computing the reachable part in the
simple quotient.

If $F$ preserves inverse images, such as the functor for automata, any order
is fine. In sets, the reachability computation is a simple breadth-first
search [39], and hence runs in linear time. On the other hand, existing
algorithms for computing the simple quotient for many $\mathsf{Set}$-functors
run in at least $n\cdot\log n$ time where $n$ is the size of the coalgebra
[15, 36]. Hence, the reachability analysis should be done first whenever
possible.

##  6 Conclusions

We have seen a common ground for minimality notions in a category with various
instances in a coalgebraic setting. The abstract results about the uniqueness
and the existence of the minimization instantiate to the standard results for
reachability and observability of coalgebras. Most of the general results even
hold if the $(\mathcal{E},\mathcal{M})$-factorization system is not proper.
The tree unravelling of an automaton is an instance of minimization for a non-
proper factorization system.

It remains for future work to relate the efficient algorithmic approaches to
the minimization tasks: reachability is computed by breadth-first search [39,
7] and observability is computed by partition refinement algorithms [24, 36,
13]. Even though their run-time complexity differs – reachability is usually
linear, whereas partition refinement algorithms are quasilinear or slower –
they have striking similarities. All these algorithms compute a chain of
subobjects resp. quotients on the carrier of the input coalgebra and terminate
at the first element of the chain admitting a coalgebra structure compatible
with the input coalgebra. It is thus likely that this relation can be made
formal. A similar connection between the reachability of algebras and
partition refinement on coalgebras is already known [30].

## References

  * [1] Peter Aczel and Nax Mendler.  A final coalgebra theorem.  In Proc. Category Theory and Computer Science (CTCS), volume 389 of Lecture Notes Comput. Sci., pages 357–365. Springer, 1989.
  * [2] Jiří Adámek, Horst Herrlich, and George E. Strecker.  Abstract and Concrete Categories: The Joy of Cats.  Dover Publications, 2nd edition, 2009.
  * [3] Jiří Adámek, Stefan Milius, and Lawrence S. Moss.  Fixed points of functors.  Journal of Logical and Algebraic Methods in Programming, 95:41–81, 2018.
  * [4] Jiří Adámek, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa.  Well-pointed coalgebras.  Logical Methods in Computer Science, 9(3:2):51 pp., 2013.
  * [5] Steve Awodey.  Category Theory.  Oxford Logic Guides. OUP Oxford, 2010.
  * [6] Adriana Balan and Alexander Kurz.  Finitary functors: From set to preord and poset.  In Andrea Corradini, Bartek Klin, and Corina Cîrstea, editors, Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Proceedings, volume 6859 of Lecture Notes in Computer Science, pages 85–99. Springer, 2011.  doi:10.1007/978-3-642-22944-2_7.
  * [7] Simone Barlocco, Clemens Kupke, and Jurriaan Rot.  Coalgebra learning via duality.  In Mikolaj Bojanczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11425 of Lecture Notes in Computer Science, pages 62–79. Springer, 2019.  doi:10.1007/978-3-030-17127-8_4.
  * [8] Falk Bartels, Ana Sokolova, and Erik P. de Vink.  A hierarchy of probabilistic system types.  Theor. Comput. Sci., 327(1-2):3–22, 2004.  doi:10.1016/j.tcs.2004.07.019.
  * [9] Nick Bezhanishvili, Clemens Kupke, and Prakash Panangaden.  Minimization via duality.  In C.-H. Luke Ong and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computation - 19th International Workshop, WoLLIC 2012, Buenos Aires, Argentina, September 3-6, 2012. Proceedings, volume 7456 of Lecture Notes in Computer Science, pages 191–205. Springer, 2012.  doi:10.1007/978-3-642-32621-9_14.
  * [10] Michel Bidoit, Rolf Hennicker, and Alexander Kurz.  On the duality between observability and reachability.  In Furio Honsell and Marino Miculan, editors, Foundations of Software Science and Computation Structures, 4th International Conference (FOSSACS 2001), Held as Part of ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, volume 2030 of Lecture Notes in Computer Science, pages 72–87. Springer, 2001.  doi:10.1007/3-540-45315-6_5.
  * [11] Filippo Bonchi, Marcello M. Bonsangue, Helle Hvid Hansen, Prakash Panangaden, Jan J. M. M. Rutten, and Alexandra Silva.  Algebra-coalgebra duality in brzozowski’s minimization algorithm.  ACM Trans. Comput. Log., 15(1):3:1–3:29, 2014.  doi:10.1145/2490818.
  * [12] Salem Derisavi, Holger Hermanns, and William H. Sanders.  Optimal state-space lumping in markov chains.  Inf. Process. Lett., 87(6):309–315, 2003.  doi:10.1016/S0020-0190(03)00343-0.
  * [13] Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann.  Efficient coalgebraic partition refinement.  In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 32:1–32:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.  doi:10.4230/LIPIcs.CONCUR.2017.32.
  * [14] Agostino Dovier, Carla Piazza, and Alberto Policriti.  An efficient algorithm for computing bisimulation equivalence.  Theor. Comput. Sci., 311(1-3):221–256, 2004.  doi:10.1016/S0304-3975(03)00361-X.
  * [15] Jan Friso Groote, Jan Martens, and Erik de Vink.  Bisimulation by Partitioning Is $\Omega((m+n)\log n)$.  In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory (CONCUR 2021), volume 203 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1–31:16, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.  doi:10.4230/LIPIcs.CONCUR.2021.31.
  * [16] H. Peter Gumm.  Functors for coalgebras.  Algebra Universalis, 45(2):135–147, April 2001.  doi:10.1007/s00012-001-8156-x.
  * [17] H. Peter Gumm.  On minimal coalgebras.  Applied Categorical Structures, 16(3):313–332, June 2008.  doi:10.1007/s10485-007-9116-1.
  * [18] H. Peter Gumm and Tobias Schröder.  Monoid-labeled transition systems.  In Coalgebraic Methods in Computer Science, CMCS 2001, volume 44(1) of ENTCS, pages 185–204. Elsevier, 2001.
  * [19] H. Peter Gumm and Tobias Schröder.  Types and coalgebraic structure.  algebra universalis, 53(2):229–252, 2005.  doi:10.1007/s00012-005-1888-2.
  * [20] Ichiro Hasuo, Bart Jacobs, and Ana Sokolova.  Generic trace theory.  In Neil Ghani and John Power, editors, Proceedings of the Eighth Workshop on Coalgebraic Methods in Computer Science, CMCS 2006, Vienna, Austria, March 25-27, 2006, volume 164 of Electronic Notes in Theoretical Computer Science, pages 47–65. Elsevier, 2006.  doi:10.1016/j.entcs.2006.06.004.
  * [21] John Hopcroft.  An $n\log n$ algorithm for minimizing states in a finite automaton.  In Theory of Machines and Computations, pages 189–196. Academic Press, 1971.
  * [22] Thomas Ihringer.  Algemeine Algebra. Mit einem Anhang über Universelle Coalgebra von H. P. Gumm, volume 10 of Berliner Studienreihe zur Mathematik.  Heldermann Verlag, 2003.
  * [23] Bartek Klin and Vladimiro Sassone.  Structural operational semantics for stochastic and weighted transition systems.  Inf. Comput., 227:58–83, 2013.
  * [24] Barbara König and Sebastian Küpper.  Generic partition refinement algorithms for coalgebras and an instantiation to weighted automata.  In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, volume 8705 of Lecture Notes in Computer Science, pages 311–325. Springer, 2014.  doi:10.1007/978-3-662-44602-7_24.
  * [25] Alexander Kurz.  Logics for Coalgebras and Applications to Computer Science.  PhD thesis, Ludwig-Maximilians-Universität München, 7 2000.  https://www.cs.le.ac.uk/people/akurz/LMU/Diss/all-s.ps.gz.
  * [26] Alexander Kurz, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries.  Nominal coalgebraic data types with applications to lambda calculus.  Log. Methods Comput. Sci., 9(4), 2013.  doi:10.2168/LMCS-9(4:20)2013.
  * [27] Stefan Milius, Dirk Pattinson, and Thorsten Wißmann.  A new foundation for finitary corecursion and iterative algebras.  Information and Computation, page 104456, 09 2019.  doi:10.1016/j.ic.2019.104456.
  * [28] Stefan Milius, Lutz Schröder, and Thorsten Wißmann.  Regular behaviours with names - on rational fixpoints of endofunctors on nominal sets.  Appl. Categorical Struct., 24(5):663–701, 2016.  doi:10.1007/s10485-016-9457-8.
  * [29] Robert Paige and Robert Endre Tarjan.  Three partition refinement algorithms.  SIAM J. Comput., 16(6):973–989, 1987.  doi:10.1137/0216062.
  * [30] Jurriaan Rot.  Coalgebraic minimization of automata by initiality and finality.  In Lars Birkedal, editor, The Thirty-second Conference on the Mathematical Foundations of Programming Semantics, MFPS 2016, Carnegie Mellon University, Pittsburgh, PA, USA, May 23-26, 2016, volume 325 of Electronic Notes in Theoretical Computer Science, pages 253–276. Elsevier, 2016\.  doi:10.1016/j.entcs.2016.09.042.
  * [31] Jan J. M. M. Rutten.  Universal coalgebra: a theory of systems.  Theor. Comput. Sci., 249(1):3–80, 2000.  doi:10.1016/S0304-3975(00)00056-6.
  * [32] Věra Trnková.  On a descriptive classification of set functors I.  Commentationes Mathematicae Universitatis Carolinae, 12(1):143–174, 1971.
  * [33] Daniele Turi and Gordon D. Plotkin.  Towards a mathematical operational semantics.  In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 280–291. IEEE Computer Society, 1997.  doi:10.1109/LICS.1997.614955.
  * [34] Antti Valmari.  Bisimilarity minimization in o(m logn) time.  In Giuliana Franceschinis and Karsten Wolf, editors, Applications and Theory of Petri Nets, 30th International Conference, PETRI NETS 2009, Paris, France, June 22-26, 2009. Proceedings, volume 5606 of Lecture Notes in Computer Science, pages 123–142. Springer, 2009.  doi:10.1007/978-3-642-02424-5_9.
  * [35] Antti Valmari and Giuliana Franceschinis.  Simple _O_(_m_ log _n_) time markov chain lumping.  In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010\. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 38–52. Springer, 2010.  doi:10.1007/978-3-642-12002-2_4.
  * [36] Thorsten Wißmann, Ulrich Dorsch, Stefan Milius, and Lutz Schröder.  Efficient and modular coalgebraic partition refinement.  Log. Methods Comput. Sci., 16(1), 2020.  doi:10.23638/LMCS-16(1:8)2020.
  * [37] Thorsten Wißmann, Jérémy Dubut, Shin-ya Katsumata, and Ichiro Hasuo.  Path category for free - open morphisms from coalgebras with non-deterministic branching.  In Mikolaj Bojanczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference (FOSSACS 2019), Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11425 of Lecture Notes in Computer Science, pages 523–540. Springer, 2019.  doi:10.1007/978-3-030-17127-8_30.
  * [38] Thorsten Wißmann.  Coalgebraic Semantics and Minimization in Sets and Beyond.  Phd thesis, Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU), 2020.  URL: https://opus4.kobv.de/opus4-fau/frontdoor/index/index/docId/14222.
  * [39] Thorsten Wißmann, Stefan Milius, Shin-ya Katsumata, and Jérémy Dubut.  A coalgebraic view on reachability.  Commentationes Mathematicae Universitatis Carolinae, 60:4:605–638, 12 2019.  doi:10.14712/1213-7243.2019.026.

## Appendix: Omitted Proofs

#### Proof of 2.6

Let $c_{i}\colon UDi\to FUDi$ be the coalgebra structure of
$Di\in\mathsf{Coalg}(F)$ for every $i\in\mathcal{D}$. For the colimit of
$UD\colon\mathcal{D}\to\mathcal{C}$

$\leavevmode\hbox to108.73pt{\vbox
to17.42pt{\pgfpicture\makeatletter\hbox{\hskip 54.3642pt\lower-8.75955pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-54.3642pt}{-8.65971pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
14.2656pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.96005pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${UDi}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
14.2656pt\hfil&\hfil\hskip 52.09859pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.79308pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\operatorname{colim}(UD)}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
28.09862pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-25.63301pt}{-6.15971pt}\pgfsys@lineto{-2.433pt}{-6.15971pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.23302pt}{-6.15971pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-18.50816pt}{-2.44585pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathsf{inj}_{i}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\qquad\text{for every
}i\in\mathcal{D}$

apply $F$ and precompose with $c_{i}$, yielding

$\leavevmode\hbox to176.9pt{\vbox
to17.42pt{\pgfpicture\makeatletter\hbox{\hskip 88.44923pt\lower-8.75955pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-88.44923pt}{-8.65971pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
14.2656pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.96005pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${UDi}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
14.2656pt\hfil&\hfil\hskip 42.1753pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.86978pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${FUDi}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
18.17532pt\hfil&\hfil\hskip 56.00832pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-27.7028pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${F\operatorname{colim}(UD)}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
32.00835pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-59.71805pt}{-6.15971pt}\pgfsys@lineto{-36.51804pt}{-6.15971pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-36.31805pt}{-6.15971pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-50.12172pt}{-2.48792pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{c_{i}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{0.63257pt}{-6.15971pt}\pgfsys@lineto{23.83258pt}{-6.15971pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{24.03256pt}{-6.15971pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.0206pt}{-2.44586pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{F\mathsf{inj}_{i}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\qquad\text{for every
}i\in\mathcal{D}.$

This is a cocone for the diagram $D$ because for all $h\colon i\to j$ in
$\mathcal{D}$ the outside of the following diagram commutes:

${UDi}$${FUDi}$${UDj}$${FUDj}$${F\operatorname{colim}(UD)}$$\scriptstyle{c_{i}}$
$Dh$ coalgebra morphism
$\scriptstyle{UDh}$$\scriptstyle{F\mathsf{inj}_{i}}$$\scriptstyle{FUDh}$$\scriptstyle{c_{j}}$$\scriptstyle{F\mathsf{inj}_{j}}$

Thus we obtain a coalgebra structure $u\colon\operatorname{colim}(UD)\to
F\operatorname{colim}(UD)$. Since $u$ is a cocone-morphism, every
$\mathsf{inj}_{i}$ is an $F$-coalgebra morphism.

In order to show that $(\operatorname{colim}(UD),u)$ is the colimit of
$D\colon\mathcal{D}\to\mathsf{Coalg}(F)$, consider another cocone
$(m_{i}\colon Di\to(E,e))_{i\in\mathcal{D}}$.

${\operatorname{colim}(UD)}$${E}$${F\operatorname{colim}(UD)}$${FE}$$\scriptstyle{u}$$\scriptstyle{w}$$\scriptstyle{e}$$\scriptstyle{Fw}$

In $\mathcal{C}$, we obtain a cocone morphism
$w\colon\operatorname{colim}(UD)\to E$. With a similar verification as before,
$(e\cdot m_{i}\colon UDi\to FE)_{i\in\mathcal{D}}$ is a cocone for $D$, and
thus both $d\cdot w$ and $Fw\cdot u\colon\operatorname{colim}(UD)\to FE$ are
cocone morphisms (for $UD$). Since $\operatorname{colim}(UD)$ is the colimit,
this implies that $d\cdot w=Fw\cdot u$, i.e. $w\colon(colim(UD),u)\to(E,e)$ is
a coalgebra morphism. Since $U\colon\mathsf{Coalg}(F)\to\mathcal{C}$ is
faithful, $w$ is the unique cocone morphism, and so
$(\operatorname{colim}UD,u)$ is indeed the colimit of $UD$. ∎

#### Proof of 2.16

Consider the $(\mathcal{E},\mathcal{M})$-factorization of $\mathsf{pr}_{j}$
into $e\colon P\twoheadrightarrow C$ and $m\colon C\rightarrowtail A_{j}$ with
$\mathsf{pr}_{j}=m\cdot e$. On the image, we define a cone structure
$(c_{i}\colon C\to A_{i})_{i\in I}$ by $c_{j}=m$ and for every $i\in
I\setminus\\{j\\}$ by the diagonal fill-in:

$\leavevmode\hbox to105.94pt{\vbox
to51.19pt{\pgfpicture\makeatletter\hbox{\hskip
54.11978pt\lower-25.64378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-50.62582pt}{-25.54385pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
8.21005pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.90451pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${P}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
8.21005pt\hfil&\hfil\hskip 32.23676pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.93124pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${C}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
8.23679pt\hfil&\hfil\hskip 33.36885pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.06334pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${A_{j}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
9.36888pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
9.02019pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.71465pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${A_{i}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
9.02019pt\hfil&\hfil\hskip 23.99997pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 32.3489pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.0434pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${B}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.34894pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{}{{}}\pgfsys@moveto{-33.19559pt}{12.04448pt}\pgfsys@lineto{-9.18544pt}{12.04448pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.4654pt}{12.04448pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.98546pt}{12.04448pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-22.62022pt}{14.39725pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{e}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-41.60564pt}{5.68477pt}\pgfsys@lineto{-41.60564pt}{-14.45087pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{-41.60564pt}{-14.65085pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-51.96701pt}{-5.40942pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathsf{pr}_{i}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{10.16806pt}{12.04448pt}\pgfsys@lineto{31.2881pt}{12.04448pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{10.36804pt}{12.04448pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{31.48808pt}{12.04448pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{17.43535pt}{16.49405pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{c_{j}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}\pgfsys@setdash{2.79985pt,1.59991pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-7.82553pt}{5.68477pt}\pgfsys@lineto{-32.0808pt}{-14.94556pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.76173}{-0.64789}{0.64789}{-0.76173}{-32.23311pt}{-15.0751pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ }}{ } {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-17.75272pt}{-10.1266pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{c_{i}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{41.25694pt}{2.74922pt}\pgfsys@lineto{41.25694pt}{-14.45087pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{41.25694pt}{-14.65085pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{43.60971pt}{-7.43294pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{f_{j}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{-30.30548pt}{-23.04385pt}\pgfsys@lineto{32.30804pt}{-23.04385pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-30.1055pt}{-23.04385pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{32.50803pt}{-23.04385pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.61804pt}{-19.32999pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{f_{i}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\quad\text{for all
}i\in I\setminus\\{j\\}.$

The diagonal $c_{i}$ is induced, because $f_{i}\in\mathcal{M}$ for all $i\in
I\setminus\\{j\\}$. The family $(c_{i})_{i\in I}$ forms a cone for the wide
pullback, because for all $i,i^{\prime}\in I$ we have $f_{i}\cdot
c_{i}=f_{j}\cdot c_{j}=f_{i^{\prime}}\cdot c_{i^{\prime}}$. This makes $e$ a
cone morphism, because $c_{i}\cdot e=\mathsf{pr}_{i}$ for all $i\in I$.
Moreover, the limiting cone $P$ induces a cone morphism $s\colon C\to P$ and
we have $s\cdot e=\mathsf{id}_{P}$. Consider the commutative diagrams:

${P}$${C}$${P}$${C}$${A_{j}}$$\scriptstyle{e}$$\scriptstyle{e}$$\scriptstyle{\mathsf{id}_{P}}$$\scriptstyle{s}$$\scriptstyle{c_{j}}$$\scriptstyle{\mathsf{pr}_{j}}$$\scriptstyle{e}$
$(*)$ $(*)$ $\scriptstyle{c_{j}}$ and  ${P}$${C}$
${C}$${A_{j}.}$$\scriptstyle{e}$$\scriptstyle{e}$$\scriptstyle{c_{j}}$$\scriptstyle{\mathsf{id}_{C}}$$\scriptstyle{c_{j}}$

The parts marked by $(*)$ commute because $e$ and $s$ are cone morphisms.
Since the diagonal fill-in in 2.10.3 is unique, we have $e\cdot
s=\mathsf{id}_{C}$. Thus, $e$ is an isomorphism, and
$\mathsf{pr}_{j}=c_{j}\cdot e$ is in $\mathcal{M}$, as desired. ∎

#### Proof of 3.2

It is clear that every $\mathsf{Mono}$-carried homomorphism is monic in
$\mathsf{Coalg}(F)$. Conversely, let $m\colon(C,c)\to(D,d)$ be a monomorphism
in $\mathsf{Coalg}(F)$. Let $\mathsf{pr}_{1},\mathsf{pr}_{2}\colon K\to C$ be
a weak kernel pair of $m$. Since $F$ preserves weak kernel pairs,
$F\mathsf{pr}_{1},F\mathsf{pr}_{2}\colon FK\to FC$ is a weak kernel pair of
$Fm\colon FC\to FD$. This induces some cone morphism $k\colon K\to FK$ making
$\mathsf{pr}_{1}$ and $\mathsf{pr}_{2}$ coalgebra morphisms $(K,k)\to(C,c)$:

${K}$${C}$${D}$${FK}$${FC}$${FD}$$\scriptstyle{\mathsf{pr}_{1}}$$\scriptstyle{\mathsf{pr}_{2}}$$\scriptstyle{k}$$\scriptstyle{c}$$\scriptstyle{m}$$\scriptstyle{d}$$\scriptstyle{F\mathsf{pr}_{1}}$$\scriptstyle{F\mathsf{pr}_{2}}$$\scriptstyle{Fm}$

Since $m$ is monic in $\mathsf{Coalg}(F)$, this implies that
$\mathsf{pr}_{1}=\mathsf{pr}_{2}$. For the verification that $m$ is a
monomorphism in $\mathcal{C}$, consider $f,g\colon X\to C$ with $m\cdot
f=m\cdot g$. Since $\mathsf{pr}_{1},\mathsf{pr}_{2}$ is a weak kernel pair, it
induces some cone morphism $v\colon X\to K$, fulfilling
$f=\mathsf{pr}_{1}\cdot v$ and $g=\mathsf{pr}_{2}\cdot v$. Since,
$\mathsf{pr}_{1}=\mathsf{pr}_{2}$, we find $f=g$ as desired. ∎

#### Proof of 3.8

Denote the unit and multiplication of the monad $T$ by
$\eta\colon\mathsf{Id}\to T$ and $\mu\colon TT\to T$, respectively. Consider
an $T$-algebra homomorphism $f\colon(A,a)\to(B,b)$ for Eilenberg-Moore
algebras $(A,a)$ and $(B,b)$ and denote its image factorization in
$\mathsf{Alg}(T)$ by $(I,i)$, with homomorphisms
$e\colon(A,a)\twoheadrightarrow(I,i)$ and $m\colon(I,i)\rightarrowtail(B,b)$.
We verify that $i\colon TI\to I$ is an Eilenberg-Moore algebra.

  * •

First, we verify $i\cdot\eta_{I}=\mathsf{id}_{I}$ by showing that both
$i\cdot\eta_{I}$ and $\mathsf{id}_{I}$ are both diagonals of the following
square:

${A}$${I}$${I}$${B}$$\scriptstyle{e}$$\scriptstyle{e}$$\scriptstyle{m}$$\scriptstyle{\mathsf{id}_{I}}$$\scriptstyle{m}$
${A}$${I}$${TA}$${TI}$${B}$${A}$${TB}$${I}$${B}$$\scriptstyle{e}$$\scriptstyle{\eta_{A}}$$\scriptstyle{\mathsf{id}_{A}}$
(N) $\scriptstyle{\eta_{I}}$$\scriptstyle{m}$ (A)
$\scriptstyle{Te}$$\scriptstyle{a}$ (N)
$\scriptstyle{Tm}$$\scriptstyle{i}$$\scriptstyle{\eta_{B}}$$\scriptstyle{\mathsf{id}_{B}}$$\scriptstyle{e}$
(H) (H) $\scriptstyle{b}$ (A) $\scriptstyle{m}$

The left-hand square commutes trivially, and the right-hand square commutes
because $\eta$ is natural (N), because $e$ and $m$ are $T$-algebra
homomorphisms (H), and because $(A,a)$ and $(B,b)$ are Eilenberg-Moore
algebras (A). By the uniqueness of the diagonal lifting property, we obtain
$i\cdot\eta_{I}=\mathsf{id}_{I}$.

  * •

Next, we verify $i\cdot Ti=i\cdot\mu_{i}$ by showing that both are diagonals
in same square. To this end, let
$(s_{A},s_{I},s_{B})\in\\{(Ta,Ti,Tb),(\mu_{A},\mu_{I},\mu_{B})\\}$, i.e. we
obtain one diagonal for $(Ta,Ti,Tb)$ and one for $(\mu_{A},\mu_{I},\mu_{B})$:

${TTA}$${TTI}$${TA}$${TA}$${TI}$${TTB}$${A}$${TB}$${TB}$${I}$${B}$$\scriptstyle{TTe}$$\scriptstyle{\mu_{A}}$$\scriptstyle{s_{A}}$
(N) $\scriptstyle{s_{I}}$$\scriptstyle{TTm}$ (A)
$\scriptstyle{a}$$\scriptstyle{Te}$$\scriptstyle{a}$$\scriptstyle{i}$$\scriptstyle{Tm}$
(N) $\scriptstyle{s_{B}}$$\scriptstyle{\mu_{B}}$$\scriptstyle{e}$ (H) (H)
$\scriptstyle{b}$ (A) $\scriptstyle{b}$$\scriptstyle{m}$

In both cases, we have that $e$ and $m$ are $T$-algebra homomorphisms $(H)$.
For $(s_{A},s_{I},s_{B}):=(Ta,Ti,Tb)$, we have that $(A,a)$ and $(B,b)$ are
Eilenberg-Moore algebras (A) and that $e$ and $m$ are homomorphisms (N). For
$(s_{A},s_{I},s_{B}):=(\mu_{A},\mu_{I},\mu_{B})$, we have that the parts (A)
commute trivially, and the parts (N) commute because $\mu$ is natural. Since
$T$ preserves $\mathcal{E}$, we have $TTe\in\mathcal{E}$, and thus by the
uniqueness of the diagonal, we obtain $i\cdot Ti=i\cdot\mu_{I}$.

Thus, $(I,i)$ fulfils the axioms of an Eilenberg-Moore algebra. The remaining
properties of the factorization system hold because the Eilenberg-Moore
category is a full subcategory of $\mathsf{Alg}(T)$. ∎

#### Proof of 4.9

We verify the postulated equivalence using that $C$ is $\mathcal{M}$-minimal
iff every $h\colon B\to C$ is an epimorphism (4.6,
$\mathcal{E}=\mathsf{Epi}$).

  * •

For ‘if’, we verify that every $h\colon B\to C$ is an epimorphism: for
$u,v\colon C\to D$ with $u\cdot h=v\cdot h$, we directly obtain $u=v$ by
assumption. Thus, $h$ is an epimorphism.

  * •

For ‘only if’, consider $u,v\colon C\to D$ and take a weak equalizer $e\colon
E\to C$; hence, $u\cdot e=v\cdot e$. Since $e$ is an epimorphism (by
minimality), we obtain $u=v$. ∎