Relative fixed points of functors

# Relative fixed points of functors

Ezra Schoen
Strathclyde University  United Kingdom
<EMAIL_ADDRESS>Jade Master
Strathclyde University Leverhulme Trust Research Project Grant RPG-2020-232
United Kingdom
<EMAIL_ADDRESS>Clemens Kupke∗
Strathclyde University  United Kingdom
<EMAIL_ADDRESS>
###### Abstract

We show how the relatively initial or relatively terminal fixed points of [1]
for a well-behaved functor $F$ form a pair of adjoint functors between
$F$-coalgebras and $F$-algebras. We use the language of locally presentable
categories to find sufficient conditions for existence of this adjunction. We
show that relative fixed points may be characterized as (co)equalizers of the
free (co)monad on $F$. In particular, when $F$ is a polynomial functor on
$\mathsf{Set}$ the relative fixed points are a quotient or subset of the free
term algebra or the cofree term coalgebra. We give examples of the relative
fixed points for polynomial functors and an example which is the Sierpinski
carpet. Lastly, we prove a general preservation result for relative fixed
points.

###### keywords:

coalgebra, algebra, fixed points, coalgebra-to-algebra morphisms

##  1 Introduction

Fixed points of functors are particularly relevant to the study of coalgebras.
As in [2, 3] these fixed points capture the ideas of induction and coinduction
on coalgebras. The main focus of this work has thus far been on either the
least fixed point of a functor or the greatest fixed point of a functor.
However, in general a functor has more fixed points than just these two. We
call these additional fixed points “relative fixed points”, after the
“relatively terminal coalgebras” of [1]. Other constructions yielding relative
fixed points are the rational fixed points of Adámek, Milius, and Velebil [4]
and the locally finite fixed points of Milius, Pattinson, and Wißmann [5]. The
main contribution of this paper is a presentation of relative fixed points via
a pair of adjoint functors

${F\text{-}\mathsf{Coalg}}$${F\text{-}\mathsf{Alg}}$$\scriptstyle{\mu}$${\bot}$$\scriptstyle{\nu}$
(1)

This adjunction reveals the deep connection between relative fixed points and
coalgebra-to-algebra homomorphisms (abreviated as ca-morphism). Algebras and
coalgebras which have unique ca-morphisms going into or out of them have been
studied extensively in [6, 7, 8, 9, 10] due to their connection to inductive
principles. However, the fixed points studied in this paper are universal with
respect to ca-morphisms which may not be unique. In the context of functional
programming [11], not-necessarily unique ca-morphisms are used as data
structures for recursion schemes. In [12], the authors argue for the use of
non-unique ca-morphisms as a framework for scientific modelling. Whatever the
reason for the their relevance, this paper studies relative fixed points in
the context of the novel adjunction through examples and results.

The paper is organised as follows: In Section 2, we will introduce relative
fixed points for $F$-(co)algebras, and the adjunction (1) in the full
categorical case. After that we will provide sufficient conditions for the
existence of the adjunction. In Section 3, we will provide examples of these
relative fixed points as well as an explicit characterization for polynomial
functors. In Section 4, we will discuss when the adjunction is preserved by a
functor and give some important examples of this phenomenon. Finally, in
Section 5 we will draw conclusions and point to ideas for future work.

We now finish the introduction with a brief discussion of relative fixed
points for monotone functions to equip the reader with some intuitions before
moving to the more general categorical setting that follows.

#### Warm-up: Relative fixed points of monotone functions

Consider a monotone function $f:L\to L$ on a complete lattice $L$. The Kleene
fixed point theorem provides a construction of least and greatest fixed points
for $f$. For example, let $f$ be the following monotone function on
$([0,1],\leq)$ the interval of real numbers with the usual ordering:

The function $f$ is overlayed with the function $y=x$. The intersection of the
two curves indicate fixed points of $f$. The least fixed point of $f$ is $0$
and the greatest fixed point is $1$ but there are $3$ other fixed points in-
between. These relative fixed points have a similar construction to the least
and greatest ones. Given a “post-fixed point” i.e. a point $x\in[0,1]$ such
that $x\leq f(x)$ we may find the first fixed point above $x$ as

$\hfill\mu(x)=\sup\\{x,f(x),f^{2}(x),f^{3}(x),\ldots\\}\hfill$

where the $\ldots$ indicate iteration to a sufficiently large ordinal.
Similarly, given a “pre-fixed point” $f(y)\leq y$, we may find the closest
fixed point below $y$ as

$\hfill\nu(y)=\inf\\{y,f(y),f^{2}(y),f^{3}(y),\ldots\\}\hfill$

For a complete lattice $L$, let $Pre(f)$ be the suborder of $L$ consisting of
only the post-fixed points $x\leq f(x)$. Similarly, let $Post(f)$ be the
suborder of pre-fixed points $f(y)\leq y$. Then there is a Galois connection

${Post(f)}$${Pre(f)}$$\scriptstyle{\mu_{\\_}f}$${\bot}$$\scriptstyle{\nu_{\\_}f}$

Being a Galois connection means that

$\hfill\mu(x)\leq y\iff x\leq\nu(y)\hfill$

In this paper we will generalize this Galois connection to fixed points of
functors rather than monotone functions. When generalizing from posets to
categories we make the replacements shown in Table 1.

Poset | Category
---|---
Monotone Function $f$ | Functor $F$
Post-fixed point of $f$ |  $F$-coalgebra
Pre-fixed point of $f$ |  $F$-algebra
$\sup\\{f(x),f^{2}(x),f^{3}(x),\ldots\\}$ | $\mathrm{colim}(X\to F(X)\to F^{2}(X)\to F^{3}(X)\ldots)$
$\inf\\{f(x),f^{2}(x),f^{3}(x),\ldots\\}$ | $\lim(X\leftarrow F(X)\leftarrow F^{2}(X)\leftarrow F^{3}(X)\ldots)$
Galois connection | Adjunction
Figure 1: Generalization from Posets to Categories

##### Acknowledgements.

For insightful comments and questions, thank you to every member of the
Mathematically Structured Programming group, Corina Cirstea, Toby Wilkinson,
and Alexandre Goy.

##  2 Relative Fixed Points are Adjoint

In this section, we recall the definition of ‘relatively terminal coalgebra’
from [1], and define the dual notion of ‘relatively initial algebra’. As is
usual for definitions via universal properties, there may or may not be an
object enjoying the property; however, if there is one, it is unique up to
unique isomorphism.

###### Definition 2.1

For an algebra $a$ and a coalgebra $b$, a coalgebra-to-algebra morphism from
$a$ to $b$ (abbreviated as ca-morphism) is a morphism $f\colon B\to A$ making
the following diagram commute:

${FB}$${FA}$${B}$${A}$$\scriptstyle{Ff}$$\scriptstyle{a}$$\scriptstyle{b}$$\scriptstyle{f}$

Let $\mathsf{Hylo}(b,a)$ denote the set of coalgebra-to-algebra morphisms from
$b$ to $a$.

The notation $\mathsf{Hylo}(b,a)$ comes from the name ‘hylomorphism’ for ca-
morphism, which is part of the ‘cata-ana’ naming scheme in the theory of
recursive algorithms [11]. We have chosen to use the term ‘ca-morphism’, as in
our view this term is more readily understood; but we will still use
$\mathsf{Hylo}(b,a)$ for the set of ca-morphisms $b\to a$.

###### Definition 2.2

Suppose we have an algebra $a:FA\to A$. A coalgebra $a^{\prime}:FA^{\prime}\to
A^{\prime}$ is called _terminal relative to $a$_ if there is a bijection
(natural in $b$)

$\hfill\phi\colon
F\text{-}\mathsf{Coalg}(b,a^{\prime})\cong\mathsf{Hylo}(b,a)\hfill$

Similarly, for a coalgebra $b:B\to FB$, an algebra $b^{\prime}:FB^{\prime}\to
B^{\prime}$ is called _initial relative to $b$_ if there is a bijection
(natural in $a$)

$\hfill\psi\colon
F\text{-}\mathsf{Alg}(b^{\prime},a)\cong\mathsf{Hylo}(b,a)\hfill$

By the Yoneda lemma, if an algebra $a$ admits a relatively terminal coalgebra,
it must be unique up to unique isomorphism; hence, we may use the functional
notation $\nu(a)$ or $\nu(a)$ to denote _the_ coalgebra which is terminal
relative to $a$. Similarly, we will write $\mu(b)$ or $\mu(b)$ for _the_
algebra which is initial relative to $b$.

However, note that so far we have no guarantee as to the existence of $\nu(a)$
and $\mu(b)$; we will adopt the convention that the use of an expression
$\nu(a)$ or $\mu(b)$ carries with it the implicit assumption that such an
object exists. So for example, Proposition 2.5 should be read as “For any
algebra $a$, _if a relatively terminal coalgebra exists_ , it is a fixed point
of $F$”. In Theorem 2.14, we will show that under appropriate conditions,
$\mu$ and $\nu$ define total functors.

###### Remark 2.3

Let

$\hfill\mathsf{Hylo}(-,=)\colon F\text{-}\mathsf{Coalg}^{\mathrm{op}}\times
F\text{-}\mathsf{Alg}\to\mathsf{Set}\hfill$

be the functor which sends a coalgebra $b$ and an algebra $a$ to the set of
coalgebra-to-algebra morphisms from $b$ into $a$. The above definition may be
rephrased as follows: $\nu(a)$ is a representing object for
$\mathsf{Hylo}(-,a)$ and $\mu(b)$ is a representing object for
$\mathsf{Hylo}(b,-)$.

###### Remark 2.4

As in the Yoneda lemma, of central importance are the maps
$\eta=\psi(\text{id}_{\\_}{\mu(b)})$ and
$\epsilon=\phi(\text{id}_{\\_}{\nu(a)})$. It can easily be verified that for
$f:a\to\mu(b)$ and $g:\nu(a)\to b$, we have the equalities

$\displaystyle\psi(f)=f\circ\eta$ (2) $\displaystyle\phi(g)=\epsilon\circ g$
(3)

Perhaps surprisingly, the universal properties of $\mu(b)$ and $\nu(a)$ imply
that they are always fixed points for $F$.

###### Proposition 2.5

For any algebra $a$, the coalgebra $\nu(a):\nu A\to F\nu A$ is a fixed point
of $F$. Similarly, for any coalgebra $b$, the algebra $\mu(b):F\mu(b)\to\mu B$
is a fixed point of $F$.

###### Proof 2.6

This proposition resembles Lambek’s lemma; indeed, it is possible to exhibit
$\mu(b)$ as an initial algebra for a well-chosen functor
$F_{\\_}b:\mathsf{C}/B\to\mathsf{C}/B$. This is (up to duality) the approach
taken in [1]. For concreteness, We have chosen to give an explicit proof. We
prove that $\mu(b)$ is a fixed point; the case for $\nu(a)$ follows by
duality.

We wish to find an inverse $\beta$ to $\mu(b):F(\mu B)\to\mu B$. Since $F(\mu
B)$ carries the algebra structure $F(\mu(b)):FF(\mu B)\to F(\mu B)$, it
suffices to find a ca-morphism $b\to F(\mu(b))$. This is given by the
following diagram:

${FB}$${FFB}$${FF\mu B}$${B}$${FB}$${F\mu
B}$$\scriptstyle{Fb}$$\scriptstyle{FF\eta}$$\scriptstyle{F\mu(b)}$$\scriptstyle{b}$$\scriptstyle{b}$$\scriptstyle{F\eta}$$\scriptstyle{Fb}$

This yields an algebra morphism $\beta:\mu B\to F\mu B$ such that

$\beta\eta=\psi(\beta)=(F\eta)b$ (4)

It remains to show that $\beta$ is a two-sided inverse to $\mu(b)$. Consider
the composite $\mu(b)\circ\beta:\mu B\to\mu B$. We claim that under the
correspondence $\psi$, this composite corresponds to $\eta$; since $\psi$ is
bijective, and $\text{id}_{\\_}{\mu B}$ corresponds to $\eta$ by definition,
this yields $\mu(b)\circ\beta=\text{id}_{\\_}{\mu B}$. To verify, we use
equality 2:

${\mu B}$${FB}$${F\mu B}$${B}$${\mu
B}$$\scriptstyle{\beta}$$\scriptstyle{F\eta}$$\scriptstyle{\mu(b)}$$\scriptstyle{\eta}$$\scriptstyle{b}$$\scriptstyle{\eta}$

The top square is equation 4, and the bottom square commutes since $\eta$ is a
ca-morphism.

We may now conclude that $\mu(b)\circ\beta=\text{id}_{\\_}{\mu B}$. To show
that $\beta\circ\mu(b)=\text{id}_{\\_}{F\mu B}$, we simply note that $\beta$
is an algebra morphism, and hence

${F\mu B}$${FF\mu B}$${\mu B}$${F\mu
B}$$\scriptstyle{F\beta}$$\scriptstyle{\mu(b)}$$\scriptstyle{F\mu(b)}$$\scriptstyle{\beta}$

commutes. The composite $F\mu(b)\circ F\beta=F(\mu(b)\circ\beta)$ is equal to
$F\text{id}_{\\_}{\mu B}=\text{id}_{\\_}{F\mu B}$ as already shown, so we also
have $\beta\circ\mu(b)=\text{id}_{\\_}{F\mu B}$.

We now give an adjunction characterizing relative fixed points.

###### Theorem 2.7

Let $\mathsf{C}$ be a category, and $F:\mathsf{C}\to\mathsf{C}$ an
endofunctor. Assume that every $F$-algebra has a relatively terminal
coalgebra, and every $F$-coalgebra has a relatively initial algebra. Then
$\nu:F\text{-}\mathsf{Alg}\to F\text{-}\mathsf{Coalg}$ and
$\mu:F\text{-}\mathsf{Coalg}\to F\text{-}\mathsf{Alg}$ are the object parts of
two adjoint functors

${F\text{-}\mathsf{Coalg}}$${F\text{-}\mathsf{Alg}}$$\scriptstyle{\mu}$${\bot}$$\scriptstyle{\nu}$

###### Proof 2.8

For the action of $\nu$ on morphisms, consider an algebra morphism

${FA}$${FA^{\prime}}$${A}$${A^{\prime}}$$\scriptstyle{Ff}$$\scriptstyle{a}$$\scriptstyle{a^{\prime}}$$\scriptstyle{f}$

Then we obtain a ca-morphism

${F\nu A}$${FA}$${FA^{\prime}}$${\nu
A}$${A}$${A^{\prime}}$$\scriptstyle{F\epsilon}$$\scriptstyle{a}$$\scriptstyle{Ff}$$\scriptstyle{Fa^{\prime}}$$\scriptstyle{\nu(a)}$$\scriptstyle{\epsilon}$$\scriptstyle{f}$

So, we can set $\nu(f)$ to be $\phi^{-1}(f\circ\epsilon)$. It is easy to check
that this preserves composition. The action of $\mu$ on morphisms is similar.

To see that $\mu\dashv\nu$, simply consider the composite isomorphism

$F\text{-}\mathsf{Alg}(\mu(b),a)\cong\mathsf{Hylo}(b,a)\cong
F\text{-}\mathsf{Coalg}(b,\nu(a))$

We end this section with the following remark:

###### Remark 2.9

It is easy to see that if $b:B\to FB$ is an isomorphism, then $b^{-1}:FB\to B$
is initial relative to $b$; hence, $\mu(b)=b^{-1}$. Similarly,
$\nu\alpha=\alpha^{-1}$ whenever $\alpha:FA\to A$ is an isomorphism. From
this, it follows that the monad $\mu\nu:F\text{-}\mathsf{Coalg}\to
F\text{-}\mathsf{Coalg}$ maps $b:B\to FB$ to

$(\mu(b))^{-1}:\mu B\to F\mu B$

### Existence of the Adjunction

In this section, we offer sufficient conditions on the endofunctor
$F:\mathsf{C}\to\mathsf{C}$ for $\mu$ and $\nu$ to define total functors. We
will require that $\mathsf{C}$ is a locally presentable category and that $F$
is an accessible endofunctor. We quickly recall the relevant definitions; for
a full explanation of locally presentable categories, see [13].

###### Definition 2.10

Let $\lambda$ be a regular infinite cardinal. $\mathsf{C}$ is a
$\lambda$-filtered category if every class of morphisms with size less than
$\lambda$ has a cocone in $\mathsf{C}$. The colimit of a functor
$D:\mathsf{C}\to\mathsf{D}$ is a $\lambda$-filtered colimit if the category
$\mathsf{C}$ is $\lambda$-filtered.

###### Definition 2.11

An object $A$ of a category $\mathsf{C}$ is $\lambda$-presentable if the
representable functor $\mathrm{Hom}(A,-)$ preserves $\lambda$-filtered
colimits.

###### Definition 2.12

A category $\mathsf{C}$ is locally $\lambda$-presentable if

  * •

$\mathsf{C}$ is cocomplete,

  * •

There are up to isomorphism only a set of $\lambda$-presentable objects, and

  * •

every object in $\mathsf{C}$ is colimit of $\lambda$-presentable objects.

A category $\mathsf{C}$ is locally presentable if it is $\lambda$-locally
presentable for some infinite cardinal $\lambda$. $\mathsf{C}$ is locally
finitely presentable if it is $\omega$-presentable for the first infinite
cardinal $\omega$.

###### Definition 2.13

A functor $F\colon\mathsf{C}\to\mathsf{C}$ is $\lambda$-accessible if it
preserves $\lambda$-filtered colimits. $F$ is accessible if it preserves
$\lambda$-filtered colimits for some $\lambda$.

We now state the main theorem of the section:

###### Theorem 2.14

Let $\mathsf{C}$ be a locally presentable category and
$F:\mathsf{C}\to\mathsf{C}$ an accessible endofunctor. Then the relatively
initial fixed point $\mu(b)$ exists for any coalgebra $b$ and the relatively
terminal fixed point $\nu(a)$ exists for any coalgebra $a$.

###### Proof 2.15

Fix a regular cardinal $\lambda$ such that $\mathsf{C}$ is
$\lambda$-presentable, and $F$ is $\lambda$-accessible. Because $\mathsf{C}$
is a locally accessible category, it has colimits of all chains. Hence, given
a coalgebra $b:B\to FB$, we can build up the chain

${B}$${F(B)}$${F^{2}(B)}$${\cdots}$$\scriptstyle{b}$$\scriptstyle{Fb}$$\scriptstyle{F^{2}(b)}$
(5)

and continue it until the $\lambda$’th iterate
$F^{\lambda}(B)=\mathrm{colim}_{\\_}{i<\lambda}F^{i}(B)$. Since the chain of
length $\lambda$ is $\lambda$-filtered (recall that $\lambda$ is regular), we
know that $F$ preserves this colimit, and hence the chain converges to a
universal cocone $m:M\cong FM$, with inclusion maps $j_{\\_}i:F^{i}B\to M$. It
remains to show that $m^{-1}$ is relatively initial for $b$.

Given a ca-morphism

${B}$${F(B)}$${A}$${F(A)}$$\scriptstyle{f}$$\scriptstyle{b}$$\scriptstyle{F(f)}$$\scriptstyle{a}$

we present $A$ as a cocone $(c_{\\_}i:F^{i}B\to A)_{\\_}{i<\lambda}$ over
chain 5. We proceed by ordinal recursion: for $i=0$, we have $c_{\\_}0=f:B\to
A$. If $i+1$ is a successor, we set

${F^{i}B}$${F^{i+1}B}$${A}$${FA}$$\scriptstyle{F^{i}b}$$\scriptstyle{c_{\\_}i}$$\scriptstyle{Fc_{\\_}i}$$\scriptstyle{c_{\\_}{i+1}}$$\scriptstyle{a}$

Finally, at successor stages $\alpha$, we have already built up a cocone
$(c_{\\_}i:F^{i}B\to A)_{\\_}{i<\alpha}$, hence since $F^{\alpha}B$ is defined
as the colimit over the stages $i<\alpha$, we get a unique mediating arrow
$c_{\\_}\alpha:F^{\alpha}B\to A$, with

${F^{i}B}$${F^{i^{\prime}}B}$${F^{\alpha}B}$${A}$$\scriptstyle{c_{\\_}i}$$\scriptstyle{c_{\\_}{i^{\prime}}}$$\scriptstyle{c_{\\_}\alpha}$

Then too, we get a colimit map $\hat{f}:M\to A$ such that $\hat{f}\circ
j_{\\_}i=c_{\\_}i$. We will verify that $\hat{f}$ is an algebra morphism -
i.e., $\hat{f}\circ m^{-1}=a\circ Ff$. This is of course equivalent to
$\hat{f}=a\circ Ff\circ m$, and by the colimit property of $M$, it suffices to
show that $\hat{f}\circ j_{\\_}i=a\circ Ff\circ m^{-1}\circ j_{\\_}i$ for all
$i<\lambda$. This follows by an easy ordinal induction: if $\alpha$ is a limit
ordinal, and it holds for all $i<\alpha$, then it also holds for $\alpha$, as
$F^{\alpha}B$ is a colimit over the earlier stages. At successor stages $i+1$,
where it holds for $i$, we get

${F^{i+1}B}$${M}$${M}$${FM}$${A}$${FA}$$\scriptstyle{c_{\\_}{i+1}}$$\scriptstyle{Fj_{\\_}{i}}$$\scriptstyle{j_{\\_}{i+1}}$$\scriptstyle{j_{\\_}{i+1}}$$\scriptstyle{m}$$\scriptstyle{\hat{f}}$$\scriptstyle{F\hat{f}}$$\scriptstyle{a}$

and here the inner square commutes, as

$\hfill c_{\\_}{i+1}=a\circ F(c_{\\_}{i})=a\circ F\hat{f}\circ
Fj_{\\_}{i}\hfill$

Next, assume that we have an algebra morphism $g:B^{\prime}\to A$. Then we
obtain a ca-morphism $g\circ j_{\\_}0:B\to A$ via

${B}$${FB}$${M}$${FM}$${A}$${FA}$$\scriptstyle{b}$$\scriptstyle{j_{\\_}0}$$\scriptstyle{Fj_{\\_}0}$$\scriptstyle{m}$$\scriptstyle{g}$$\scriptstyle{Fg}$$\scriptstyle{a}$

We now have the two operations
$\hat{(-)}:\mathsf{Hylo}(b,a)\to\mathsf{Alg}(m^{-1},a)$ and $(-)\circ
j_{\\_}0:\mathsf{Alg}(m^{-1},a)\to\mathsf{Hylo}(b,a)$. We quickly verify that
these two operations are inverse.

In one direction, it is clear that $j_{\\_}0\circ\hat{f}=f$ by construction of
$\hat{f}$.

In the other direction, we need to show that $g$ is a mediating arrow for the
cone induced by $g\circ j_{\\_}0:B\to A$. We prove by induction that $g\circ
j_{\\_}i=c_{\\_}i$ for all $i$. For $i=0$, this is the definition. If it holds
for $i$, then for $i+1$, we get

${F^{i}B}$${M}$${FM}$${A}$${FA}$$\scriptstyle{j_{\\_}{i+1}}$$\scriptstyle{Fj_{\\_}i}$$\scriptstyle{m}$$\scriptstyle{g}$$\scriptstyle{Fg}$$\scriptstyle{a}$

By induction, the right-hand composition is equal to $a\circ F(c_{\\_}i)$,
which is by definition equal to $c_{\\_}{i+1}$. For limit stages $\alpha$, it
follows by the colimit condition. So $g$ is the unique mediating arrow, and
hence we get $\widehat{(j_{\\_}0\circ g)}=g$.

This shows that $\mathsf{Hylo}(b,a)\cong F\text{-}\mathsf{Alg}(m^{-1},a)$, and
hence $m$ is initial relative to $b$. Since $b$ was arbitrary, we now know
that $\mu(b)$ exists for all $b$.

To show the existence of $\nu$ we use the (dual of) the special adjoint
functor theorem (e.g. [14, Thm. 4.58]). By [13, Exercise 2j],
$F\text{-}\mathsf{Coalg}$ is locally presentable and by [13, Corr. 2.75] so is
the category $F\text{-}\mathsf{Alg}$. By [13, Thm. 1.58], both these
categories are co-wellpowered. The functor $\mu$ preserves colimits, because
it is constructed as a colimit and colimits distribute over themselves.
Therefore, by the special adjoint functor theorem, $\mu$ has right adjoint
$\nu$; to see that that $\nu(a)$ is terminal relative to $a$, consider the
natural equivalences

$F\text{-}\mathsf{Coalg}(b,\nu(a))\cong
F\text{-}\mathsf{Alg}(\mu(b),a)\cong\mathsf{Hylo}(b,a).$

As a special case, we may consider functors that preserve both limits and
colimits of shape $\omega$.

###### Theorem 2.16

Suppose $C$ is a category with limits of $\omega^{\mathrm{op}}$-chains and
colimits of $\omega$-chains and $F$ is a functor that preserves them. Then
$\mu$ and $\nu$ may be calculated as

$\hfill\mu(b)\cong\mathrm{colim}(\leavevmode\hbox to172.2pt{\vbox
to18.56pt{\pgfpicture\makeatletter\hbox{\hskip 86.09958pt\lower-9.32843pt\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\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\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}{-86.09958pt}{-9.22859pt}\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.34894pt\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&\hfil\hskip 40.14754pt\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}{-11.84203pt}{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(B)}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
16.14757pt\hfil&\hfil\hskip 41.54755pt\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.24203pt}{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^{2}(B)}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
17.54758pt\hfil&\hfil\hskip 32.05551pt\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.75pt}{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{${\cdots}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.05554pt\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{-69.2017pt}{-6.72859pt}\pgfsys@lineto{-46.0017pt}{-6.72859pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-45.80171pt}{-6.72859pt}\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}{-58.9038pt}{-4.37582pt}\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{b}$}
}}\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{-12.9066pt}{-6.72859pt}\pgfsys@lineto{10.29341pt}{-6.72859pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.4934pt}{-6.72859pt}\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.3455pt}{-4.37582pt}\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{Fb}$}
}}\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{46.18852pt}{-6.72859pt}\pgfsys@lineto{69.38853pt}{-6.72859pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{69.58852pt}{-6.72859pt}\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.02739pt}{-2.62582pt}\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^{2}(b)}$} }}\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}})\hfill$ (6)
$\hfill\nu(a)\cong\lim(\leavevmode\hbox to170.44pt{\vbox
to18.56pt{\pgfpicture\makeatletter\hbox{\hskip 85.21939pt\lower-9.32843pt\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\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\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}{-85.21939pt}{-9.22859pt}\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.05554pt\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.75pt}{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}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
8.05554pt\hfil&\hfil\hskip 39.85414pt\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}{-11.54863pt}{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(A)}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
15.85417pt\hfil&\hfil\hskip 41.25415pt\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}{-12.94864pt}{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^{2}(A)}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
17.25418pt\hfil&\hfil\hskip 32.05551pt\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.75pt}{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{${\cdots}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.05554pt\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{-45.30833pt}{-6.72859pt}\pgfsys@lineto{-68.50835pt}{-6.72859pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-68.70833pt}{-6.72859pt}\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}{-58.95837pt}{-4.37582pt}\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{a}$}
}}\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.39998pt}{-6.72859pt}\pgfsys@lineto{-12.80003pt}{-6.72859pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-13.00002pt}{-6.72859pt}\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.98688pt}{-4.37582pt}\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{Fa}$}
}}\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{68.90831pt}{-6.72859pt}\pgfsys@lineto{45.7083pt}{-6.72859pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{45.50832pt}{-6.72859pt}\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}{48.79922pt}{-2.62582pt}\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^{2}(a)}$} }}\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}})\hfill$

In particular, $\mu(b)$ and $\nu(a)$ exist for all coalgebras $b$ and all
algebras $a$.

###### Remark 2.17

Let $1$ be the terminal object of $\mathsf{C}$ and let $0$ be the initial
object. Then there is a unique algebra $1:F1\to 1$ and $\nu(1)$ is the
terminal coalgebra. Similarly, the initial algebra is given by $\mu(0)$ for
the unique coalgebra $0:0\to F0$.

Before moving on to the next section we state a corollary about recursive
coalgebras and corecursive algebras.

###### Definition 2.18

An $F$-algebra $a$ is corecursive if for every $F$-coalgebra $b$ there is a
unique ca-morphism from $b\to a$. Dually, an $F$-coalgebra $b$ is recursive if
for any $F$-algebra $a$, there is a unique ca-morphism $b\to a$.

Recursivity of a coalgebra relates to the termination of that coalgebra when
thought of as a program (c.f. [6]). The following corollary connects
(co)recursivity to the $\mu-\nu$ adjunction:

###### Corollary 2.19

A coalgebra $b:B\to FB$ for which $\mu(b)$ exists is recursive if and only if
$\mu(b)$ is initial; similarly, an algebra $a:FA\to A$ for which $\nu(a)$
exists is corecursive if and only if $\nu(a)$ is terminal.

###### Proof 2.20

This can be easily read off: $b$ is recursive if and only if
$\mathsf{Hylo}(b,a)$ always has a unique element, and $\mu(b)$ is initial if
and only if $F\text{-}\mathsf{Alg}(\mu(b),a)$ always has a unique element.
Since

$\mathsf{Hylo}(b,a)\cong F\text{-}\mathsf{Alg}(\mu(b),a)$

by definition, the equivalence follows. The second statement follows
analogously.

##  3 Concrete Constructions of Relative Fixed Points

In this section we provide several concrete constructions of relative fixed
points, using a presentation of $\mu$ and $\nu$ based on (co)free
(co)algebras. In Examples 3.7, 3.8 we explore relative fixed points of
polynomial functors and discuss their interpretations. Next, in Proposition
3.10, we construct a downward fixed point which classifies cartesian
subcoalgebras in the sense of [10]. In Proposition 3 we illustrate how the
Sierpinski carpet may be constructed as a relatively terminal coalgebra.
Lastly, we show in Example 3.18, how the depleted version of the adjunction,
that is the Galois connection between post-fixed points and pre-fixed points
mentioned in the introduction, may be useful for something called the safety
problem.

###### Proposition 3.1

For a polynomial functor $F:\mathsf{Set}\to\mathsf{Set}$, each coalgebra
admits a relatively initial algebra, and every algebra admits a relatively
terminal coalgebra.

###### Proof 3.2

Theorem 2.14 guarantees their existence if $F$ is accessible. Let
$F=\sum_{\\_}{i\in I}y^{X_{\\_}i}$, and let $\lambda$ be a regular cardinal,
such that $\lambda\geq\sup\\{|X_{\\_}i|\mid i\in I\\}$. Then each
$y^{X_{\\_}i}$ is $\lambda$-accessible, and hence so is their coproduct $F$.

In order to give explicit descriptions for $\mu$ and $\nu$ on $\mathsf{Set}$,
we exploit the fact that free algebras and cofree coalgebras for polynomial
functors on $\mathsf{Set}$ have elegant characterizations:

###### Proposition 3.3

Let $F:\mathsf{Set}\to\mathsf{Set}$ be the polynomial functor given by
$FX=\sum_{\\_}{\sigma\in\Sigma}X^{\mathsf{ar}(\sigma)}$. Then,

  1. (i)

the free $F$-algebra on $X$, denoted $T^{\Sigma}(X)$, is given by the set of
finite $\Sigma$-branching trees with leaves labeled by elements of $X$.
Equivalently, $T^{\Sigma}(X)$ is the algebra of $\Sigma$-terms over $X$, known
from universal algebra (see [15] for further description of free algebras, as
well as quotients of $F$-algebras).

  2. (ii)

The cofree $F$-coalgebra on $X$, denoted $C^{\Sigma}(X)$, is given by the set
of finite and infinite $\Sigma$-branching trees with internal nodes labeled by
elements of $X$.

In order to make use of (co)free (co)algebras in describing $\mu$ and $\nu$,
we employ the following construction:

###### Theorem 3.4

Let $\mathsf{C}$ be a category, and $F:\mathsf{C}\to\mathsf{C}$ an
endofunctor.

  * •

Assume that every object $X$ in $\mathsf{C}$ admits a free algebra $T^{F}X$,
with unit $\eta:X\to T^{F}X$ and free algebra structure $\alpha:FT^{F}X\to
T^{F}X$. Then $\mu(b)$ is given by the coequalizer of the diagram

${T^{F}(B)}$${T^{F}(B)}$$\scriptstyle{id}$$\scriptstyle{\mathsf{unfold}}$

in the category of $F$-algebras and where $\mathsf{unfold}$ is the free
extension of the following map to $T^{F}(B)$

$B\xrightarrow{b}FB\xrightarrow{F\eta}FT^{F}(B)\xrightarrow{\alpha_{\\_}B}T^{F}(B)$

  * •

Assume that every object $X$ in $\mathsf{C}$ admits a cofree coalgebra
$C^{F}X$, with counit $\eta:C^{F}X\to X$ and cofree coalgebra structure
$\gamma:C^{F}X\to FC^{F}X$. Then $\nu(a)$ is given by the equalizer of the
diagram

${C^{F}(A)}$${C^{F}(A)}$$\scriptstyle{id}$$\scriptstyle{\mathsf{pred}}$

in the category of $F$-coalgebras where $\mathsf{pred}$ is the coextension of
the following map to $C^{F}(A)$

$C^{F}(A)\xrightarrow{\gamma_{\\_}A}FC^{F}(A)\xrightarrow{F\epsilon}FA\xrightarrow{a}A$

###### Proof 3.5

We only prove the statement for $\mu$, since the statement for $\nu$ follows
by duality. Let $m:FM\to M$ be the coequalizer of id and $\mathsf{unfold}$,
with quotient map $q:T^{F}(B)\to M$. Let $a:FA\to A$ be an algebra, and assume

${FB}$${FA}$${B}$${A}$$\scriptstyle{Ff}$$\scriptstyle{a}$$\scriptstyle{b}$$\scriptstyle{f}$

is a coalgebra-to-algebra morphism. We wish to find an algebra morphism
$\tilde{f}:M\to A$ such that $\tilde{f}\circ(q\eta)=f$. Since $T^{F}(B)$ is
the free $F$-algebra on $B$, there is a unique algebra morphism
$\check{f}:T^{F}(B)\to A$ with $\check{f}\circ\eta=f$; it suffices to show
that $\check{f}$ factors through $q$, or equivalently, that $\check{f}$
coequalizes id and $\mathsf{unfold}$.

Since $\check{f}\circ\text{id}=\check{f}$ and $\check{f}\circ\mathsf{unfold}$
are both algebra morphisms $T^{F}B\to A$, we only have to show that they agree
on the generators; i.e.,

$\hfill\hat{f}\circ\eta=\hat{f}\circ\mathsf{unfold}\circ\eta\hfill$ (7)

To this end, consider the following diagram.

${B}$${FB}$${{T^{F}(B)}}$${{T^{F}(B)}}$${{FT^{F}(B)}}$${A}$${FA}$$\scriptstyle{\check{f}}$$\scriptstyle{\check{f}}$$\scriptstyle{\eta}$$\scriptstyle{\mathsf{unfold}}$$\scriptstyle{f}$$\scriptstyle{a}$$\scriptstyle{F\check{f}}$$\scriptstyle{F\eta}$$\scriptstyle{b}$$\scriptstyle{\alpha_{\\_}B}$$\scriptstyle{Ff}$${(*)}$

Facet $(*)$ is equation 7, which is to be established. The outer square
commutes, since by assumption $f$ is a coalgebra-to-algebra morphism. The top
right square is the definition of $\mathsf{unfold}$, and the bottom right
square commutes as $\hat{f}$ is an algebra morphism.

Unpacking the above equalizers and coequalizers in the case of polynomial
functors on $\mathsf{Set}$ gives the following corollary. The proof of this
corollary is left to the reader.

###### Proposition 3.6

Let $F:\mathsf{Set}\to\mathsf{Set}$ be a polynomial functor, say
$FX=\sum_{\\_}{\sigma\in\Sigma}X^{\mathsf{ar}(\sigma)}$.

  1. (i)

If $b:B\to FB$ is an $F$-coalgebra, then $\mu(b)$ is given by

$\hfill T^{\Sigma}(B)/\\{x\sim b(x)\\}\hfill$

  2. (ii)

If $a:FA\to A$ is an $F$-algebra, then $\nu(a)$ is given by

$\hfill\\{t\in C^{\Sigma}(A)\mid\text{ if }\leavevmode\hbox to78.29pt{\vbox
to47.97pt{\pgfpicture\makeatletter\hbox{\hskip 39.01657pt\lower-5.48578pt\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\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.85764pt}{-2.15277pt}\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{{$x$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}{-35.68356pt}{32.461pt}\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{{$y_{\\_}1$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}{20.96155pt}{32.211pt}\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{{$y_{\\_}k$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}{-3.75pt}{31.64322pt}\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{{$\dots$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-6.40182pt}{7.68219pt}\pgfsys@lineto{-22.05093pt}{26.46103pt}\pgfsys@stroke\pgfsys@invoke{
} {}{{}}{}
{}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{6.40182pt}{7.68219pt}\pgfsys@lineto{22.05093pt}{26.46103pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.85706pt}{17.76407pt}\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{{$\sigma$}}
}}\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}}\text{ is a height one
subtree of }t\text{, then }x=a(\sigma(\vec{y}))\\}\hfill$

This proposition also shows a connection between the $\nu$-construction, and
coequations. To illustrate this, consider what happens in the
$\mu$-construction: A coalgebra $b:B\to FB$ is treated as a ‘(flatly)
recursive set of equations’ $x\sim b(x)$. Then this set of equations can be
used construct a quotient $\mu(b)$ of the free $F$-algebra. Comparing this to
the coalgebra-to-algebra picture, it has been noted before that giving a
coalgebra-to-algebra morphism $b\to a$ is akin to solving the system of
equations presented by $b$ in the algebra $a$ . We propose that there is a
dual perspective: rather than solving the system of equations $b$ in $a$, one
could also see a coalgebra-to-algebra morphism as _solving the coequation $a$
in $b$_. To our knowledge, the ‘coequations-as-algebras’ perspective is new.
We can leverage $\nu$ to fit it into the wider spectrum of coequational logic.
As demonstrated in [16], the most general definition of a coequation is ‘a
subcoalgebra of a cofree coalgebra’. Point (ii) of proposition 3.6 then shows
how each algebra gives rise to a canonical coequation.

As a final note, we should highlight an important difference between our
current approach to (co)equations, and the one common in universal
(co)algebras: in the latter, the main notion is that of _satisfaction_ of
(co)equations, whereas we focus on _solving_ (co)equations. A coequation
$E\subseteq C^{\Sigma}(X)$ is satisfied by $b:B\to FB$ if every coalgebra-to-
algebra morphism $B\to C^{\Sigma}(X)$ factors through $E$. It can quickly be
seen that for coequations of the form $\nu(a)$, a coalgebra $b:B\to FB$
satisfies $\nu(a)$ if and only if _every_ map $B\to A$ is a coalgebra-to-
algebra morphism. Such a situation is exceedingly rare. This also shows that
only particular coequations can be described as $\nu(a)$.

There are ubiquitous examples of the above theorems.

###### Example 3.7

Let $F:\mathsf{Set}\to\mathsf{Set}$ be the functor given by
$FX=\\{\times,\checkmark\\}\times X$. Let $a$ be the algebra $a\colon F(X)\to
X$ with carrier $X=\\{0,1\\}$ given by

$\hfill(\checkmark,s)\mapsto s\text{ and }(\times,s)\mapsto 1-s\hfill$

where $s$ is either $0$ or $1$. The algebra may be depicted as

${0}$${1}$$\scriptstyle{\times}$$\scriptstyle{\checkmark}$$\scriptstyle{\times}$

Then $\nu(a)$ has a carrier given by

$\hfill\\{\begin{pmatrix}u_{\\_}1\\\
s_{\\_}1\end{pmatrix}\begin{pmatrix}u_{\\_}2\\\
s_{\\_}2\end{pmatrix}\begin{pmatrix}u_{\\_}3\\\
s_{\\_}3\end{pmatrix}\cdots\in(\\{\times,\checkmark\\}\times
X)^{\omega}\quad|\quad u_{\\_}i=\times\implies s_{\\_}i=s_{\\_}{i+1}\text{ and
}u_{\\_}i=\checkmark\implies s_{\\_}i=1-s_{\\_}{i+1}\\}\hfill$

i.e. the subset of streams in $(\\{\times,\checkmark\\})^{\omega}$ which
follow the action of $a$ _when read from right to left_. Given a coalgebra
$b:B\to\\{\times,\checkmark\\}\times B$, a coalgebra-to-algebra morphism may
represent a solution to the constraint represented by $a$. That is, we divide
the states of $B$ into two classes, such that the division ‘respects the
algebra structure on $A$’. If $m$ is such a marking, we obtain

${B}$${\\{\times,\checkmark\\}\times
B}$${\nu(a)}$${\\{\times,\checkmark\\}\times\nu(a)}$$\scriptstyle{\hat{m}}$$\scriptstyle{F{\hat{m}}}$

via the universal property of $\nu$. Intuitively, $\hat{m}$ maps a state $x$
to the stream of ‘tags and classes’ that are observed when running $b$
forwards. The constraint on $m$ then states that whenever a $\checkmark$ is
observed, the class must change, whereas whenever a $\times$ is observed, the
class must stay the same. A marking satisfying this constraint exists, if and
only if on each cycle in $B$, the number of $\checkmark$’s is even.

###### Example 3.8

Consider the coalgebra $b$ for the functor $FX=\\{\times,\checkmark\\}\times
X^{\\{a,b\\}}$ as depicted in figure 2

$q_{\\_}0$$q_{\\_}1$$q_{\\_}2$abba,b Figure 2:

with carrier given by $X=\\{q_{\\_}0,q_{\\_}1,q_{\\_}2\\}$. Then the carrier
of $\mu(b)$ is given by

$\frac{\text{ finite }\\{a,b\\}\text{ branching trees with
$\\{\times,\checkmark\\}$ labeling internal nodes and $X$ labeling
leaves}}{q_{\\_}0\cong
q_{\\_}1\xleftarrow{a}\times\xrightarrow{b}q_{\\_}2,q_{\\_}1\cong
q_{\\_}0\xleftarrow{a}\times\xrightarrow{b}q_{\\_}1,q_{\\_}2\cong
q_{\\_}2\xleftarrow{a}\checkmark\xrightarrow{b}q_{\\_}2}$

where the quotient denotes a quotient in $\mathsf{Set}$, i.e. the set in the
numerator modulo the smallest congruence relation satisfying the tree
equations in the denominator. Intuitively, $\mu(b)$ has all finite trees but
leaves may be replaced with the equations in the numerator in a recursive and
transitive way. One may also see it as terms over the 2 binary operations
$\times$ and $\checkmark$ in the three unknowns
$\\{q_{\\_}0,q_{\\_}1,q_{\\_}2\\}$, where $q_{\\_}0,q_{\\_}1,q_{\\_}2$ satisfy
a mutual recursive relationship.

###### Example 3.9

Let $F:\mathsf{Set}\to\mathsf{Set}$ be the polynomial functor given by
$FX=\sum_{\\_}{\sigma\in\Sigma}X^{\mathsf{ar}(\sigma)}$. Since polynomial
functors preserve pullbacks, it follows from Corollary 3.2 in [17] that
$F\text{-}\mathsf{Coalg}$ is an (elementary) topos. Its subobject classifier
$\Omega$ is the coalgebra of ‘non-decreasing $\Sigma$-trees’; that is, the
points of $\Omega$ are $\mathbf{2}$-labeled $\Sigma$-trees, where the label of
a child may not be smaller than the label of its parent.

$\Omega$ is not a fixed point unless $F$ is trivial; however, there is a
subcoalgebra $\Omega_{\\_}{\mathsf{cart}}$ which is a fixed point, and arises
as $\nu$ of a well-chosen algebra. Consider the algebra
$\bigwedge:F\mathbf{2}\to\mathbf{2}$, explicitly

$\hfill\bigwedge:\sigma(x_{\\_}1,\dots,x_{\\_}n)\mapsto\begin{cases}1&x_{\\_}i=1\text{
for all }i=1,\dots,n\\\ 0&\text{ otherwise}\end{cases}\hfill$

Then $\nu(\bigwedge)$ is a subcoalgebra of $\Omega$; it consists of those non-
decreasing $\Sigma$-trees where zeroes ‘cannot disappear’, i.e. if a node is
labeled with $0$, at least one of its children is labeled with $0$.

$\Omega_{\\_}{\mathsf{cart}}$ satisfies a universal property similar to the
subobject classifier in $F\text{-}\mathsf{Coalg}$; but instead of classifying
_all_ subcoalgebras, it classifies only the _cartesian_ subcoalgebras i.e.,
those subcoalgebras $s:S\leq X$ such that the square

${S}$${X}$${FS}$${FX}$$\scriptstyle{s}$$\scriptstyle{Fs}$

is a pullback square. Explicitly, that means that there is a map
$\top:Z\to\Omega_{\\_}\mathsf{cart}$ (with $Z$ the terminal coalgebra), such
that for each coalgebra $X$ and each cartesian subobject $S\leq X$, there is a
unique map $s:X\to\Omega_{\\_}\mathsf{cart}$ such that

${S}$${Z}$${X}$${\Omega_{\\_}\mathsf{cart}}$$\scriptstyle{\top}$$\scriptstyle{s}$

is a pullback square. Ordinary subobjects are understood as ‘forward stable
subsets’: they are subsets $S$ such that if $s\in S$, then so are all the
successors of $s$. Cartesian subcoalgebras are those subsets which also
satisfy the converse implication: if all successors of $s$ are in $S$, then so
is $s$.

More formally, let $\xi:X\to FX$ be a coalgebra, and consider the ‘next-time
modality’ $\fullmoon:P(X)\to P(X)$ from [2], defined on a subobject $U\leq X$
via the pullback

${\fullmoon(U)}$${X}$${FU}$${FX}$$\scriptstyle{\xi}$

Then subcoalgebras are subsets $P\subseteq X$ such that $P\subseteq\fullmoon
P$; these are classified by $\Omega$. In [10], they show that Cartesian
subcoalgebras are fixed points for $\fullmoon$, i.e. they satisfy $P=\fullmoon
P$.

###### Proposition 3.10

$\Omega_{\\_}\mathsf{cart}$ classifies cartesian subcoalgebras.

###### Proof 3.11

We wish to show that $\Omega_{\\_}{\mathsf{cart}}=\nu(\bigwedge)$ classifies
cartesian subobjects. We first prove that cartesian subobjects are closed
under pullbacks.

Assume $P\leq X$ is a cartesian subcoalgebra. Let $y:Y\to X$ be a coalgebra
morphism. Then consider the following cube:

${Fy^{*}P}$${FY}$${FP}$${FX}$${y^{*}P}$${Y}$${P}$${X}$

Note that since $F$ preserves pullbacks, we obtain a unique arrow $y^{*}P\to
Fy^{*}P$. In the above cube, the front square is a pullback since $P$ is
strong, and the bottom square is a pullback by definition of $y^{*}$. Hence,
we see that taking the top and back square together, as in

${y^{*}P}$${Y}$${Fy^{*}P}$${FY}$${FP}$${FX}$

the outer square is a pullback. The bottom square is also a pullback, since
$F$ preserves pullbacks; hence the top square is a pullback, which shows that
$y^{*}P$ is cartesian.

Now consider the terminal object $Z$ in $F\text{-}\mathsf{Coalg}$; this is the
coalgebra of finite and infinite $\Sigma$-branching trees. We note that
$\top:Z\to\Omega$, which maps a tree $t$ to $t$ constantly labeled with $1$,
factors through $\Omega_{\\_}\mathsf{cart}$; and moreover $\top$ is a
_cartesian_ subcoalgebra of $\Omega_{\\_}\mathsf{cart}$. So whenever $P\leq X$
is a pullback of $\top:Z\to\Omega_{\\_}\mathsf{cart}$, $P$ is a cartesian
subcoalgebra. Uniqueness of classifiers $X\to\Omega_{\\_}\mathsf{cart}$
follows from uniqueness of classifiers $X\to\Omega$, so it suffices to show
that if $P\leq X$ is cartesian, there exists a classifier $\ulcorner
P\urcorner:X\to\Omega_{\\_}\mathsf{cart}$.

We know that
$F\text{-}\mathsf{Coalg}(X,\Omega_{\\_}\mathsf{cart})\cong\mathsf{Hylo}(X,\bigwedge)$,
so we may equivalently provide a coalgebra-to-algebra map $X\to 2$. We claim
that the characteristic function

$\hfill\chi_{\\_}P:x\mapsto\begin{cases}1&x\in P\\\ 0&\text{
otherwise}\end{cases}\hfill$

is a coalgebra-to-algebra morphism. For, consider an arbitrary $x\in X$. Let
$\xi(x)=\sigma(x_{\\_}1,\dots,x_{\\_}n)$. We consider two cases.

  1. (i)

If $x\in P$, then since $P$ is a subcoalgebra, we know $x_{\\_}i\in P$ for all
$i$; hence,

$\hfill\bigwedge(\sigma(\chi_{\\_}P(x_{\\_}1),\dots,\chi_{\\_}P(x_{\\_}n)))=\bigwedge(\sigma(1,\dots,1))=1=\chi_{\\_}P(x).\hfill$

  2. (ii)

If $x\notin P$, then it suffices to show that at least one of the $x_{\\_}i$
is also not in $P$. Assume towards a contradiction that $x_{\\_}i\in P$ for
all $i$. Then the following square commutes:

${\\{*\\}}$${X}$${FP}$${FX}$$\scriptstyle{*\mapsto
x}$$\scriptstyle{*\mapsto\sigma(x_{\\_}1,\dots,x_{\\_}n)}$$\scriptstyle{\xi}$

hence since $P$ was cartesian, we conclude that the map $*\mapsto x$ factors
through the inclusion $P\rightarrowtail X$. But this amounts to saying $x\in
P$, which is not the case.

We conclude that there is an $x_{\\_}i$ with $\chi_{\\_}P(x_{\\_}i)=0$, and
hence

$\hfill\bigwedge(\sigma(\chi_{\\_}P(x_{\\_}1),\dots,\chi_{\\_}P(x_{\\_}n)))=0=\chi_{\\_}P(x).\hfill$

So in both cases, we have $\bigwedge(F\chi_{\\_}P(\xi(x)))=\chi_{\\_}P(x)$,
which shows that $\chi_{\\_}P$ is a coalgebra-to-algebra morphism.

We conclude that there is a unique coalgebra morphism $\ulcorner
P\urcorner:X\to\Omega_{\\_}\mathsf{cart}$ such that
$\chi_{\\_}P=h\circ\ulcorner P\urcorner$, where
$h:\Omega_{\\_}\mathsf{cart}\to\mathbf{2}$ is the universal coalgebra-to-
algebra morphism, mapping a labeled $\Sigma$-tree to the label of its node. We
still need to show that $P$ is the pullback of $\top$ along $\ulcorner
P\urcorner$. Note, however, that

${Z}$${1}$${\Omega_{\\_}\mathsf{cart}}$${\mathbf{2}}$$\scriptstyle{\top}$$\scriptstyle{*\mapsto
1}$$\scriptstyle{h}$

is a pullback square, since if the root node of a non-decreasing $\Sigma$-tree
$t$ is labeled by 1, then so are all the other nodes in $t$, and hence $t$ is
in the image of $\top$. Hence, we can fill in the following diagram:

${P}$${Z}$${1}$${X}$${\Omega_{\\_}\mathsf{cart}}$${\mathbf{2}}$$\scriptstyle{\top}$$\scriptstyle{*\mapsto
1}$$\scriptstyle{\ulcorner
P\urcorner}$$\scriptstyle{\chi_{\\_}P}$$\scriptstyle{h}$

Here, the outer square is a pullback, since $\chi_{\\_}P$ classifies $P$ in
$\mathsf{Set}$, and we have just shown that the right-hand side is a pullback
as well. Therefore, the left-hand square is a pullback, which finishes the
proof.

###### Example 3.12

In _Sierpinski Carpet as a Final Coalgebra_ ([18]) Moss and Noquez provide a
construction of the Sierpinski carpet as a final coalgebra in a category of
‘square metric spaces’. In this section we recall this work and then show how
the downward fixed point construction $\nu$ gives a more direct way of
constructing the Sierpinski carpet as a final coalgebra.

###### Definition 3.13

Let $\blacksquare$ denote the set $[0,1]^{2}$ where $[0,1]$ is the real unit
interval. Let $\square$ denote the boundary of $\blacksquare$ or explicitly

$\hfill\square=\\{(i,r):i\in\\{0,1\\},r\in[0,1]\\}\cup\\{(r,i):r\in[0,1],i\in\\{0,1\\}\\}\hfill$

Let $\mathsf{MS}$ be the category whose objects are metric spaces with
diameter less than $2$ and whose morphisms are short maps
$f:(X,d)\to(X^{\prime},d^{\prime})$ i.e. a function $f:X\to X^{\prime}$ such
that $d(x,y)\leq d^{\prime}(f(x),f(y))$.

We are interested in two different metrics on $\square$:

  * •

The path metric $d_{\\_}p:\square\times\square\to\mathbb{R}$ with
$d_{\\_}p(x,y)$ given by the length of the shortest path in $\square$ between
$x$ and $y$.

  * •

The taxicab metric $d_{\\_}t:\square\times\square\to\mathbb{R}$ given by
$d_{\\_}t((s,r),(s^{\prime},r^{\prime}))=|s^{\prime}-s|+|r^{\prime}-r|$.

###### Definition 3.14

A square metric space is a metric space $(X,d)$ equipped with an injective
function $S:\square\hookrightarrow X$ such that for all $x,y\in\square$,

$\hfill d_{\\_}t(x,y)\leq d(S(x),S(y))\leq d_{\\_}p(x,y)\hfill$

A morphism of square metric spaces $f:(X,S)\to(X^{\prime},S^{\prime})$ is a
short map $f:X\to Y$ such that $S=S^{\prime}\circ f$. This defines a category
$\mathsf{SqMS}$ of square metric spaces and their morphisms.

$\square$ with the identity function is the initial algebra in square metric
spaces. We now define an endofunctor on square metric spaces for which the
Sierpinski carpet is a fixed point. We present the following definitions
informally. The full definitions may be found in [18].

###### Definition 3.15

Let $M$ be the set $\\{0,1,2\\}^{2}/(1,1)$. For a square metric space
$S:\square\to X$, $M\otimes X$ is eight copies of $X$ in a three-by-three grid
with the center removed. Mathematically, $M\otimes X$ is the cartesian product
$M\times X$ modulo the smallest equivalence relation which identifies the
boundaries of the subsquares with each other. We write $m\otimes x$ to denote
the equivalence class of $(m,x)$ in $M\otimes X$. We equip $M\otimes X$ with
the structure of a square metric space. $M\otimes X$ is equipped with a metric
given by scaling down the metric of $X$ by $\frac{1}{3}$ in each copy of $X$.
If $x$ and $y$ live in adjacent copies, their distance is set such that the
sum of distances to the shared boundary is minimized. For all other points,
the distance is set to $2$. There is a map $\square\to M\otimes X$ which maps
$\square$ injectively to the outer boundary. For a short map $f:X\to Y$, there
is a short map $M\otimes f:M\otimes X\to M\otimes Y$ given by $m\otimes
x\mapsto m\otimes f(x)$. This defines a functor

$\hfill M\otimes-\colon\mathsf{SqMS}\to\mathsf{SqMS}\hfill$

As shown in [18], $M\otimes-$ has an initial algebra. $\square$ is an initial
object in $\mathsf{SqMS}$ so the initial algebra may be found by taking the
colimit of the usual chain

$\hfill\square\to M\otimes\square\to M\otimes M\otimes\square\to\ldots\hfill$

As $\mathsf{SqMS}$ does not have a final object, we cannot construct a final
coalgebra by taking the limit of the dual of this chain. However, our
construction $\nu$ does not require a final object in the base category.

Figure 3: The Sierpinski carpet is the downward fixed point of the indicated
algebra

The square metric space $M\otimes\blacksquare$ is the same as $\blacksquare$
except with the middle removed. There is an algebra $a\colon
M\otimes\blacksquare\to\blacksquare$ given by the natural inclusion. As
illustrated in Figure 3, the Sierpinski carpet is given by the downward fixed
point $\nu$ applied to this algebra.

###### Proposition 3.16

The downward fixed point $\nu(\blacksquare\leftarrow M\otimes\blacksquare)$ is
the Sierpinski carpet.

###### Proof 3.17

Because every morphism in the chain

$\hfill\blacksquare\leftarrow M\otimes\blacksquare\leftarrow M\otimes
M\otimes\blacksquare\ldots\hfill$

is an injection, its limit is the intersection

$\hfill\bigcap_{\\_}{n=0}^{\infty}M^{n}\otimes\blacksquare\hfill$

This infinite intersection is the usual definition of the Sierpinski carpet.

We have seen that the Sierpinski carpet may be obtained in a more
straightforward way than in [18] using a relatively initial or terminal fixed
point. Other fractals may be generated as downward fixed points in a similar
way; for example one can imagine that the Sierpinski triangle may constructed
as a downward fixed point in a category of ‘triangular metric spaces’.

###### Example 3.18

In [19], the authors state the safety problem. This problem may be rephrased
in terms of the Galois connection

${Post(F)}$${Pre(F)}$$\scriptstyle{\mu_{\\_}F}$${\bot}$$\scriptstyle{\nu_{\\_}F}$

for a particular choice of $F$ and assuming that the set of initial states
forms a post-fixed point.

###### Definition 3.19

A transition system is a triple $(S,I,\delta)$ where $S$ is a set of states,
$I\subseteq S$, is a set of initial states, and $\delta\colon
S\to\mathcal{P}(S)$ is a transitition relation. Here $\mathcal{P}(S)$ is the
power-set of $S$ which is a complete lattice ordered by $\subseteq$. Let
$F:\mathcal{P}(S)\to\mathcal{P}(S)$ be the monotone function defined by
$F(X)=\bigcup_{\\_}{x\in X}\delta(x)$ and suppose that $I$ is a post fixed
point, i.e., $I\subseteq F(I)$. For a set $P\in\mathcal{P}(S)$, the the safety
problem for $(I,P,S,F)$ asks if $\mu_{\\_}F(I)\subseteq P$.

The idea here is that $\mu_{\\_}F(I)$ is the set of reachable states from $I$
and if $\mu_{\\_}F(I)\subseteq P$, then we say that $I$ is $P$-safe. Now
suppose that $P$ is a pre-fixed point $F(P)\subseteq P$. Then the adjunction
of this paper says that

$\mu_{\\_}F(I)\subseteq P\iff I\subseteq\nu_{\\_}F(P)$

While $\mu_{\\_}F(I)$ represents the states reachable from $I$,
$\nu_{\\_}F(P)$ are the states which never go above $P$. In this case the
adjunction suggests a strategy for verifying the safety problem. One may
answer the safety problem by simultaneously unfolding $I$ and $P$ using $F$.
In other words on the first step we check if $I\subseteq P$ if it is then we
check $F(I)\subseteq P$ and $I\subseteq F(P)$. If either of those are false,
then we know $I$ is not $P$-safe. If both are true then we continue to check
$F^{2}(I)\subseteq P$ and $I\subseteq F^{2}(P)$. We continue this process
indefinitely, checking to see if any of $F^{n}(I)\subseteq P$ and $I\subseteq
F^{n}(P)$ are false. If we can’t falsify any of these inclusions and we arrive
at a fixed point (either $\mu_{\\_}F(I)$ or $\nu_{\\_}F(P)$), then we know
that $I$ is $P$-safe.

A major limitation of this approach is that we require $I$ to be increasing
and $P$ to be decreasing. In other cases, a different analysis will be
necessary to verify safety. Regardless, we believe these ideas may be used to
develop an effective algorithm for the safety problem.

##  4 Preservation results

In this section, we explore when functors preserve $\mu$ and $\nu$. To this
end, we take inspiration from [8], and focus on an adjoint situation equipped
with a ‘step’ $\theta$. This requires the ingredients depicted in equation 8.

$\hfill\leavevmode\hbox to117.97pt{\vbox
to39.69pt{\pgfpicture\makeatletter\hbox{\hskip
58.96922pt\lower-28.30626pt\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\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\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}{-34.76219pt}{-11.3811pt}\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
11.3811pt\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.61111pt}{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{${\mathsf{C}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
11.3811pt\hfil&\hfil\hskip 35.38107pt\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.81944pt}{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{${\mathsf{D}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
11.3811pt\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{-34.96219pt}{-11.98296pt}\pgfsys@curveto{-53.66605pt}{-16.99623pt}{-53.66605pt}{-0.76598pt}{-35.34851pt}{-5.6757pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.96591}{-0.2589}{0.2589}{0.96591}{-35.15536pt}{-5.72748pt}\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}{-56.81645pt}{-11.27272pt}\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}$}
}}\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{-11.79999pt}{-2.19603pt}\pgfsys@curveto{-3.8297pt}{2.40561pt}{3.8297pt}{2.40561pt}{11.45361pt}{-1.99605pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.86603}{-0.5}{0.5}{0.86603}{11.6268pt}{-2.09604pt}\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.38194pt}{3.60796pt}\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{L}$}
}}\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{34.96219pt}{-5.77925pt}\pgfsys@curveto{53.66605pt}{-0.76598pt}{53.66605pt}{-16.99623pt}{35.34851pt}{-12.0865pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.96591}{0.2589}{-0.2589}{-0.96591}{35.15536pt}{-12.03473pt}\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.34285pt}{-11.27272pt}\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{G}$}
}}\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{11.79999pt}{-15.56618pt}\pgfsys@curveto{3.8297pt}{-20.16782pt}{-3.8297pt}{-20.16782pt}{-11.45361pt}{-15.76616pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.86603}{0.5}{-0.5}{-0.86603}{-11.6268pt}{-15.66617pt}\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.68454pt}{-26.15349pt}\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{R}$}
}}\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{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{2.5pt}{-11.93666pt}\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{${\vdash}$}
}}\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\theta:LF\Rightarrow
GL\hfill$ (8)

We note that such a $\theta$ comes equipped with its _mate_
$\theta^{\flat}:FR\to RG$ (and indeed this mate correspondence is a bijection,
as shown in [20]). This situation covers a wide range of examples. Of
particular interest are those cases where $\mathsf{D}$ is an Eilenberg-Moore
category $\mathsf{C}^{T}$ or Kleisli category $\mathsf{Kl}(T)$ for a monad $T$
on $\mathsf{C}$. In these cases, the existence of a lifting $\bar{F}$ of an
endofunctor $F:\mathsf{C}\to\mathsf{C}$ is equivalent to the existence of a
step.

###### Definition 4.1

Consider the data of Scenario 8. $L$ extends to a functor
$\bar{L}:F\text{-}\mathsf{Coalg}\to G\text{-}\mathsf{Coalg}$ given by

$\hfill\leavevmode\hbox to24.52pt{\vbox
to46.31pt{\pgfpicture\makeatletter\hbox{\hskip
12.25867pt\lower-23.15276pt\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\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\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}{-12.25867pt}{-23.15276pt}\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
12.25867pt\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}{-7.95313pt}{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{${FB}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
12.25867pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
8.34894pt\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{0.0pt}{-12.45973pt}\pgfsys@lineto{0.0pt}{4.74036pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{0.0pt}{4.94034pt}\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.35692pt}{-6.09026pt}\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{b}$}
}}\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\mapsto\qquad\leavevmode\hbox
to31.37pt{\vbox to78.46pt{\pgfpicture\makeatletter\hbox{\hskip
15.68297pt\lower-39.22916pt\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\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\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}{-15.68297pt}{-39.22916pt}\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
15.68297pt\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}{-11.37743pt}{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{${GLB}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
15.68297pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
15.66145pt\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}{-11.35591pt}{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{${LFB}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
15.66145pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
11.75172pt\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}{-7.44618pt}{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{${LB}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
11.75172pt\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{0.0pt}{3.61665pt}\pgfsys@lineto{0.0pt}{20.81674pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{0.0pt}{21.01672pt}\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.63887pt}{9.98613pt}\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{\theta}$}
}}\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.0pt}{-28.53613pt}\pgfsys@lineto{0.0pt}{-11.33604pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{0.0pt}{-11.13606pt}\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}{-10.12083pt}{-22.16666pt}\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{Lb}$}
}}\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}}\hfill$

Similarly, $R$ extends to a functor $\bar{R}:G\text{-}\mathsf{Alg}\to
F\text{-}\mathsf{Alg}$ given by

$\hfill\leavevmode\hbox to23.97pt{\vbox
to46.31pt{\pgfpicture\makeatletter\hbox{\hskip
11.98679pt\lower-23.15276pt\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\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\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}{-11.98679pt}{-23.15276pt}\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
11.98679pt\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}{-7.68124pt}{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{${GA}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
11.98679pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
8.05554pt\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.75pt}{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}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.05554pt\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{0.0pt}{5.14032pt}\pgfsys@lineto{0.0pt}{-12.05977pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-12.25975pt}\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.35277pt}{-5.16664pt}\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{a}$}
}}\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\mapsto\qquad\leavevmode\hbox
to31.64pt{\vbox to78.46pt{\pgfpicture\makeatletter\hbox{\hskip
15.82187pt\lower-39.22916pt\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\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\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}{-15.82187pt}{-39.22916pt}\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
15.80035pt\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}{-11.49481pt}{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{${FRA}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
15.80035pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
15.82187pt\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}{-11.51633pt}{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{${RGA}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
15.82187pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
11.89063pt\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}{-7.58508pt}{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{${RA}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
11.89063pt\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{0.0pt}{21.2167pt}\pgfsys@lineto{0.0pt}{4.01662pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{3.81664pt}\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.35277pt}{9.23615pt}\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{\theta^{\flat}}$} }}\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.0pt}{-10.93608pt}\pgfsys@lineto{0.0pt}{-28.13617pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{0.0pt}{-28.33615pt}\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.35277pt}{-22.12776pt}\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{Ra}$}
}}\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}}\hfill$

These functors $\bar{L}$ and $\bar{R}$ satisfy something akin to an adjoint
relationship. Before stating this relationship, we recall the following
(‘useful’) lemma:

###### Lemma 4.2

If $\theta:LF\to GL$ is a step, with mate $\theta^{\flat}$, the following two
squares commute:

${F}$${FRL}$${LFR}$${LRG}$${RLF}$${RGL}$${GLR}$${G}$$\scriptstyle{\eta_{\\_}F}$$\scriptstyle{F\eta}$$\scriptstyle{\theta^{\flat}_{\\_}L}$$\scriptstyle{\theta_{\\_}R}$$\scriptstyle{L\theta^{\flat}}$$\scriptstyle{\epsilon_{\\_}G}$$\scriptstyle{R\theta}$$\scriptstyle{G\epsilon}$

See e.g. [21] for a proof.

###### Lemma 4.3

Let $b:B\to FB$ be an $F$-coalgebra, and $a:GA\to A$ a $G$-algebra. The
natural isomorphism
$\mathrm{Hom}_{\\_}\mathsf{D}(LB,A)\cong\mathrm{Hom}_{\\_}\mathsf{C}(B,RA)$
restricts to a natural isomorphism

$\hfill\mathsf{Hylo}(\bar{L}b,a)\cong\mathsf{Hylo}(b,\bar{R}a)\hfill$

###### Proof 4.4

Fix a coalgebra-to-algebra morphism $\phi:\bar{L}b\to a$. Consider $\phi$’s
transpose $\tilde{\phi}=R\phi\circ\eta$ along the adjunction. We claim that
$\tilde{\phi}$ is a coalgebra-to-algebra morphism $b\to\bar{R}a$. This can be
seen in the following diagram:

${FRLB}$${FRA}$${FB}$${RGLB}$${RGA}$${RLFB}$${B}$${RLB}$${RA}$$\scriptstyle{FR\phi}$$\scriptstyle{\theta^{\flat}}$$\scriptstyle{\theta^{\flat}}$$\scriptstyle{F\eta}$$\scriptstyle{\eta}$$\scriptstyle{RG\phi}$$\scriptstyle{Ra}$$\scriptstyle{R\theta}$$\scriptstyle{b}$$\scriptstyle{\eta}$$\scriptstyle{RLb}$$\scriptstyle{R\phi}$

Here, the bottom right square is the ca-morphism square for $\phi$; the top
right is a naturality square for $\theta^{\flat}$; the top left is given by
lemma 4.2; and the bottom left is naturality for $\eta$. The outside of the
square is a ca-morphism square for $\tilde{\phi}$.

On the other hand, let $\psi:b\to\bar{R}a$ be a ca-morphism. We claim that its
transpose is again a ca-morphism $\bar{L}b\to a$. This is completely dual to
the previous case; but for completeness, it can be seen in the following
diagram:

${GL(B)}$${GLRA}$${LF(B)}$${LFRA}$${GA}$${LRGA}$${L(B)}$${LRA}$${A}$$\scriptstyle{GL\psi}$$\scriptstyle{G\epsilon}$$\scriptstyle{\theta}$$\scriptstyle{LF\psi}$$\scriptstyle{\theta}$$\scriptstyle{L\theta^{\flat}}$$\scriptstyle{a}$$\scriptstyle{LRa}$$\scriptstyle{\epsilon}$$\scriptstyle{b}$$\scriptstyle{L\psi}$$\scriptstyle{\epsilon}$

In [8], it was shown that $\bar{L}$ preserves recursive coalgebras, and
(dually) $\bar{R}$ preserves corecursive algebras. This now follows directly
from the above lemma; however, we can obtain the stronger result that
$\bar{L}$ commutes with the induced comonad $\nu\mu$, and $\bar{R}$ commutes
with the induced monad $\mu\nu$.

###### Theorem 4.5

Consider an adjoint situation as in 8. Let $b:B\to FB$ be an $F$-coalgebra,
and $a:GA\to A$ a $G$-algebra.

  1. (i)

$\nu\mu(\bar{L}b)=\bar{L}(\nu\mu(b))$

  2. (ii)

$\mu\nu(\bar{R}a)=\bar{R}(\mu\nu(a))$

###### Proof 4.6

We only prove (i), since (ii) follows by duality. Let $b$ be a (fixed)
$F$-coalgebra, and $a$ a $G$-algebra. By remark 2.9, we know that
$\nu\mu(b)=\mu(b)^{-1}$, and $\nu\mu(\bar{L}b)=\mu(\bar{L}b)^{-1}$; hence, it
suffices to show

$\mu(\bar{L}b)=(\bar{L}(\mu(b)^{-1}))^{-1}$

Using lemma 4.3, we have the following chain of equivalences, natural in $a$:

$\displaystyle\mathsf{Hylo}(\bar{L}b,a)$
$\displaystyle\cong\mathsf{Hylo}(b,\bar{R}a)$
$\displaystyle\cong\mathrm{Hom}_{\\_}{\mathsf{Alg}F}(\mu(b),\bar{R}a)$
$\displaystyle\cong\mathsf{Hylo}(\mu(b)^{-1},\bar{R}a)$
$\displaystyle\cong\mathsf{Hylo}(\bar{L}(\mu(b)^{-1}),a)$
$\displaystyle\cong\mathrm{Hom}_{\\_}{\mathsf{Alg}G}(\bar{L}(\mu(b)^{-1})^{-1},a)$

This general theorem can be used to prove preservation in various specific
circumstances.

###### Corollary 4.7

Let $T:\mathsf{C}\to\mathsf{C}$ be a monad, let $F:\mathsf{C}\to\mathsf{C}$ be
an endofunctor. Write $j\dashv U$ for the Kleisli adjunction of the monad, and
$T\dashv|-|$ for the Eilenberg-Moore adjunction.

  1. (i)

Assume that $F$ extends to a functor $\bar{F}:Kl(T)\to Kl(T)$ with
$\bar{F}j=jF$. Then $j$ commutes with $\mu$ and $U$ commutes with $\nu$.

  2. (ii)

Assume that $F$ extends to a functor $\bar{F}:EM(T)\to EM(T)$ with
$\bar{F}T=TF$. Then $T$ commutes with $\mu$ and $|-|$ commutes with $\nu$.

###### Proof 4.8

Both of these are instances of adjoint situation 8 with the step given by
identities, and hence the statement follows immediately from 4.5.

###  $\mu$ and $\nu$ Coincide in a Dagger Category

When coalgebras for a polynomial functor $F:\mathsf{Set}\to\mathsf{Set}$ are
interpreted as $F$-shaped automata, the initial $F$-algebra serves as finite
trace semantics and the terminal $F$-coalgebra gives an infinite trace
semantics. When $F$ is no longer a $\mathsf{Set}$-functor this interpretation
breaks down. For example if $F:\mathsf{Rel}\to\mathsf{Rel}$, where
$\mathsf{Rel}$ is the category of sets and relations, then the initial algebra
and terminal coalgebra coincide [22]. In [23], it is shown that this holds
more generally in any dagger category. With this coincidence, the initial
algebra/final coalgebra gives a finite trace semantics instead of an infinite
trace semantics. To obtain a semantics for infinite traces, Urabe and Hasuo
construct an object which is weakly terminal among coalgebras and define the
infinite trace semantics as the maximal map into this object [24]. Note that
the limit colimit coincidence causes no issues when $\mu(c)$ is interpreted as
a semantic object for $c$. However, a generalized limit colimit coincidence
also holds for the fixed points generated by $\mu$ and $\nu$.

###### Definition 4.9

A dagger category $(\mathsf{C},{\dagger})$ is a category equipped with an
identity on objects functor ${\dagger}:\mathsf{C}\to\mathsf{C}^{\mathrm{op}}$
such that ${\dagger}^{2}=id$.

###### Theorem 4.10

Suppose that $(\mathsf{C},{\dagger})$ is a dagger category with limits and
colimits of countable chains and $F:\mathsf{C}\to\mathsf{C}$ is a dagger
functor preserving such limits and colimits. Then there is an isomorphism

$\hfill\mu(c)^{\dagger}\cong\nu(c^{\dagger})\hfill$

for each coalgebra $c$. Dually, for each algebra $a$, there is an isomorphism
$\nu(a)^{\dagger}\cong\mu(a^{\dagger})$.

This theorem may be viewed as a special case of Theorem 4.5 but it is simpler
to use the construction as a (co)limit.

###### Proof 4.11

For a coalgebra $X\xrightarrow{c}FX$ we have

$\displaystyle\nu(c^{{\dagger}})$
$\displaystyle\cong\lim(X\xleftarrow{c^{{\dagger}}}FX\xleftarrow{Fc^{{\dagger}}}F^{2}X\leftarrow\ldots)$
$\displaystyle\cong\mathrm{colim}_{\\_}{C^{\mathrm{op}}}(X\xleftarrow{c^{{\dagger}}}FX\xleftarrow{Fc^{{\dagger}}}F^{2}X\leftarrow\ldots)$
$\displaystyle\cong\mathrm{colim}(X\xrightarrow{c}FX\xrightarrow{Fc}F^{2}X\to\ldots)^{{\dagger}}$
$\displaystyle\cong\mu(c)^{{\dagger}}$

The second isomorphism is because limits in $\mathsf{C}$ are colimits in
$\mathsf{C}^{op}$ and the third isomorphism is because ${\dagger}$ preserves
colimits because it is an equivalence. A similar proof holds for the dual
statement.

##  5 Conclusion

In this paper, we have studied the relative fixed points of functors in a
variety of contexts. In some of these, the fixed points from these functors
have previously been presented as initial algebras or final coalgebras. In
other cases, the fixed points are novel, as is the case with polynomial
functors.

Relative fixpoints provide a fresh perspective on ca-morphisms. Previous work
has mostly focused on cases where there is a unique ca-morphisms, via the
notions of recursive algebras and corecursive coalgebras [7]. However, in
[12], the authors argue that ca-morphisms also hold interest when they are not
unique. Using examples in probability, dynamical systems, and game theory, the
authors show how non-unique ca-morphisms often represent solutions to problems
in these disciplines. This gives us hope that relative fixed points and the
results we have proven about them may be useful in these applications as well.
In particular, in future work we will develop the algorithm suggested in 3.18
and expand its capabilities to solve a wider range of problems.

Another direction of future work is to understand the connection between
relatively terminal coalgebras and coequations. As discussed in section 3,
$\nu(a)$ may be thought of as a ‘cofree solution of the coequation $a$’. As
such, studying $\nu$ may yield new insights into this class of ‘(flatly)
corecursive coequations’, and the kind of properties that may be defined by
such.

## References

  * [1] Adámek J, Trnková V.  Relatively terminal coalgebras.  _Journal of Pure and Applied Algebra_ , 2012.  216(8):1887–1895.  10.1016/j.jpaa.2012.02.026.  Special Issue devoted to the International Conference in Category Theory ‘CT2010’.
  * [2] Jacobs B.  Introduction to coalgebra, volume 59.  Cambridge University Press, 2017.
  * [3] Adámek J, Milius S, Moss LS.  Fixed points of functors.  _Journal of Logical and Algebraic Methods in Programming_ , 2018.  95:41–81.
  * [4] Adámek J, Milius S, Velebil J.  Iterative algebras at work.  _Mathematical Structures in Computer Science_ , 2006.  16(6):1085–1131.
  * [5] Milius S, Pattinson D, Wißmann T.  A new foundation for finitary corecursion: The locally finite fixpoint and its properties.  In: 19th International Conference on Foundations of Software Science and Computation Structures. Springer, 2016 pp. 107–125.
  * [6] Adámek J, Lücke D, Milius S.  Recursive coalgebras of finitary functors.  _Theoretical Informatics and Applications_ , 2007.  41(4):447–462.  10.1051/ita:2007028.
  * [7] Capretta V, Uustalu T, Vene V.  Corecursive algebras: A study of general structured corecursion.  In: Brazilian Symposium on Formal Methods. Springer, 2009 pp. 84–100.
  * [8] Capretta V, Uustalu T, Vene V.  Recursive coalgebras from comonads.  _Information and Computation_ , 2006.  204(4):437–468.  10.1016/j.ic.2005.08.005.
  * [9] Levy PB.  Final Coalgebras from Corecursive Algebras.  In: Moss LS, Sobocinski P (eds.), 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015), volume 35 of _Leibniz International Proceedings in Informatics (LIPIcs)_. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2015 pp. 221–237.  10.4230/LIPIcs.CALCO.2015.221.
  * [10] Adámek J, Milius S, Moss LS.  On Well-Founded and Recursive Coalgebras, 2020.  arxiv:1910.09401.
  * [11] Meijer E, Fokkinga M, Paterson R.  Functional programming with bananas, lenses, envelopes and barbed wire.  In: Conference on functional programming languages and computer architecture. Springer, 1991 pp. 124–144.
  * [12] Trancón y Widemann B, Hauhs M.  Scientific Modelling with Coalgebra-Algebra Homomorphisms.  arxiv:1506.07290.
  * [13] Adámek J, Rosicky J.  Locally presentable and accessible categories, volume 189.  Cambridge University Press, 1994.
  * [14] Riehl E.  Category theory in context.  Courier Dover Publications, 2017.
  * [15] Burris S, Sankappanavar H.  A Course in Universal Algebra, volume 91.  Taylor & Francis, Ltd., 1981.  10.2307/2322184.
  * [16] Dahlqvist F, Schmid T.  How to Write a Coequation ((Co)algebraic pearls).  In: 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2018), volume 211 of _LIPIcs_. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021 pp. 13:1–13:25.  10.4230/LIPIcs.CALCO.2021.13.
  * [17] Johnstone P, Power J, Tsujishita T, Watanabe H, Worrell J.  On the structure of categories of coalgebras.  _Theoretical Computer Science_ , 2001.  260(1):87–117.  10.1016/S0304-3975(00)00124-9.
  * [18] Noquez V, Moss LS.  The Sierpinski Carpet as a Final Coalgebra.  In: Fourth Conference of Applied Category Theory (ACT2021), volume 372 of _EPTCS_. 2022 pp. 249–262.  10.4204/EPTCS.372.
  * [19] Kori M, Ascari F, Bonchi F, Bruni R, Gori R, Hasuo I.  Exploiting Adjoints in Property Directed Reachability Analysis.  In: 35th Conference on Computer Aided Verification (CAV2023). Springer, 2023 pp. 41–63.  10.1007/978-3-031-37703-73.
  * [20] Kelly GM, Street R.  Review of the elements of 2-categories.  In: Category Seminar: Proceedings Sydney Category Theory Seminar 1972/1973. Springer, 2006 pp. 75–103.  10.1007/BFb0063101.
  * [21] Rot J, Jacobs B, Levy PB.  Steps and Traces.  _Journal of Logic and Computation_ , 2021.  31(6):1482–1525.  10.1093/logcom/exab050.
  * [22] Smyth MB, Plotkin GD.  The category-theoretic solution of recursive domain equations.  _SIAM Journal on Computing_ , 1982.  11(4):761–783.
  * [23] Karvonen MJ.  Way of the dagger.  Ph.D. thesis, University of Edinburgh, 2019.
  * [24] Hasuo I, Urabe N.  Coalgebraic Infinite Traces and Kleisli Simulations.  _Logical Methods in Computer Science_ , 2018.  14.