Czech Technical University in Prague, Czech Republic and Technische
Universität Braunschweig<EMAIL_ADDRESS>by the grant No.
22-02964S of the Czech Grant Agency Friedrich-Alexander-Universität Erlangen-
Nürnberg,
Germanystefan.milius@fau.dehttps://orcid.org/0000-0002-2021-1644Supported by
Deutsche Forschungsgemeinschaft (DFG) under project MI 717/9-1 and as part of
the Research and Training Group 2475 “Cybercrime and Forensic Computing”
(393541319/GRK2475/1-2019)Indiana University, Bloomington IN,
<EMAIL_ADDRESS>by grant #586136 from the Simons
Foundation.Jiří Adámek, Stefan Milius, Lawrence S. Moss [500]Theory of
computation Models of computation [500]Theory of computation Logic and
verification

# On Kripke, Vietoris and Hausdorff Polynomial Functors

Jiří Adámek  Stefan Milius  Lawrence S. Moss

###### Abstract

The Vietoris space of compact subsets of a given Hausdorff space yields an
endofunctor $\mathscr{V}$ on the category of Hausdorff spaces. Vietoris
polynomial endofunctors on that category are built from $\mathscr{V}$, the
identity and constant functors by forming products, coproducts and
compositions. These functors are known to have terminal coalgebras and we
deduce that they also have initial algebras. We present an analogous class of
endofunctors on the category of extended metric spaces, using in lieu of
$\mathscr{V}$ the Hausdorff functor $\mathcal{H}$. We prove that the ensuing
Hausdorff polynomial functors have terminal coalgebras and initial algebras.
Whereas the canonical constructions of terminal coalgebras for Vietoris
polynomial functors takes $\omega$ steps, one needs $\omega+\omega$ steps in
general for Hausdorff ones. We also give a new proof that the closed set
functor on metric spaces has no fixed points.

###### category:

(Co)algebraic pearls

###### keywords:

Hausdorff functor, Vietoris functor, initial algebra, terminal coalgebra

##  1 Introduction

This paper presents results on terminal coalgebras and initial algebras for
certain endofunctors on the categories $\mathsf{Haus}$ of Hausdorff
topological spaces and $\mathsf{Met}$ of extended metric spaces. These results
are based on the terminal coalgebra construction first presented by Adámek [2]
(in dual form) and independently by Barr [9]. Given an endofunctor $F$,
iterate $F$ on the unique morphism $!\colon F1\to 1$ to obtain the following
$\omega^{\mathsf{op}}$-chain

$1\xleftarrow{\leavevmode\nobreak\ !\leavevmode\nobreak\
}F1\xleftarrow{\leavevmode\nobreak\ F!\leavevmode\nobreak\
}FF1\xleftarrow{\leavevmode\nobreak\ FF!\leavevmode\nobreak\
}FFF1\xleftarrow{\leavevmode\nobreak\ FFF!\leavevmode\nobreak\ }\cdots$ (1)

Assume that the limit exists, and denote it by $V_{\omega}$ and the limit cone
by $\ell_{n}\colon V_{\omega}\to F^{n}1$ ($n<\omega$). We obtain a unique
morphism $m\colon FV_{\omega}\to V_{\omega}$ such that for all
$n\in\omega^{\mathsf{op}}$ we have

$F\ell_{n}=\big{(}FV_{\omega}\xrightarrow{\leavevmode\nobreak\
m\leavevmode\nobreak\ }V_{\omega}\xrightarrow{\leavevmode\nobreak\
\ell_{n+1}\leavevmode\nobreak\ }F^{n+1}1\big{)}.$ (2)

If $F$ preserves the limit $V_{\omega}$, then $m$ is an isomorphism. Its
inverse yields the terminal coalgebra $m^{-1}\colon V_{\omega}\to
FV_{\omega}$; shortly $\nu F=V_{\omega}$, and we say that the terminal
coalgebra is _obtained in $\omega$ steps_.

This technique of _finitary iteration_ is the most basic and prominent
construction of terminal coalgebras. However finite iteration requires that
the limit in (1) exists and also that it is preserved by the functor. It does
_not_ apply on $\mathsf{Set}$ to the finite power set functor
$\mathscr{P}_{\mathsf{f}}$. For that functor $FV_{\omega}\not\cong
V_{\omega}$. However, a modification of finite iteration does apply, as shown
by Worrell [26]. One makes a _second infinite iteration_ , iterating $F$ on
the morphism $m\colon FV_{\omega}\to V_{\omega}$ rather than on $!\colon F1\to
1$, obtaining a chain

$V_{\omega}\xleftarrow{\leavevmode\nobreak\ m\leavevmode\nobreak\
}V_{\omega+1}\xleftarrow{\leavevmode\nobreak\ Fm\leavevmode\nobreak\
}V_{\omega+2}\xleftarrow{\leavevmode\nobreak\ FFm\leavevmode\nobreak\ }\cdots$
(3)

Its limit is denoted by $V_{\omega+\omega}=\lim_{n<\omega}V_{\omega+n}$ with
the limit cone $\bar{l}_{n}\colon V_{\omega+\omega}\to V_{\omega+n}$, for
$n<\omega$. Worrell’s insight was that this second limit, $V_{\omega+\omega}$,
is preserved by every finitary functor. We prove that this also works for
functors built from $\mathscr{P}_{\mathsf{f}}$ using product, coproduct, and
composition (which may be non-finitary). These are the _Kripke polynomial
functors_ mentioned in our title.

We are interested in other settings where terminal coalgebras may be built
using either the limit in (1) or the limit in (3). We study fixed points of
naturally occurring endofunctors on Hausdorff spaces and metric spaces,
endofunctors built from the Vietoris and Hausdorff functors and several other
natural constructions.

In the category $\mathsf{Top}$ a good analogy of $\mathscr{P}_{\mathsf{f}}$ is
the _Vietoris functor_ $\mathscr{V}$ assigning to every space $X$ the space of
all compact subsets equipped with the Vietoris topology (section 4). Hofmann
et al. [12] define _Vietoris polynomial_ functors as those endofunctors on
$\mathsf{Top}$ built from $\mathscr{V}$, the constant functors, and the
identity functor, using product, coproduct, and composition. We study this on
the subcategory $\mathsf{Haus}$ of Hausdorff spaces and use that
$\mathscr{V}\colon\mathsf{Haus}\to\mathsf{Haus}$ preserves limits of
$\omega^{\mathsf{op}}$-chains, a fact for which we present a new proof. This
implies that for _Vietoris polynomial functors_ (defined as above but with
$\mathscr{V}$ in lieu of $\mathscr{P}_{\mathsf{f}})$, the terminal coalgebra
exists and is the limit of (1). The existence of initial algebras follows.

We also present a result for the category $\mathsf{Met}$ of metric spaces and
nonexpanding maps. The role of the Vietoris functor is played by the
_Hausdorff functor_ $\mathcal{H}$ assigning to every space $X$ the space
$\mathcal{H}X$ of all compact subsets with the Hausdorff metric.

#### Other contributions.

In addition to the aforementioned results we show results obtained by either
varying the category or the endofunctor. For example, consider again the
Hausdorff polynomial functors. Whenever $F$ is such a functor and the
constants involved in its construction are complete spaces, $\nu F$ again
turns out to be complete. Analogous results hold for compact spaces, or
ultrametric spaces. Finally, we present a proof of the description of
$\nu\mathscr{P}_{\mathsf{f}}$ and $V_{\omega}$ for $\mathscr{P}_{\mathsf{f}}$
exhibited by Worrell [26] (the latter without a proof).

We simplify a proof of a known negative result: the variation of $\mathcal{H}$
obtained by moving from compact sets to closed sets has no fixed points.

#### Related work.

Our work is more general and hence improves results of Abramsky [1], Hofmann
et al. [12], and Worrell [26].

There are numerous results about the existence and construction of terminal
coalgebras in the literature. At several places we discuss other possible
approaches to our results.

##  2 Preliminaries

We review a few preliminary points. We assume that readers are familiar with
basic notions of category theory as well as algebras and coalgebras for an
endofunctor. We denote by $\mathsf{Set}$ the category of sets and functions,
$\mathsf{Top}$ is the category of topological spaces and continuous functions,
and $\mathsf{Met}$ is the category of _(extended) metric spaces_ (so we might
have $d(x,y)=\infty$) and non-expanding maps: the functions $f\colon X\to Y$
where $d(f(x),f(x^{\prime}))\leq d(x,x^{\prime})$ holds for every pair
$x,x^{\prime}\in X$. Note that this class of morphisms is smaller than the
class of continuous functions between metric spaces.

######  Remark .

Consider an $\omega^{\mathsf{op}}$-chain

$X_{0}\xleftarrow{\leavevmode\nobreak\ f_{0}\leavevmode\nobreak\
}X_{1}\xleftarrow{\leavevmode\nobreak\ f_{1}\leavevmode\nobreak\
}X_{2}\xleftarrow{\leavevmode\nobreak\ f_{2}\leavevmode\nobreak\ }\cdots$ (4)

  1. 1.

In $\mathsf{Set}$, the limit $L$ consists of all sequences
$(x_{n})_{n<\omega}$, $x_{n}\in X_{n}$ that are _compatible_ :
$f_{n}(x_{n+1})=x_{n}$ for every $n$. The limit projections are the functions
$\ell_{n}\colon L\to X_{n}$ defined by $\ell_{n}((x_{i}))=x_{n}$.

  2. 2.

In $\mathsf{Top}$, the limit is again carried by the same set $L$ as in
$\mathsf{Set}$, and the limit projections $\ell_{n}$ are also the same. The
topology on $L$ has as a base the sets $\ell_{n}^{-1}(U)$, for $U$ open in
$X_{n}$.

  3. 3.

In $\mathsf{Met}$, the limit is again carried by the same set $L$, and the
same limit projections $\ell_{n}$. The metric on $L$ is defined by
$d((x_{n}),(y_{n}))=\sup_{n<\omega}d(x_{n},y_{n})$.

#### Smooth Monomorphisms.

In addition to terminal coalgebras, we also study initial algebras for the
functors of interest in this paper. For this, we call on a general result
which allows one to infer the existence of the initial algebra for an
endofunctor $F$ from the existence of a terminal coalgebra for $F$ (or in fact
of any algebra with monic structure).

For a class $\mathcal{M}$ of monomorphisms we denote by
$\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$ the collection of subobjects of
$A$ represented by monomorphisms from $\mathcal{M}$. To say that this is a
dcpo means that it is a set which (when ordered by factorization in the usual
way) is a poset having directed joins.

######  Definition  ([4, Def. 3.1]).

Let $\mathcal{M}$ be a class of monomorphisms closed under isomorphisms and
composition.

  1. 1.

We say that an object $A$ has _smooth $\mathcal{M}$-subobjects_ provided that
$\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$ is a dcpo with bottom $\bot$,
where the least element and directed joins are given by colimits of the
corresponding diagrams of subobjects.

  2. 2.

The class $\mathcal{M}$ is _smooth_ if every object of $\mathscr{A}$ has
smooth $\mathcal{M}$-subobjects.

A category has _smooth monomorphisms_ if the class of all monomorphisms is
smooth.

######  Example 2.1.

  1. 1.

The categories $\mathsf{Set}$ and $\mathsf{Top}$ have smooth monomorphisms,
and so does the full subcategory of Hausdorff spaces. This is easy to see.

  2. 2.

The category $\mathsf{Met}$ also has smooth monomorphisms (these are the
injective non-expanding maps) [4, Lemma A.1].

The full subcategory $\mathsf{CMS}$ of complete metric spaces does not have
smooth monomorphisms. However, strong monomorphisms (isometric embeddings) are
smooth in both $\mathsf{Met}$ and $\mathsf{CMS}$ [4, Lemma A.2].

  3. 3.

Strong monomorphisms (subspace embeddings) in $\mathsf{Top}$ are not smooth
[3, Ex. 3.5].

######  Theorem 2.2 ([4, Cor. 4.4]).

Let $\mathcal{M}$ be a smooth class of monomorphisms. If an endofunctor $F$
preserving $\mathcal{M}$ has a terminal coalgebra, then it has an initial
algebra.

Note that loc. cit. states more: given any algebra $m\colon FA\rightarrowtail
A$ where $m$ lies in $\mathcal{M}$, the initial algebra exists and is a
subalgebra of $(A,m)$.

##  3 Kripke Polynomial Functors

We turn to the first collection of functors mentioned in the title of this
paper: the Kripke polynomial functors on $\mathsf{Set}$. The name stems from
_Kripke structures_ used in modal logic. Our definition below is a slight
generalization of the (finite) Kripke polynomial functors presented by Jacobs
[13, Def. 2.2.1]. (Kripke polynomial functors using the full power-set functor
were originally introduced by Rößiger [21].) We admit arbitrary products in
lieu of just arbitrary exponents.

######  Definition 1.

The _Kripke polynomial functors_ $F$ are the set functors built from the
finite power-set functor, constant functors and the identity functor, by using
product, coproduct and composition. In other words, Kripke polynomial functors
are built according to the following grammar:

$\textstyle F::=\mathscr{P}_{\mathsf{f}}\mid A\mid\mathsf{Id}\mid\prod_{i\in
I}F_{i}\mid\coprod_{i\in I}F_{i}\mid FF,$

where $A$ ranges over all sets (and is interpreted as a constant functor) and
$I$ is an arbitrary index set.

######  Remark 2.

The constant functors could be omitted from the grammar since they are
obtainable from the rest of the grammar. The constant functor with value $1$
is the empty product. For each set $A$, the constant functor with value $A$ is
then a coproduct: $A=\coprod_{a\in A}1$.

######  Example 3.1.

The Kripke polynomial functor $FX=\mathscr{P}_{\mathsf{f}}(A\times X)$ is the
type functor of finitely branching labelled transition systems with a set $A$
of actions.

######  Remark 3.

An endofunctor is _finitary_ if it preserves directed colimits. Worrell [26]
proved that for every finitary set functor the terminal coalgebra is obtained
in $\omega+\omega$ steps. We prove a version of Worrell’s result but for
Kripke polynomial functors.

There are Kripke polynomial set functors which are not finitary. One example
of such a functor is $F(X)=X^{\mathds{N}}$, where $\mathds{N}$ is the set of
natural numbers. There are also finitary set functors which are not Kripke
polynomial functors. One example (see Appendix C) is the functor assigning to
a set $X$ the set of _nonempty_ finite subsets of $X$.

Our proof below uses ideas from Worrell’s work [26].

######  Theorem 3.2.

Every Kripke polynomial functor $F$ has a terminal coalgebra obtained in
$\omega+\omega$ steps: $\nu F=V_{\omega+\omega}$.

######  Proof 3.3.

  1. 1.

We first observe that $F$ preserves monomorphisms and intersections of
monomorphisms. This is clear for constant functors and for $\mathsf{Id}$, and
it is easy to see for $\mathscr{P}_{\mathsf{f}}$. Moreover, these properties
are clearly preserved by product, coproduct and composition.

  2. 2.

Let $(X_{n})_{n<\omega}$ be an $\omega^{\mathsf{op}}$-chain in $\mathsf{Set}$.
Then the canonical morphism $m\colon F(\lim X_{n})\to\lim FX_{n}$ is monic.
This is obvious for constant functors and $\mathsf{Id}$. Let us check it for
$\mathscr{P}_{\mathsf{f}}$. Denote the limit projections by
$\ell_{n}\colon\lim X_{n}\to X_{n}$ and
$p_{n}\colon\lim\mathscr{P}_{\mathsf{f}}X_{n}\to\mathscr{P}_{\mathsf{f}}X_{n}$
($n<\omega$); the canonical morphism $m$ is unique such that $p_{n}\cdot
m=\mathscr{P}_{\mathsf{f}}\ell_{n}$. Now given $S\neq T$ in
$\mathscr{P}_{\mathsf{f}}(\lim X_{n})$, without loss of generality we can pick
$x\in T\setminus S$. Using that the $\ell_{n}$ are jointly monic, for every
$s\in S$ we can choose $n<\omega$ such that $\ell_{n}(x)\neq\ell_{n}(s)$.
Since $S$ is finite, this choice can be performed independently of $s\in S$.
Thus $\ell_{n}(x)\not\in\ell_{n}[S]$, and hence
$\mathscr{P}_{\mathsf{f}}\ell_{n}(T)\neq\mathscr{P}_{\mathsf{f}}(S)$. Thus,
$\mathscr{P}_{\mathsf{f}}\ell_{n}$ is a jointly monic family. Since
$p_{n}\cdot m=\mathscr{P}_{\mathsf{f}}\ell_{n}$, we see that $m$ is monic.

  3. 3.

An induction on Kripke polynomial functors $F$ now shows that $m\colon
V_{\omega+1}\to V_{\omega}$ is monic. We have seen this for the base case
functors in Item 2. The desired property that $m$ is monic is preserved by
products, coproducts and composition. In particular, for a composition $FG$
note that the canonical morphism for $FG$ is the composition

$FG(\lim X_{n})\xrightarrow{\leavevmode\nobreak\ Fm\leavevmode\nobreak\
}F(\lim GX_{n})\xrightarrow{\leavevmode\nobreak\
m^{\prime}\leavevmode\nobreak\ }\lim FGX_{n},$

where $m$ is the canonical morphism for $G$ w.r.t. the given
$\omega^{\mathsf{op}}$-chain and $m^{\prime}$ the one for $F$ and the
$\omega^{\mathsf{op}}$-chain $(GX_{n})_{n<\omega}$. So this morphism
$m^{\prime}\cdot Fm$ is monic since both $m$ and $m^{\prime}$ are so and $F$
preserves monomorphisms by Item 1.

  4. 4.

Since $F$ preserves monomorphisms, we see that $Fm$, $FFm$ etc. are monic. We
obtain a decreasing chain of subobjects $V_{\omega+n}\rightarrowtail
V_{\omega}$. Therefore, the limit
$V_{\omega+\omega}=\lim_{n<\omega}V_{\omega+n}$ is simply the intersection of
these subobjects. From Item 1 we know that $F$ preserves this limit. It
follows that $\nu F=V_{\omega+\omega}$, as desired.

######  Corollary 3.4.

Every Kripke polynomial functor $F$ on $\mathsf{Set}$ has an initial algebra.

This follows from Theorem 3.2, 2.1.1, and Theorem 2.2 since $F$ preserves
monomorphisms.

######  Example 3.5 ([26]).

The functor $\mathscr{P}_{\mathsf{f}}$ has a terminal coalgebra consisting of
all finitely branching strongly extensional trees (up to isomorphism of
trees). Moreover, the limit $V_{\omega}$ consists of all compactly branching
strongly extensional trees. We present a proof of these results in Appendix A
(Theorem A.14).

##  4 Vietoris Polynomial Functors

Hofmann et al. [12] proved that Vietoris polynomial functors on the category
$\mathsf{Haus}$ of Hausdorff spaces have terminal coalgebras obtained in
$\omega$ steps. Our proof is slightly different from theirs because we wish to
avoid a result stated by Zenor [27] whose proof is incomplete.

Recall that a _base_ of a topology is a collection $\mathcal{B}$ of open sets
such that every open set is a union of members of $\mathcal{B}$. A _subbase_
is a collection of open sets whose finite intersections form a base. For every
collection $\mathcal{B}$ of subsets of the space, there is a smallest topology
for which $\mathcal{B}$ is a (sub)base, the family of unions of finite
intersections from $\mathcal{B}$.

######  Definition 4.

  1. 1.

Let $X$ be a topological space. We denote by $\mathscr{V}X$ the space of
compact subsets of $X$ equipped with the “hit-and-miss” topology. This
topology has as a subbase all sets of the following forms:

$\displaystyle U^{\Diamond}$ $\displaystyle=\\{R\in VX:R\cap
U\neq\emptyset\\}$ $\displaystyle\text{($R$ hits $U$)},$ (5) $\displaystyle
U^{\Box}$ $\displaystyle=\\{R\in VX:R\subseteq U\\}$ ($R$ misses $X\setminus
U$),

where $U$ ranges over the open sets of $X$. We call $\mathscr{V}X$ the
_Vietoris space of $X$_, also known as the _hyperspace_ of $X$.

  2. 2.

Recalling that the image of a compact set under a continuous function is also
compact, for a continuous function $f\colon X\to Y$ we put
$\mathscr{V}f(A)=f[A]$ for every compact subset $A$ of $X$.

######  Remark 5.

  1. 1.

For a compact Hausdorff space $X$, Vietoris [25] defined $\mathscr{V}X$ to
consist of all _closed_ subsets of $X$. These are the same as the compact
subsets in this case. In the coalgebraic literature, $\mathscr{V}X$ has also
mostly been studied for spaces $X$ which are compact Hausdorff. However, the
“classic Vietoris space” (using closed subsets) does not yield a functor on
$\mathsf{Top}$ (see Hofmann et al. [12, Rem. 2.28]). Hofmann et al. [12, Def.
2.27] call the functor $\mathscr{V}$ in 4 the _compact Vietoris functor_.

  2. 2.

Michael [18, Thm. 4.9.8] proved that $X$ is Hausdorff iff so is
$\mathscr{V}X$.

  3. 3.

Vietoris [25] originally proved that for a compact Hausdorff space $X$ (the
classic Vietoris space) $\mathscr{V}X$ is compact Hausdorff, too.

  4. 4.

A _Stone space_ is a compact Hausdorff space having a base of clopen sets. If
$X$ is a Stone space, so is $\mathscr{V}X$; see [18, Thm. 4.9.9] or [14,
Section III.4].

######  Proposition 4.1.

For every continuous function $f\colon X\to Y$ and every open $U\subseteq Y$,
$(f^{-1}(U))^{\Diamond}=(\mathscr{V}f)^{-1}(U^{\Diamond})$, and
$(f^{-1}(U))^{\Box}=(\mathscr{V}f)^{-1}(U^{\Box})$.

######  Proof 4.2.

Let $R\in\mathscr{V}X$. Observe that

$R\cap f^{-1}(U)\neq\emptyset\iff f[R]\cap U\neq\emptyset\iff f[R]\in
U^{\Diamond}\iff R\in(\mathscr{V}f)^{-1}(U^{\Diamond}).$

This proves our first assertion for all $R$. For the second assertion, we have

$R\subseteq f^{-1}(U)\iff f[R]\subseteq U\iff f[R]\in U^{\Box}\iff
R\in(\mathscr{V}f)^{-1}(U^{\Box}).$

######  Corollary 4.3.

The mappings $X\mapsto\mathscr{V}X$ and $f\mapsto\mathscr{V}f$ form a functor
$\mathscr{V}$ on $\mathsf{Top}$.

Indeed, 4.1 shows that for every subbasic open set of $\mathscr{V}Y$ its
inverse image under $\mathscr{V}f$ is open in $\mathscr{V}X$. This establishes
continuity of $\mathscr{V}f$.

######  Notation 4.4.

We denote by $\mathsf{Haus}$, $\mathsf{KHaus}$ and $\mathsf{Stone}$ the full
subcategories of $\mathsf{Top}$ given by all Hausdorff spaces, all compact
Hausdorff spaces and all Stone spaces, respectively. By 5.2–4, $\mathscr{V}$
restricts to these three full subcategories, and we denote the restrictions by
$\mathscr{V}$ as well.

######  Remark 6.

  1. 1.

The full subcategories $\mathsf{Haus}$, $\mathsf{KHaus}$ and $\mathsf{Stone}$
are closed under limits in $\mathsf{Top}$. In particular, the inclusion
functors preserve and reflect limits. In fact, $\mathsf{KHaus}$ is a full
reflective subcategory: the reflection of a space is its Stone-Čech
compactification.

  2. 2.

If an $\omega^{\mathsf{op}}$-chain as in (4) consists of surjective continuous
maps between compact Hausdorff spaces, then each limit projection
$\ell_{n}\colon\lim_{k<\omega}X_{k}\to X_{n}$ is surjective, too. Moreover,
Eilenberg and Steenrod [10, Cor. 3.9] prove the surjectivity of projections
for all codirected limits of surjections between compact Hausdorff spaces; see
also Ribes and Zalesskii [20, Prop. 1.1.10]).

  3. 3.

If $X$ has a base $\mathcal{B}$ which is closed under finite unions, then the
sets $U^{\Diamond}$ and $U^{\Box}$ for $U\in\mathcal{B}$ already form a
subbase of $\mathscr{V}X$. Indeed, given a set $\mathcal{S}$ of open subsets
of $X$ we have
$(\bigcup\mathcal{S})^{\Diamond}=\bigcup\\{U^{\Diamond}:U\in\mathcal{S}\\}$.
Moreover, it is easy to see that

$\textstyle(\bigcup\mathcal{S})^{\Box}=\bigcup\\{\big{(}\bigcup\mathcal{F}\big{)}^{\Box}:\text{$\mathcal{F}\subseteq\mathcal{S}$
finite}\\};$

“$\supseteq$” is trivial, and for “$\subseteq$” use compactness of
$R\in\mathscr{V}X$. Hence, if $\mathcal{S}$ consists of basic open sets from
$\mathcal{B}$, then $\bigcup F\in\mathcal{B}$ due to its closure under finite
unions. Thus, $(\bigcup\mathcal{S})^{\Box}$ is a union of sets of the form
$U^{\Box}$ for $U\in\mathcal{B}$.

######  Proposition 4.5.

The functor $\mathscr{V}\colon\mathsf{Haus}\to\mathsf{Haus}$ preserves limits
of $\omega^{\mathsf{op}}$-chains.

######  Proof 4.6.

Consider an $\omega^{\mathsf{op}}$-chain as in (4). Let
$M=\lim\mathscr{V}X_{n}$, with limit cone $r_{n}\colon M\to\mathscr{V}X_{n}$.
Let $m\colon\mathscr{V}L\to M$ be the unique continuous map such that
$\mathscr{V}\ell_{n}=r_{n}\cdot m$ for all $n<\omega$. We shall prove that $m$
is a bijection and then that its inverse is continuous, which proves that $m$
is an isomorphism.

  1. 1.

Injectivity of $m$ follows from the fact that $\mathscr{V}\ell_{n}$
($n<\omega$) forms a jointly monic family, as we will now prove. Suppose that
$A,B\in\mathscr{V}L$ satisfy $\ell_{n}[A]=\ell_{n}[B]$ for every $n<\omega$.
We prove that $A\subseteq B$; by symmetry $A=B$ follows. Given $a\in A$, we
show that every open neighbourhood of $a$ has a nonempty intersection with
$B$. Since $B$ is closed, we then have $a\in B$ (otherwise $L\setminus B$
would be an open neighbourhood of $a$ disjoint from $B$). It suffices to prove
the desired property for the basic open neighbourhoods $\ell_{n}^{-1}(U)$ of
$a$, for $U$ open in $X_{n}$ (see section 2.2). Since
$\ell_{n}[A]=\ell_{n}[B]$ we have some $b\in B$ which satisfies
$\ell_{n}(a)=\ell_{n}(b)$. Then $b\in\ell_{n}^{-1}(U)\cap B$.

  2. 2.

Surjectivity of $m$. An element of $M$ is a sequence $(K_{n})_{n<\omega}$ of
compact (hence closed) subsets $K_{n}\subseteq X_{n}$ such that
$f_{n}[K_{n+1}]=K_{n}$ for every $n<\omega$. We need to find a compact set
$K\subseteq L$ such that $\ell_{n}[K]=K_{n}$ for every $n<\omega$. With the
subspace topology, $K_{n}$ is itself a compact space. The connecting maps
$f_{n}\colon X_{n+1}\to X_{n}$ restrict to surjective continuous maps
$K_{n+1}\twoheadrightarrow K_{n}$. Thus, the $K_{n}$ form an
$\omega^{\mathsf{op}}$-chain of surjections in $\mathsf{KHaus}$. Let $K$ be
the limit with projections $p_{n}\colon K\twoheadrightarrow K_{n}$. Then $K$
is a subset of $L$, and each projection $p_{n}$ is the restriction of
$\ell_{n}$ to $X_{n}$.

Let us check that the topology on $K$ is the subspace topology inherited from
$L$. A base of the topology on $K$ is the family of sets $p_{n}^{-1}(U)$ as
$U$ ranges over the open subset of $K_{n}$. Each $U$ is of the form $V\cap
K_{n}$ for some open $V$ of $X_{n}$, and $p_{n}^{-1}(U)=\ell_{n}^{-1}(V)\cap
K$. Thus $p_{n}^{-1}(U)$ is open in the subspace topology, and the converse
holds as well.

The maps $p_{n}$ are surjective by 6.2. Moreover, $K$ is a compact space by
6.1. Thus, $K$ is the desired compact set in $\mathscr{V}L$ such that
$p_{n}[K]=K_{n}$ for all $n$.

  3. 3.

Finally, we prove that the inverse $k\colon M\to\mathscr{V}L$, say, of $m$ is
continuous. We know that the sets $\ell_{n}^{-1}(U)$, for $U$ open in $X_{n}$,
form a base of $L$. Moreover, this base is closed under finite unions. By 6.3
and using 4.1 we obtain that $\mathscr{V}L$ has a subbase given by the
following sets

$(\mathscr{V}\ell_{n})^{-1}(U^{\Diamond})=(\ell_{n}^{-1}(U))^{\Diamond}\quad\text{and}\quad(\mathscr{V}\ell_{n})^{-1}(U^{\Box})=(\ell_{n}^{-1}(U))^{\Box}\quad\text{for
$U$ open in $X_{n}$.}$

It suffices to show that the inverse images of these subbasic open sets of
$\mathscr{V}L$ are open in $M$. For $\mathscr{V}\ell_{n}^{-1}(U^{\Diamond})$
with $U$ open in $X_{n}$ we use that $\mathscr{V}\ell_{n}\cdot k=r_{n}$
clearly holds to obtain

$k^{-1}\big{(}\mathscr{V}\ell_{n}^{-1}(U^{\Diamond})=r_{n}^{-1}(U^{\Diamond}),$

which is a basic open set of $M$ by section 2.2. For the subbasic open sets
$\mathscr{V}\ell_{n}^{-1}(U^{\Box})$ the proof is similar.

######  Corollary 4.7.

The restrictions of $\mathscr{V}$ to $\mathsf{KHaus}$ and $\mathsf{Stone}$
preserve limits of $\omega^{\mathsf{op}}$-chains.

Indeed, use 6.1.

######  Remark 7.

A _codirected limit_ is the limit of a diagram whose scheme is of the form
$P^{\mathsf{op}}$ for a directed poset $P$. 4.5 and 4.7 hold more generally
for codirected limits. The argument is the same. This proves a result stated
in Zenor [27], but with an incomplete proof.

The following definition is due to Kupke et al. [16] for Stone spaces, whereas
Hofmann et al. [12, Def. 2.29] use arbitrary topological spaces, but they
later essentially restrict constants to be (compact) Hausdorff, stably compact
or spectral spaces.

######  Definition 8.

The _Vietoris polynomial functors_ are the endofunctors on $\mathsf{Top}$
built from the Vietoris functor $\mathscr{V}$, the constant functors, and the
identity functor, using product, coproduct, and composition. Thus, the
Vietoris polynomial functors are built according to the following grammar

$\textstyle F::=\mathscr{V}\mid A\mid\mathsf{Id}\mid\prod_{i\in
I}F_{i}\mid\coprod_{i\in I}F_{i}\mid FF,$

where $A$ ranges over all topological spaces and $I$ is an arbitrary index
set.

######  Theorem 4.8.

Let $F\colon\mathsf{Top}\to\mathsf{Top}$ be a Vietoris polynomial functor, and
assume that all constants in $F$ are Hausdorff spaces. Then $F$ has a terminal
coalgebra obtained in $\omega$ steps, and $\nu F=V_{\omega}$ is a Hausdorff
space.

######  Proof 4.9.

An easy induction on Vietoris polynomial functors $F$ shows that:

  1. 1.

The functor $F$ has a restriction $F_{0}\colon\mathsf{Haus}\to\mathsf{Haus}$,

  2. 2.

The restriction $F_{0}$ preserves surjective maps; the most important step
being for $\mathscr{V}$ itself, and this uses the fact when $f\colon X\to Y$
is continuous and $X$ and $Y$ are Hausdorff, the inverse images of compact
sets are compact.

  3. 3.

The functor $F_{0}$ preserves limits of $\omega^{\mathsf{op}}$-chains; the
most important step is done in 4.5.

The terminal coalgebra result for $F_{0}$ follows from the fact which we have
mentioned in section 2: $\nu F$ is the limit of the terminal-coalgebra
$\omega^{\mathsf{op}}$-chain $F_{0}^{n}1$ ($n<\omega$). Since $\mathsf{Haus}$
is closed under limits in $\mathsf{Top}$ and $F_{0}^{n}1=F^{n}1$, the functor
$F$ has the same terminal coalgebra $\nu F=\lim F^{n}1$.

######  Corollary 4.10.

Let $F\colon\mathsf{Top}\to\mathsf{Top}$ be a Vietoris polynomial functor, and
assume that all constants in $F$ are Hausdorff spaces. Then $F$ has an initial
algebra.

This follows from Theorem 4.8, 2.1.1 and Theorem 2.2, since an easy induction
shows that $F$ preserves monomorphisms.

######  Corollary 4.11.

Let $F\colon\mathsf{Top}\to\mathsf{Top}$ be a Vietoris polynomial functor in
which all constants are _compact_ Hausdorff spaces and only finite coproducts
are used. Then the terminal coalgebra $\nu F$ is a compact Hausdorff space.

######  Proof 4.12.

The functor $F$ restricts to an endofunctor on $\mathsf{KHaus}$. Thus, the
terminal-coalgebra $\omega^{\mathsf{op}}$-chain $F^{n}1$ lies in
$\mathsf{KHaus}$. Moreover, $\mathsf{KHaus}$ is closed under limits in
$\mathsf{Top}$ because it is a full reflective subcategory (6.1). Thus, $\nu
F=\lim_{n<\omega}F^{n}1$ is compact Hausdorff.

######  Corollary 4.13.

Let $F\colon\mathsf{Top}\to\mathsf{Top}$ be a Vietoris polynomial functor in
which all constants are Stone spaces and only finite coproducts are used. Then
the terminal coalgebra $\nu F$ is a Stone space.

The proof is similar.

######  Remark 9.

4.11 essentially appears in work by Hofmann et al. [12, Thm. 3.42] (except for
the convergence ordinal). 4.13 is due to Kupke et al. [16]. Our proof using
convergence of the terminal-coalgebra chain is different than the previous
ones.

######  Example 4.14.

The terminal coalgebra for $\mathscr{V}$ itself was identified by Abramsky
[1]. By what we have shown, it is $V_{\omega}=\lim\mathscr{V}^{n}1$. An easy
induction on $n$ shows that $\mathscr{V}^{n}1$ is
$\mathscr{P}_{\mathsf{f}}^{n}1$ with the discrete topology; the key point is
that each set $\mathscr{P}_{\mathsf{f}}^{n}1$ is finite. The topology was
described in section 2.2: it has as a base the sets $\partial_{n}^{-1}(U)$ as
$U$ ranges over the subsets of $\mathscr{P}_{\mathsf{f}}^{n}1$. By Theorem
4.8, $\nu F$ is a Stone space.

In Appendix A, we present a concrete description of $V_{\omega}$ as the set of
compactly branching strongly extensional trees.

######  Remark 10.

Note that Theorem 4.8 also holds for Vietoris polynomial functors when we take
$\mathsf{Haus}$ as our base category. Hofmann et al. [12] consider other full
subcategories of $\mathsf{Top}$, and they also study the completeness of the
category of coalgebras for Vietoris polynomial functors $F$ (however, they
restrict to using finite products and finite coproducts in their definition of
Vietoris polynomial functors). For a Vietoris polynomial functor $F$ on
$\mathsf{Haus}$, the category of coalgebras is complete [12, Cor. 3.41].
Moreover, every subfunctor of $F$ has a terminal coalgebra [12, Cor. 4.6].

######  Remark 11.

Hofmann et al. [12, Ex. 2.27(2)] also consider a related construction called
the _lower Vietoris space_ of $X$. It is the set of all closed subsets of $X$
with the topology generated by all sets $U^{\Diamond}$, cf. (5). This again
yields a functor on $\mathsf{Top}$: a given continuous function is mapped to
$A\mapsto\overline{f[A]}$, where $\overline{f[A]}$ denotes the closure of
$f[A]$. Furthermore, one has a corresponding notion of lower Vietoris
polynomial functors. They prove that for such functors $F$ on the category of
stably compact spaces (defined in [12]), $\mathop{\mathsf{Coalg}}F$ is
complete [12, Thm. 3.35]. Furthermore, if a lower Vietoris polynomial functor
$F$ on $\mathsf{Top}$ can be restricted to that category, then it has a
terminal coalgebra obtained by finite iteration: $\nu F=V_{\omega}$ [12, Thm.
3.36]. Similar results hold for the category of spectral spaces and spectral
maps.

######  Remark 12.

Let us mention a very general result which applies in many situations to
deliver a terminal coalgebra: Makkai and Paré’s Limit Theorem [17, Thm.
5.1.6]. It implies that every accessible endofunctor
$F\colon\mathscr{A}\to\mathscr{A}$ on a locally presentable category has an
initial algebra and a terminal coalgebra. (Indeed, the theorem implies that
the category of $F$-coalgebras is cocomplete.) This result cannot be used here
because $\mathsf{Haus}$ is not locally presentable: it does not have a small
set of objects that is colimit-dense [3, Prop. 8.2].

######  Open Problem 4.15.

  1. 1.

Does every Vietoris polynomial functor on $\mathsf{Top}$ have a terminal
coalgebra?

  2. 2.

Does every Vietoris polynomial functor on $\mathsf{KHaus}$ as in 4.11 have an
initial algebra?

Item 1 above is equivalent to asking whether the result that $\nu F$ exists
for every Vietoris polynomial functor would remain true if we allowed non-
Hausdorff constants.

##  5 Hausdorff Polynomial Functors

Analogously to the Vietoris polynomial functors on $\mathsf{Top}$, we
introduce Hausdorff polynomial functors on $\mathsf{Met}$. Closer to the
situation of Kripke polynomial functors on $\mathsf{Set}$ than to Vietoris
polynomial functors on $\mathsf{Top}$, the Hausdorff polynomial functors on
$\mathsf{Met}$ have terminal coalgebras obtained in $\omega+\omega$ steps.

######  Notation 5.1.

The Hausdorff functor $\mathcal{H}\colon\mathsf{Met}\to\mathsf{Met}$ maps a
metric space $X$ to the space $\mathcal{H}X$ of all compact subsets of $X$
equipped with the Hausdorff distance111The definition goes back to Pompeiu
[19] and was popularized by Hausdorff [11, p. 293]. given by

$\bar{d}(S,T)=\max\left(\sup\nolimits_{x\in S}d(x,T),\sup\nolimits_{y\in
T}d(y,S)\right),\qquad\text{for $S,T\subseteq X$ compact},$

where $d(x,S)=\inf_{y\in S}d(x,y)$. In particular
$\bar{d}(\emptyset,T)=\infty$ for nonempty compact sets $T$. For a non-
expanding map $f\colon X\to Y$ we have $\mathcal{H}f\colon S\mapsto f[S]$.

######  Remark 13.

  1. 1.

The functors $\mathscr{V}\colon\mathsf{Top}\to\mathsf{Top}$ and
$\mathcal{H}\colon\mathsf{Met}\to\mathsf{Met}$ are closely related: for
compact metric spaces $X$ the Vietoris space $\mathscr{V}X$ is precisely the
topological space induced by the Hausdorff space $\mathcal{H}X$.

  2. 2.

Some authors define $\mathcal{H}X$ to consist of all _nonempty_ compact
subsets of $X$. However, Hausdorff [11] did not exclude $\emptyset$, and the
above formula works (as already indicated) without such an exclusion.

######  Remark 14.

  1. 1.

For a complete metric space, $\mathcal{H}X$ is complete again (see e.g.
Barnsley [7, Thm. 7.1]). Thus $\mathcal{H}$ restricts to a functor on the
category $\mathsf{CMS}$ of complete metric spaces, which we denote by the same
symbol $\mathcal{H}$.

  2. 2.

Let $\mathsf{UMet}$ denote the category of (extended) ultrametric spaces: the
full subcategory of $\mathsf{Met}$ given by spaces satisfying the following
stronger version of the triangle inequality:

$d(x,z)\leq\max\\{d(x,y),d(y,z)\\}.$

If $X$ is an ultrametric space, then so is $\mathcal{H}X$. To see this, let
$S,T,U\in\mathcal{H}X$. Write $p$ for $\max\\{\bar{d}(S,T),\bar{d}(T,U)\\}$.
For each $x\in S$, there is some $y\in T$ such that $d(x,y)\leq\bar{d}(S,T)$.
For this $y$, there is some $z\in U$ such that $d(y,z)\leq\bar{d}(T,U)$. So

$d(x,z)\leq\max\\{d(x,y),d(y,z)\\}\leq\max\\{\bar{d}(S,T),\bar{d}(T,U)\\}=p.$

It follows that $d(x,U)\leq p$. This for all $x\in X$ shows that $d(S,U)\leq
p$. Note that $p=\max\\{\bar{d}(U,T),\bar{d}(T,S)\\}$. The same argument shows
that $\sup_{z\in U}d(z,S)\leq p$. So we have $\bar{d}(S,U)\leq p$. This proves
the ultrametric inequality.

We again denote the restriction of the Hausdorff functor to $\mathsf{UMet}$ is
denoted by $\mathcal{H}$.

  3. 3.

For a discrete metric space $X$ (where all distances are $0$ or $1$),
$\mathcal{H}X$ is the discrete space formed by all finite subsets of $X$.

  4. 4.

For an arbitrary metric space $X$, the nonempty finite subsets of $X$ form a
dense set in $\mathcal{H}X$. Indeed, given a nonempty compact set $S\subseteq
X$, for every $\varepsilon>0$, there exists a nonempty finite set $T\subseteq
S$ such that $S$ is covered by $\varepsilon$-balls around the points in $T$.
Therefore $d(x,T)\leq\varepsilon$ for all $x\in S$, and we have $d(y,S)=0$ for
all $y\in T$. This implies that $\bar{d}(S,T)\leq\varepsilon$.

######  Example 5.2.

  1. 1.

For the Hausdorff functor, a terminal coalgebra is carried by the space of all
finitely branching strongly extensional trees equipped with the discrete
metric. This follows from the finite power-set functor
$\mathscr{P}_{\mathsf{f}}$ having its terminal coalgebra formed by those trees
(3.5). Indeed, the terminal-coalgebra chain $V_{i}$ ($i\in\mathsf{Ord}$) for
$\mathcal{H}$ is obtained by equipping the sets in the terminal-coalgebra
chain for $\mathscr{P}_{\mathsf{f}}$ with the discrete metric. Furthermore,
since limits in $\mathsf{Met}$ (or $\mathsf{CMS}$) are set-based, we see that
both chains converge in exactly $\omega+\omega$ steps. Therefore
$\nu\mathcal{H}=V_{\omega+\omega}$.

It follows that, unlike the Vietoris functor, the Hausdorff functor does not
preserve limits of $\omega^{\mathsf{op}}$-chains: the terminal-coalgebras
chain for $\mathcal{H}(-)$ does not converge before $\omega+\omega$ steps (see
5.2.1). Thus this functor does not preserve the limit
$V_{\omega}=\lim_{n<\omega}V_{n}$.

######  Definition 15.

Let $(X_{n})_{n<\omega}$ be an $\omega^{\mathsf{op}}$-chain in $\mathsf{Met}$.
A cone $r_{n}\colon M\to X_{n}$ is _isometric_ if for all $x,y\in M$ we have
$d(x,y)=\sup_{n\in\mathds{N}}d(r_{n}(x),r_{n}(y))$.

By section 2.3, limit cones of $\omega^{\mathsf{op}}$-chains in $\mathsf{Met}$
are isometric.

######  Proposition 5.3.

The Hausdorff functor preserves isometric cones of
$\omega^{\mathsf{op}}$-chains.

######  Proof 5.4.

Let $(X_{n})_{n<\omega}$ be an $\omega^{\mathsf{op}}$-chain with connecting
maps $f_{n}\colon X_{n+1}\to X_{n}$. Given an isometric cone $\ell_{n}\colon
M\to X_{n}$ ($n<\omega$), we prove that the cone
$\mathcal{H}\ell_{n}\colon\mathcal{H}M\to\mathcal{H}X_{n}$ is also isometric:

$\bar{d}(S,T)=\sup_{n<\omega}\bar{d}(\ell_{n}(S),\ell_{n}(T))\qquad\text{for
all compact subset $S,T\subseteq M$.}$

We can assume that $S$ and $T$ are nonempty and finite: since finite sets are
dense in $\mathcal{H}M$ by 14.4, and the maps $\ell_{n}$ are (non-expanding
whence) continuous, the desired equality then holds for all pairs in
$\mathcal{H}M$. The case where $S$ or $T$ is empty is trivial.

Since every $\ell_{n}$ is non-expanding, we only need to prove that
$\bar{d}(S,T)\leq c$ holds for
$c=\sup_{n<\omega}\bar{d}(\ell_{n}[S],\ell_{n}[T])$. For this, we show that
for every $\varepsilon>0$, $\bar{d}(S,T)\leq c+\varepsilon$. By the definition
of the Hausdorff metric $\bar{d}$, it suffices to prove that for every $x\in
S$ we have $d(x,T)\leq c+\varepsilon$. By symmetry, we then also have
$d(y,S)\leq c+\varepsilon$ for every $y\in T$.

Given $y\in T$ we have $d(x,y)=\sup_{n<\omega}d(\ell_{n}(x),\ell_{n}(y))$.
Thus, there is a $k<\omega$ such that

$d(x,y)\leq d(\ell_{k}(x),\ell_{k}(y))+\varepsilon.$

Since $T$ is finite, we can choose $k$ such that this inequality holds for all
$y\in T$. By definition,

$\bar{d}(\ell_{k}(x),\ell_{k}[T])=\inf_{y\in
T}d(\ell_{k}(x),\ell_{k}(y))\qquad\text{in $X_{k}$}.$

Again using that $T$ is finite, we can pick some $y\in T$ such that
$d(\ell_{k}(x),\ell_{k}[T])=d(\ell_{k}(x),\ell_{k}(y))$. With this $y$ we
conclude that
$\hskip 15.00002ptd(x,T)\leq d(x,y)\leq
d(\ell_{k}(x),\ell_{k}(y))+\varepsilon=d(\ell_{k}(x),\ell_{k}[T])+\varepsilon\leq\bar{d}(\ell_{k}[S],\ell_{k}[T])+\varepsilon\leq
c+\varepsilon.$

######  Remark 16.

The Hausdorff functor preserves isometric embeddings and their intersections.
Indeed, for every subspace $X$ of a metric space $Y$, a set $S\subseteq X$ is
compact in $X$ iff it is so in $Y$. Moreover, given $S,T\in\mathcal{H}X$,
their distances in $\mathcal{H}X$ and $\mathcal{H}Y$ are the same. Thus,
$\mathcal{H}$ preserves isometric embeddings.

Given a collection $X_{i}\subseteq Y$ ($i\in I$) of subspaces, a set
$S\subseteq\bigcap_{i\in I}X_{i}$ is compact in $X$ iff it is so in $Y$ (and
therefore in every $X_{i}$). Thus $\mathcal{H}$ preserves that intersection.

######  Definition 17.

The _Hausdorff polynomial functors_ are the endofunctors on $\mathsf{Met}$
built from the Hausdorff functor, the constant functors, and the identity
functor, using product, coproduct, and composition. Thus, the Hausdorff
polynomial functors are built according to the following grammar (cf. 1):

$\textstyle F::=\mathcal{H}\mid A\mid\mathsf{Id}\mid\prod_{i\in
I}F_{i}\mid\coprod_{i\in I}F_{i}\mid FF,$

where $A$ ranges over all metric spaces and $I$ is an arbitrary index set.

######  Theorem 5.5.

Every Hausdorff polynomial functor $F\colon\mathsf{Met}\to\mathsf{Met}$ has a
terminal coalgebra obtained in $\omega+\omega$ steps: $\nu
F=V_{\omega+\omega}$.

######  Proof 5.6.

An easy induction over the structure of Hausdorff polynomial functors shows
that each such functor $F$ preserves:

  1. 1.

isometric cones of $\omega^{\mathsf{op}}$-chains, and

  2. 2.

isometric embeddings and their intersections.

The most important step is done in 5.3 and 16.

We conclude that in the terminal-coalgebra chain, the map $m\colon
V_{\omega+1}\to V_{\omega}$ from (2) in the Introduction is an isometric
embedding by item 1. By item 2, all of the maps $m,Fm,FFm,\ldots$ in the chain
$(V_{\omega+n})_{n<\omega}$ are isometric embeddings. Hence $F$ preserves the
intersection of the ensuing subspaces of $V_{\omega}$ viz. the limit
$V_{\omega+\omega}=\lim_{n<\omega}V_{\omega+n}$. Consequently, we have $\nu
F=V_{\omega+\omega}$.

######  Remark 18.

Note that if a Hausdorff polynomial functor $F$ uses only contants given by
complete metric spaces $A$, then it has a restriction to an endofunctor on
$\mathsf{CMS}$. Indeed, by an easy induction on the structure of $F$ one shows
that $FX$ is complete whenever $X$ is complete. Similarly, when $F$ uses
constants which are ultrametric spaces, then $F$ has a restriction on
$\mathsf{UMet}$.

Since $\mathsf{CMS}$ and $\mathsf{UMet}$ are closed under limits of
$\omega^{\mathsf{op}}$-chains in $\mathsf{Met}$, we obtain the following

######  Corollary 5.7.

Every Hausdorff polynomial functor on $\mathsf{CMet}$ or $\mathsf{UMet}$ has a
terminal coalgebra obtained in $\omega+\omega$ steps.

######  Corollary 5.8.

Every Hausdorff polynomial functor $F$ on $\mathsf{Met}$ or $\mathsf{CMS}$ has
an initial algebra.

Indeed, since Hausdorff polynomial functors preserve isometric embeddings,
this follows from Theorem 5.5, 2.1.2, and Theorem 2.2.

######  Remark 19.

We mentioned another possible approach to terminal coalgebras in 12. Let us
comment on the situation regarding the results on $\mathsf{Met}$ here. The
category $\mathsf{Met}$ is locally presentable (see e.g. [6, Ex. 2.3]). The
Limit Theorem does imply that on $\mathsf{Met}$, the Hausdorff polynomial
functors have terminal coalgebras. In more detail, the Hausdorff functor is
finitary: this was proved for its restriction to $1$-bounded metric spaces [5,
Sec. 3], and the proof for $\mathcal{H}$ itself is the same. An easy induction
then shows that every Hausdorff polynomial functor is accessible, so that the
Limit Theorem can be applied. However, our elementary proof shows that the
terminal coalgebra chain converges in $\omega+\omega$ steps. The proof of
Makkai and Paré’s Limit Theorem does not yield such a bound.

##  6 Variation: the Closed Subset Functor on $\mathsf{Met}$

We have been concerned with the Hausdorff functor taking a metric space $M$ to
the space of its nonempty compact subsets. For two variations, let us consider
$\mathscr{P}_{\mathsf{cl}}\colon\mathsf{Met}\to\mathsf{Met}$ taking $M$ to the
set of its _closed_ subsets, and its subfunctor
$\mathscr{P}_{\mathsf{cl}}^{\prime}\colon\mathsf{Met}\to\mathsf{Met}$ taking
$M$ to the set of its nonempty closed subsets. Both
$\mathscr{P}_{\mathsf{cl}}M$ and $\mathscr{P}_{\mathsf{cl}}^{\prime}M$ are
given the Hausdorff metric. For a non-expanding map $f\colon X\to Y$, the non-
expanding map
$\mathscr{P}_{\mathsf{cl}}f\colon\mathscr{P}_{\mathsf{cl}}X\to\mathscr{P}_{\mathsf{cl}}Y$
sends a closed subset $S$ of $X$ to the closure of $f[S]$. This makes
$\mathscr{P}_{\mathsf{cl}}$ and $\mathscr{P}_{\mathsf{cl}}^{\prime}$ functors.
Due to the empty set, $\mathscr{P}_{\mathsf{cl}}$ is a closer analog of
$\mathcal{H}$. It is natural to ask whether the positive results of Section 5
hold for these functors $\mathscr{P}_{\mathsf{cl}}$ and
$\mathscr{P}_{\mathsf{cl}}^{\prime}$. As proved by van Breugel [23, Prop. 8],
the functor $\mathscr{P}_{\mathsf{cl}}$ has no terminal coalgebra. Turning to
$\mathscr{P}_{\mathsf{cl}}^{\prime}$, this functor has an initial algebra
given by the empty metric space and a terminal coalgebra carried by a
singleton metric space. But $\mathscr{P}_{\mathsf{cl}}^{\prime}$ has no other
fixed points (see van Breugel et al. [24, Cor. 5]), where an object $X$ is a
_fixed point_ of an endofunctor $F$ if $FX\cong X$. We provide below a
different, shorter proof.

######  Remark 20.

  1. 1.

A subset $X$ of a metric space is _$\delta$ -discrete_ if whenever $x\neq y$
are elements of $X$, $d(x,y)\geq\delta$. Every subset of a $\delta$-discrete
set is $\delta$-discrete, and every such set is closed. Moreover, if $C$ and
$D$ are different subsets of a $\delta$-discrete set, then
$\bar{d}(C,D)\geq\delta$.

  2. 2.

A subset $S$ of an ordinal $i$ is _cofinal_ if for all $j<i$ there is some
$k\in S$ with $j\leq k<i$. If $S$ is not cofinal, then its complement
$i\setminus S$ must be so. (But it is possible that both $S$ and $i\setminus
S$ are cofinal in $i$.)

######  Theorem 6.1.

There is no isometric embedding $\mathscr{P}_{\mathsf{cl}}^{\prime}M\to M$
when $|M|\geq 2$.

######  Proof 6.2.

Suppose towards a contradiction that $\iota\colon\mathscr{P}_{\mathsf{cl}}M\to
M$ were an isometric embedding where $|M|\geq 2$. If all distances in $M$ are
$0$ or $\infty$, then $\mathscr{P}_{\mathsf{cl}}^{\prime}M$ is the nonempty
power set of $M$. In this case, our result follows from the fact that for
$|M|\geq 2$, $M$ has more nonempty subsets than elements. Thus we fix distinct
points $a,b\in M$ of finite distance, and put $\delta=d(a,b)/2$. Let
$A=\\{x\in M:d(x,a)\leq\delta\\}$, and let $B=M\setminus A$. (In case
$d(a,b)=\infty$, we need to adjust this by setting $\delta=\infty$, and $B$ to
be the points whose distance to $a$ is finite. But we shall not present the
argument in this case.)

We proceed to define an ordinal-indexed sequence of elements $x_{i}\in M$. We
also prove that each set $S_{i}=\\{x_{j}:j<i\\}$ is $\delta$-discrete, and we
put

$X_{i}=\begin{cases}A&\text{if $\\{j<i:x_{j}\in A\\}$ is cofinal in $i$}\\\
B&\text{else}.\end{cases}$

For $i=0$, put $x_{0}=\iota(\\{a,b\\})$. Given an ordinal $i>0$, we put

$x_{i}=\iota(X_{i}\cap S_{i}).$

Being nonempty (since $i>0$) and $\delta$-discrete, $X_{i}\cap S_{i}$ lies in
$\mathscr{P}_{\mathsf{cl}}^{\prime}M$.

The remainder of our proof consists of showing that for every ordinal $i$:

$d(x_{j},x_{k})\geq\delta\qquad\text{for $0\leq j<k\leq i$}.$

We proceed by transfinite induction. Assume that our claim holds for every
$k<i$ and then prove it for $i$. The base case $i=0$ is trivial. For $i>0$,
note first that it follows from the induction hypothesis that $S_{i}$ is
$\delta$-discrete.

Hence, we need only verify that $d(x_{j},x_{i})\geq\delta$ when $0\leq j<i$.
We argue the case $X_{i}=A$; when $X_{i}=B$, the argument is similar, mutatis
mutandis. For $j=0$, recall that $x_{0}=\iota(\\{a,b\\})$ and
$x_{i}=\iota(A\cap S_{i})$. Since $b$ has distance at least $\delta$ from
every element of $A$, we obtain $\bar{d}(\\{a,b\\},A\cap S_{i})\geq\delta$. As
$\iota$ is an isometric embedding, this distance is also $d(x_{0},x_{i})$. Now
let $j>0$. Since we have $X_{i}=A$, let $k$ be such that $j\leq k<i$ and
$x_{k}\in A$. Now either $x_{j}=\iota(A\cap S_{j})$ or else $x_{j}=\iota(B\cap
S_{j})$.

In the first case, note that $x_{k}\in A\cap S_{i}$ since $k<i$, and
$x_{k}\notin S_{j}$ by the definition of $S_{j}$ since $k\geq j$. So $A\cap
S_{j}$ and $A\cap S_{i}$ are different nonempty subsets of the
$\delta$-discrete set $S_{i}$. Hence, the distance between these sets is at
least $\delta$, and therefore we have $d(x_{j},x_{i})\geq\delta$.

In the second case, $B\cap S_{j}$ is a nonempty subset of $B$, and thus again
it not equal to $A\cap S_{i}$. So again we see that
$d(x_{j},x_{i})=\bar{d}(B\cap S_{j},A\cap S_{i})\geq\delta$.

We now obtain the desired contradiction since $(x_{i})$ is an ordinal-indexed
sequence of pairwise distinct elements of $M$.

######  Corollary 6.3.

  1. 1.

The functor
$\mathscr{P}_{\mathsf{cl}}^{\prime}\colon\mathsf{Met}\to\mathsf{Met}$ has no
fixed points except the empty set and the singletons.

  2. 2.

The functor $\mathscr{P}_{\mathsf{cl}}\colon\mathsf{Met}\to\mathsf{Met}$
admits no isometric embedding $\mathscr{P}_{\mathsf{cl}}M\to M$, whence has no
fixed point.

######  Proof 6.4.

The first item is immediate from Theorem 6.1. For the second one, observe that
the inclusion map
$e\colon\mathscr{P}_{\mathsf{cl}}^{\prime}M\to\mathscr{P}_{\mathsf{cl}}M$ is
an isometric embedding. Assuming that there were an isometric embedding
$\iota\colon\mathscr{P}_{\mathsf{cl}}M\to M$, we see that $M$ cannot be empty
(since $\mathscr{P}_{\mathsf{cl}}M$ is nonempty) or a singleton (since then
$|\mathscr{P}_{\mathsf{cl}}M|=2$). Hence $|M|\geq 2$. Moreover, we obtain an
isometric embedding $\iota\cdot e\colon\mathscr{P}_{\mathsf{cl}}^{\prime}M\to
M$, contradicting Theorem 6.1.

##  7 Summary

We have investigated versions of the finite power set functor for the
categories $\mathsf{Haus}$ and $\mathsf{Met}$. Our main results are that the
Vietoris functor $\mathscr{V}$, and indeed all Vietoris polynomial functors,
have terminal coalgebras obtained in $\omega$ steps of the terminal-coalgebra
chain. The same holds for the Hausdorff polynomial functors on $\mathsf{Met}$,
but the iteration takes $\omega+\omega$ steps and so the underlying reasons
are different.

Our work on the Kripke and Hausdorff polynomial functors highlights a
technique which we feel could be of wider interest. To prove that a terminal
coalgebra exists in a situation where the limit of the
$\omega^{\mathsf{op}}$-chain (1) is not preserved by the functor, one could
try to find preservation properties which imply that the limit of the
$\omega^{\mathsf{op}}$-chain $(V_{\omega+n})_{n}$ was preserved. In
$\mathsf{Set}$, we used finitarity and preservation of monomorphisms and
intersections, and in $\mathsf{Met}$ we used preservation of intersections,
isometric embeddings, and isometric cones.

We have also seen that for the functor $\mathscr{P}_{\mathsf{cl}}$ on
$\mathsf{Met}$, there is no fixed point and hence no terminal coalgebra. We
leave open the question of whether every Vietoris polynomial functor on
$\mathsf{Top}$ has a terminal coalgebra.

#### Acknowledgement

We are grateful to Pedro Nora for discussions on the proof of 4.5.

##  Appendix A Trees and the Limit of the Terminal-Coalgebra Chain for
$\mathscr{P}_{\mathsf{f}}$

We give the description of $V_{\omega}$ for $\mathscr{P}_{\mathsf{f}}$ due to
Worrell [26]. We provide a full exposition to the results which Worrell stated
without proof.

A _tree_ is a directed graph $t$ with a distinguished node $\mbox{\sf
root}(t)$ from which every other node can be reached by a unique directed
path. Every tree in our sense must have a root, so there is no empty tree. All
of our trees are _unordered_. We always identify isomorphic trees.

######  Definition 21.

  1. 1.

We use the notation $t_{x}$ for the subtree of $t$ rooted in the node $x$ of
$t$.

  2. 2.

A tree $t$ is _extensional_ if for every node $x$ distinct children $y$ and
$z$ of $x$ give different (that is, non-isomorphic) subtrees $t_{y}$ and
$t_{z}$.

  3. 3.

A _graph bisimulation_ between two trees $t$ and $u$ is a relation between the
nodes of $t$ and the nodes of $u$ with the property that whenever $x$ and $y$
are related: (a) every child of $x$ is related to some child of $y$, and (b)
every child of $y$ is related to some child of $x$.

  4. 4.

A _tree bisimulation_ between two trees $t$ and $u$ is a graph bisimulation
$R$ with the additional properties that that

    1. (a)

The nodes $\mbox{\sf root}(t)$ and $\mbox{\sf root}(u)$ are related; the roots
are not related to other nodes; and

    2. (b)

whenever two nodes are related, their parents are also related.

  5. 5.

Two trees are _tree bisimilar_ if there is a tree bisimulation between them.

  6. 6.

A tree $t$ is _strongly extensional_ if every tree bisimulation on it is a
subset of the diagonal

$\Delta_{t}=\\{(x,x):x\in t\\}.$

In other words, $t$ is strongly extensional iff distinct children $x$ and $y$
of the same node define subtrees $t_{x}$ and $t_{y}$ which are _not_ tree
bisimilar.

######  Remark 22.

  1. 1.

Every composition and every union of tree bisimulations is again a tree
bisimulation. In addition, the opposite relation of every tree bisimulation is
a tree bisimulation: if $R$ is a tree bisimulation from $t$ to $u$, then
$R^{\mathsf{op}}$ is a tree bisimulation from $u$ to $t$. Consequently, the
largest tree bisimulation on every tree is an equivalence relation.

  2. 2.

A subtree $s$ of a strongly extensional tree $t$ is strongly extensional.
Indeed, if $R$ is a tree bisimulation on $s$, then $R\cup\Delta_{t}$ is a tree
bisimulation on $t$. Since $R\cup\Delta_{t}\subseteq\Delta_{t}$, we have
$R\subseteq\Delta_{s}$.

######  Lemma A.1.

If $t$ and $u$ are strongly extensional and related by a tree bisimulation,
then we have $t=u$.

######  Proof A.2.

Let $R$ be a tree bisimulation between $t$ and $u$. By 22,
$R^{\mathsf{op}}\cdot R$ is a tree bisimulation on $t$, whence
$R^{\mathsf{op}}\cdot R\subseteq\Delta_{t}$ by strong extensionality. But
every node of $t$ is related to at least one node of $u$ (use induction on the
depth of nodes) implying that $R^{\mathsf{op}}\cdot R=\Delta_{t}$. Similarly,
$R\cdot R^{\mathsf{op}}=\Delta_{u}$. Thus, $R$ (is a function and it) is an
isomorphism of trees, and we identify such trees.

######  Notation A.3.

  1. 1.

Let $\mathcal{T}$ be the class of trees. We define maps
$\partial_{n}\colon\mathcal{T}\to V_{n}=\mathscr{P}_{\mathsf{f}}^{n}1$ as
follows: $\partial_{0}$ is the unique map to $1$, and given the map
$\partial_{n}$ and a tree $t$, we put

$\partial_{n+1}(t)=\\{\partial_{n}(t_{x}):\text{$x$ is a child of the root of
$t$}\\}.$

On the right we have a subset of $\mathscr{P}_{\mathsf{f}}^{n}1$, and this is
an element of $\mathscr{P}_{\mathsf{f}}^{n+1}1$.

  2. 2.

The trees $t$ and $u$ are _Barr equivalent_ provided that
$\partial_{n}t=\partial_{n}u$ for all $n$. We write $t\approx u$ in this case.

  3. 3.

For every tree $t$, we define maps $\rho^{t}_{n}\colon t\to
V_{n}=\mathscr{P}_{\mathsf{f}}^{n}1$ in the following way: $\rho^{t}_{0}$ is
the unique map $t\to 1$, and for all nodes $x$ of $t$,
$\rho^{t}_{n+1}(x)=\\{\rho^{t}_{n}(y):\mbox{$y$ is a child of $x$ in $t$}\\}$.
This family of maps $\rho^{t}_{n}$ is a cone: we have
$\rho^{t}_{n}=v_{m,n}\cdot\rho^{t}_{m}$ for every connecting map
$v_{m,n}\colon\mathscr{P}_{\mathsf{f}}^{m}1\to\mathscr{P}_{\mathsf{f}}^{n}1$,
$m\geq n$. Hence, there is a unique map $\rho^{t}_{\omega}\colon t\to
V_{\omega}$ such that $\ell_{n}\cdot\rho^{t}_{\omega}=\rho^{t}_{n}$ for all
$n$.

######  Remark 23.

Note that $V_{n}=\mathscr{P}_{\mathsf{f}}^{n}1$ may be described as the set of
all extensional trees of height at most $n$. Indeed, $1$ is described as the
singleton set consisting of the root-only tree, and every finite set of
extensional trees in $V_{n+1}=\mathscr{P}_{\mathsf{f}}V_{n}$ is represented by
the extensional tree obtained by tree-tupling the trees from the given set.

######  Remark 24.

  1. 1.

If $\rho^{t}_{n+1}(a)=\rho^{t}_{n+1}(b)$, then for all children $a^{\prime}$
of $a$, there is some child $b^{\prime}$ of $b$ and
$\rho^{t}_{n}(a^{\prime})=\rho^{t}_{n}(b^{\prime})$. This is easy to see from
the definition of $\rho^{t}_{n+1}$.

  2. 2.

For all trees $t$, $\rho^{t}_{i}(\mbox{\sf root}(t))=\partial_{i}(t).$
Furthermore, let $b\colon t\to\mathcal{T}$ be given by $b(x)=t_{x}$. Then
$\rho^{t}_{i}=\partial_{i}\cdot b$.

######  Definition 25.

Let $x_{0},x_{1},\ldots,$ be a sequence of nodes in a tree $t$, and let $y$
also be a node in $t$. We write

$\lim x_{n}=y$

to mean that for every $n$ there is some $m$ such that
$\rho^{t}_{n}(x_{p})=\rho^{t}_{n}(y)$ whenever $p\geq m$.

A tree $t$ is _compactly branching_ if for all nodes $x$ of $t$, the set of
children of $x$ is _sequentially compact_ : for every sequence of $(y_{n})$ of
children of $x$ there is a subsequence $(w_{n})$ of $(y_{n})$ and some child
$z$ of $x$ such that $\lim{w_{n}}={z}$.

######  Example A.4.

The following tree $t$ is not compactly branching:

$t\colon\qquad\leavevmode\hbox to91.29pt{\vbox
to55.21pt{\pgfpicture\makeatletter\hbox{\hskip 40.9272pt\lower-53.21414pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}
{{}}{{{{}}}}{}{}{}\hbox{\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}} {{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{-21.99963pt}{-17.07138pt}\pgfsys@curveto{-21.99963pt}{-15.9668pt}{-22.89505pt}{-15.07138pt}{-23.99963pt}{-15.07138pt}\pgfsys@curveto{-25.10422pt}{-15.07138pt}{-25.99963pt}{-15.9668pt}{-25.99963pt}{-17.07138pt}\pgfsys@curveto{-25.99963pt}{-18.17596pt}{-25.10422pt}{-19.07138pt}{-23.99963pt}{-19.07138pt}\pgfsys@curveto{-22.89505pt}{-19.07138pt}{-21.99963pt}{-18.17596pt}{-21.99963pt}{-17.07138pt}\pgfsys@closepath\pgfsys@moveto{-23.99963pt}{-17.07138pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.99963pt}{-17.07138pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-37.5942pt}{-18.25194pt}\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_{0}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{-1.63011pt}{-1.15952pt}\pgfsys@lineto{-22.3699pt}{-15.91214pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}} {{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{2.0pt}{-17.07138pt}\pgfsys@curveto{2.0pt}{-15.9668pt}{1.10458pt}{-15.07138pt}{0.0pt}{-15.07138pt}\pgfsys@curveto{-1.10458pt}{-15.07138pt}{-2.0pt}{-15.9668pt}{-2.0pt}{-17.07138pt}\pgfsys@curveto{-2.0pt}{-18.17596pt}{-1.10458pt}{-19.07138pt}{0.0pt}{-19.07138pt}\pgfsys@curveto{1.10458pt}{-19.07138pt}{2.0pt}{-18.17596pt}{2.0pt}{-17.07138pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-17.07138pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-17.07138pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.59456pt}{-18.25194pt}\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}}} { {{{{}}}}{}{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{-2.00024pt}\pgfsys@lineto{0.0pt}{-15.07141pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{2.0pt}{-34.14276pt}\pgfsys@curveto{2.0pt}{-33.03818pt}{1.10458pt}{-32.14276pt}{0.0pt}{-32.14276pt}\pgfsys@curveto{-1.10458pt}{-32.14276pt}{-2.0pt}{-33.03818pt}{-2.0pt}{-34.14276pt}\pgfsys@curveto{-2.0pt}{-35.24734pt}{-1.10458pt}{-36.14276pt}{0.0pt}{-36.14276pt}\pgfsys@curveto{1.10458pt}{-36.14276pt}{2.0pt}{-35.24734pt}{2.0pt}{-34.14276pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-34.14276pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-34.14276pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{-19.07162pt}\pgfsys@lineto{0.0pt}{-32.14279pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}} {{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{25.99963pt}{-17.07138pt}\pgfsys@curveto{25.99963pt}{-15.9668pt}{25.10422pt}{-15.07138pt}{23.99963pt}{-15.07138pt}\pgfsys@curveto{22.89505pt}{-15.07138pt}{21.99963pt}{-15.9668pt}{21.99963pt}{-17.07138pt}\pgfsys@curveto{21.99963pt}{-18.17596pt}{22.89505pt}{-19.07138pt}{23.99963pt}{-19.07138pt}\pgfsys@curveto{25.10422pt}{-19.07138pt}{25.99963pt}{-18.17596pt}{25.99963pt}{-17.07138pt}\pgfsys@closepath\pgfsys@moveto{23.99963pt}{-17.07138pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.99963pt}{-17.07138pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{29.53261pt}{-19.57138pt}\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{{$\quad\cdots$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.40508pt}{-18.25194pt}\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_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{{}}}}{}{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{1.63011pt}{-1.15952pt}\pgfsys@lineto{22.3699pt}{-15.91214pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{25.99963pt}{-34.14276pt}\pgfsys@curveto{25.99963pt}{-33.03818pt}{25.10422pt}{-32.14276pt}{23.99963pt}{-32.14276pt}\pgfsys@curveto{22.89505pt}{-32.14276pt}{21.99963pt}{-33.03818pt}{21.99963pt}{-34.14276pt}\pgfsys@curveto{21.99963pt}{-35.24734pt}{22.89505pt}{-36.14276pt}{23.99963pt}{-36.14276pt}\pgfsys@curveto{25.10422pt}{-36.14276pt}{25.99963pt}{-35.24734pt}{25.99963pt}{-34.14276pt}\pgfsys@closepath\pgfsys@moveto{23.99963pt}{-34.14276pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.99963pt}{-34.14276pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{{}}}}{}{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{23.99963pt}{-19.07162pt}\pgfsys@lineto{23.99963pt}{-32.14279pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{25.99963pt}{-51.21414pt}\pgfsys@curveto{25.99963pt}{-50.10956pt}{25.10422pt}{-49.21414pt}{23.99963pt}{-49.21414pt}\pgfsys@curveto{22.89505pt}{-49.21414pt}{21.99963pt}{-50.10956pt}{21.99963pt}{-51.21414pt}\pgfsys@curveto{21.99963pt}{-52.31873pt}{22.89505pt}{-53.21414pt}{23.99963pt}{-53.21414pt}\pgfsys@curveto{25.10422pt}{-53.21414pt}{25.99963pt}{-52.31873pt}{25.99963pt}{-51.21414pt}\pgfsys@closepath\pgfsys@moveto{23.99963pt}{-51.21414pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{23.99963pt}{-51.21414pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{23.99963pt}{-36.143pt}\pgfsys@lineto{23.99963pt}{-49.21417pt}\pgfsys@stroke\pgfsys@invoke{
} }\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}}$

To see this, consider the sequence $y_{0}$, $y_{1}$, $\ldots$. Note that for
$n\geq m$, $\rho^{t}_{n}(y_{n})=\partial_{i}(t_{y_{n}})=t_{y_{m}}$. We claim
that for every subsequence $(y_{k_{n}})$ of this sequence $(y_{n})$ there is
no $y_{p}$ such that $\lim_{n}y_{k_{n}}=y_{p}$. To simplify the notation, we
only verify this for the sequence $(y_{n})$ itself. It does not converge to
any fixed element $y_{m}$ because for $p>m$,

$\rho^{t}_{p}(y_{m})=\partial_{p}(t_{y_{m}})\neq\partial_{p}(t_{y_{p}})=\rho^{t}_{p}(y_{p}).$

In contrast, the following tree is compactly branching (also observe also that
$t\approx t^{\prime}$):

$t^{\prime}\colon\qquad\leavevmode\hbox to124.32pt{\vbox
to88.15pt{\pgfpicture\makeatletter\hbox{\hskip 55.95564pt\lower-86.1515pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}
{{}}{{{{}}}}{}{}{}{}\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}} {{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{-39.99936pt}{-17.07138pt}\pgfsys@curveto{-39.99936pt}{-15.9668pt}{-40.89478pt}{-15.07138pt}{-41.99936pt}{-15.07138pt}\pgfsys@curveto{-43.10394pt}{-15.07138pt}{-43.99936pt}{-15.9668pt}{-43.99936pt}{-17.07138pt}\pgfsys@curveto{-43.99936pt}{-18.17596pt}{-43.10394pt}{-19.07138pt}{-41.99936pt}{-19.07138pt}\pgfsys@curveto{-40.89478pt}{-19.07138pt}{-39.99936pt}{-18.17596pt}{-39.99936pt}{-17.07138pt}\pgfsys@closepath\pgfsys@moveto{-41.99936pt}{-17.07138pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-41.99936pt}{-17.07138pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-52.62263pt}{-19.22415pt}\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{{$z$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{{}}}}{}{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{-1.85344pt}{-0.75337pt}\pgfsys@lineto{-40.14658pt}{-16.31828pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{-39.99936pt}{-34.14276pt}\pgfsys@curveto{-39.99936pt}{-33.03818pt}{-40.89478pt}{-32.14276pt}{-41.99936pt}{-32.14276pt}\pgfsys@curveto{-43.10394pt}{-32.14276pt}{-43.99936pt}{-33.03818pt}{-43.99936pt}{-34.14276pt}\pgfsys@curveto{-43.99936pt}{-35.24734pt}{-43.10394pt}{-36.14276pt}{-41.99936pt}{-36.14276pt}\pgfsys@curveto{-40.89478pt}{-36.14276pt}{-39.99936pt}{-35.24734pt}{-39.99936pt}{-34.14276pt}\pgfsys@closepath\pgfsys@moveto{-41.99936pt}{-34.14276pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-41.99936pt}{-34.14276pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{{}}}}{}{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{-41.99936pt}{-19.07162pt}\pgfsys@lineto{-41.99936pt}{-32.14279pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{-39.99936pt}{-51.21414pt}\pgfsys@curveto{-39.99936pt}{-50.10956pt}{-40.89478pt}{-49.21414pt}{-41.99936pt}{-49.21414pt}\pgfsys@curveto{-43.10394pt}{-49.21414pt}{-43.99936pt}{-50.10956pt}{-43.99936pt}{-51.21414pt}\pgfsys@curveto{-43.99936pt}{-52.31873pt}{-43.10394pt}{-53.21414pt}{-41.99936pt}{-53.21414pt}\pgfsys@curveto{-40.89478pt}{-53.21414pt}{-39.99936pt}{-52.31873pt}{-39.99936pt}{-51.21414pt}\pgfsys@closepath\pgfsys@moveto{-41.99936pt}{-51.21414pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-41.99936pt}{-51.21414pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{{}}}}{}{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{-41.99936pt}{-36.143pt}\pgfsys@lineto{-41.99936pt}{-49.21417pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}} {{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{-39.99936pt}{-68.28552pt}\pgfsys@curveto{-39.99936pt}{-67.18094pt}{-40.89478pt}{-66.28552pt}{-41.99936pt}{-66.28552pt}\pgfsys@curveto{-43.10394pt}{-66.28552pt}{-43.99936pt}{-67.18094pt}{-43.99936pt}{-68.28552pt}\pgfsys@curveto{-43.99936pt}{-69.3901pt}{-43.10394pt}{-70.28552pt}{-41.99936pt}{-70.28552pt}\pgfsys@curveto{-40.89478pt}{-70.28552pt}{-39.99936pt}{-69.3901pt}{-39.99936pt}{-68.28552pt}\pgfsys@closepath\pgfsys@moveto{-41.99936pt}{-68.28552pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-41.99936pt}{-68.28552pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-45.74936pt}{-80.8185pt}\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{{$\vdots$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{-41.99936pt}{-53.21439pt}\pgfsys@lineto{-41.99936pt}{-66.28555pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}} {{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{-11.99979pt}{-17.07138pt}\pgfsys@curveto{-11.99979pt}{-15.9668pt}{-12.8952pt}{-15.07138pt}{-13.99979pt}{-15.07138pt}\pgfsys@curveto{-15.10437pt}{-15.07138pt}{-15.99979pt}{-15.9668pt}{-15.99979pt}{-17.07138pt}\pgfsys@curveto{-15.99979pt}{-18.17596pt}{-15.10437pt}{-19.07138pt}{-13.99979pt}{-19.07138pt}\pgfsys@curveto{-12.8952pt}{-19.07138pt}{-11.99979pt}{-18.17596pt}{-11.99979pt}{-17.07138pt}\pgfsys@closepath\pgfsys@moveto{-13.99979pt}{-17.07138pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.99979pt}{-17.07138pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-27.59435pt}{-18.25194pt}\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_{0}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{-1.26842pt}{-1.54672pt}\pgfsys@lineto{-12.7316pt}{-15.52493pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}} {{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{15.99979pt}{-17.07138pt}\pgfsys@curveto{15.99979pt}{-15.9668pt}{15.10437pt}{-15.07138pt}{13.99979pt}{-15.07138pt}\pgfsys@curveto{12.8952pt}{-15.07138pt}{11.99979pt}{-15.9668pt}{11.99979pt}{-17.07138pt}\pgfsys@curveto{11.99979pt}{-18.17596pt}{12.8952pt}{-19.07138pt}{13.99979pt}{-19.07138pt}\pgfsys@curveto{15.10437pt}{-19.07138pt}{15.99979pt}{-18.17596pt}{15.99979pt}{-17.07138pt}\pgfsys@closepath\pgfsys@moveto{13.99979pt}{-17.07138pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{13.99979pt}{-17.07138pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.40523pt}{-18.25194pt}\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}}} { {{{{}}}}{}{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{1.26842pt}{-1.54672pt}\pgfsys@lineto{12.7316pt}{-15.52493pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{15.99979pt}{-34.14276pt}\pgfsys@curveto{15.99979pt}{-33.03818pt}{15.10437pt}{-32.14276pt}{13.99979pt}{-32.14276pt}\pgfsys@curveto{12.8952pt}{-32.14276pt}{11.99979pt}{-33.03818pt}{11.99979pt}{-34.14276pt}\pgfsys@curveto{11.99979pt}{-35.24734pt}{12.8952pt}{-36.14276pt}{13.99979pt}{-36.14276pt}\pgfsys@curveto{15.10437pt}{-36.14276pt}{15.99979pt}{-35.24734pt}{15.99979pt}{-34.14276pt}\pgfsys@closepath\pgfsys@moveto{13.99979pt}{-34.14276pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{13.99979pt}{-34.14276pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{13.99979pt}{-19.07162pt}\pgfsys@lineto{13.99979pt}{-32.14279pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}} {{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{43.99936pt}{-17.07138pt}\pgfsys@curveto{43.99936pt}{-15.9668pt}{43.10394pt}{-15.07138pt}{41.99936pt}{-15.07138pt}\pgfsys@curveto{40.89478pt}{-15.07138pt}{39.99936pt}{-15.9668pt}{39.99936pt}{-17.07138pt}\pgfsys@curveto{39.99936pt}{-18.17596pt}{40.89478pt}{-19.07138pt}{41.99936pt}{-19.07138pt}\pgfsys@curveto{43.10394pt}{-19.07138pt}{43.99936pt}{-18.17596pt}{43.99936pt}{-17.07138pt}\pgfsys@closepath\pgfsys@moveto{41.99936pt}{-17.07138pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{41.99936pt}{-17.07138pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{47.53233pt}{-19.57138pt}\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{{$\quad\cdots$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{28.4048pt}{-18.25194pt}\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_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{{}}}}{}{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{1.85344pt}{-0.75337pt}\pgfsys@lineto{40.14658pt}{-16.31828pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{43.99936pt}{-34.14276pt}\pgfsys@curveto{43.99936pt}{-33.03818pt}{43.10394pt}{-32.14276pt}{41.99936pt}{-32.14276pt}\pgfsys@curveto{40.89478pt}{-32.14276pt}{39.99936pt}{-33.03818pt}{39.99936pt}{-34.14276pt}\pgfsys@curveto{39.99936pt}{-35.24734pt}{40.89478pt}{-36.14276pt}{41.99936pt}{-36.14276pt}\pgfsys@curveto{43.10394pt}{-36.14276pt}{43.99936pt}{-35.24734pt}{43.99936pt}{-34.14276pt}\pgfsys@closepath\pgfsys@moveto{41.99936pt}{-34.14276pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{41.99936pt}{-34.14276pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{{}}}}{}{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{41.99936pt}{-19.07162pt}\pgfsys@lineto{41.99936pt}{-32.14279pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@moveto{43.99936pt}{-51.21414pt}\pgfsys@curveto{43.99936pt}{-50.10956pt}{43.10394pt}{-49.21414pt}{41.99936pt}{-49.21414pt}\pgfsys@curveto{40.89478pt}{-49.21414pt}{39.99936pt}{-50.10956pt}{39.99936pt}{-51.21414pt}\pgfsys@curveto{39.99936pt}{-52.31873pt}{40.89478pt}{-53.21414pt}{41.99936pt}{-53.21414pt}\pgfsys@curveto{43.10394pt}{-53.21414pt}{43.99936pt}{-52.31873pt}{43.99936pt}{-51.21414pt}\pgfsys@closepath\pgfsys@moveto{41.99936pt}{-51.21414pt}\pgfsys@fill\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{41.99936pt}{-51.21414pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{41.99936pt}{-36.143pt}\pgfsys@lineto{41.99936pt}{-49.21417pt}\pgfsys@stroke\pgfsys@invoke{
} }\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}}$

To check the compactness, consider a sequence of children of the root, say
$({x_{n}})$. If there is an infinite subsequence which is constant, then of
course that sequence converges. If not, then there is a subsequence of
$({x_{n}})$, say $({w_{n}})$, where each $w_{n}$ is $y_{k}$ for some $k\geq
n$. In this case, $\lim_{n}({w_{n}})=z$. This is because for all but finitely
many $n$,
$\rho^{t}_{n}(z)=\partial_{n}(t_{z})=t_{w_{n}}=\partial_{n}(t_{w_{n}})=\rho^{t}_{n}(w_{n})$.

######  Lemma A.5.

If $t$ and $u$ are compactly branching, and if $\rho^{t}_{\omega}(\mbox{\sf
root}(t))=\rho^{u}_{\omega}(\mbox{\sf root}(u))$, then there is a tree
bisimulation between $t$ and $u$ which includes $\\{(x,y)\in t\times
u\colon\rho^{t}_{\omega}(x)=\rho^{u}_{\omega}(y)\\}.$

######  Proof A.6.

Given compactly branching trees $t$ and $u$, we define a relation $R\subseteq
t\times u$ inductively by

$\displaystyle x\mathbin{R}y\quad\mbox{iff}\quad$ (1) $x=\mbox{\sf root}(t)$
and $y=\mbox{\sf root}(u)$, or $x$ and $y$ have $R$-related parents, and
$\displaystyle\text{(2)\leavevmode\nobreak\
$\rho^{t}_{\omega}(x)=\rho^{u}_{\omega}(y)$}.$

Let us check that $R$ is a tree bisimulation. Suppose that $(x,y)$ are related
by $R$ as above, and let $x^{\prime}$ be a child of $x$ in $t$. Using 24.1 we
see that for each $n$, there is some child $y^{\prime}_{n}$ of $y$ in $u$ with
$\rho^{t}_{n}(x^{\prime})=\rho^{u}_{n}(y_{n}^{\prime})$. Consider the sequence
$y^{\prime}_{0}$, $y^{\prime}_{1}$, $\ldots$. Now
$\rho^{t}_{n}(x^{\prime})=\rho^{u}_{n}(y_{m}^{\prime})$ if $m\geq n$, since
$\rho^{t}_{n}$ and $\rho^{u}_{n}$ form cones:
$\rho^{t}_{n}(x^{\prime})=v_{m,n}\cdot\rho^{t}_{m}(x^{\prime})=v_{m,n}\cdot\rho^{u}_{m}(y_{m}^{\prime})=\rho^{u}_{n}(y_{m}^{\prime}).$
By sequential compactness, there is a subsequence $z_{0}$, $z_{1}$, $\ldots$,
and also some child $z^{*}$ of $y$ such that $\lim z_{n}=z^{*}$. Being a
subsequence, $\rho^{t}_{n}(x^{\prime})=\rho^{u}_{n}(z_{m})$ whenever $m\geq
n$. Let us check that for all $n$,
$\rho^{t}_{n}(x^{\prime})=\rho^{u}_{n}(z^{*})$. To see this, fix $n$ and let
$m\geq n$ be large enough so that for $p\geq m$,
$\rho^{u}_{n}(z_{p})=\rho^{u}_{n}(z^{*})$. Thus,
$\rho^{t}_{n}(x^{\prime})=\rho^{u}_{n}(z_{m})=\rho^{u}_{n}(z^{*})$. Thus,
$\rho^{t}_{\omega}(x^{\prime})=\rho^{u}_{\omega}(z^{*})$, which shows
$x^{\prime}\mathbin{R}z^{*}$, as desired.

The other half of the verification that $R$ is a tree bisimulation is similar.

######  Notation A.7.

In this section, $V_{\omega}$ denotes the limit of (1) for the finite power
set functor.

  1. 1.

We take the elements of $V_{\omega}$ to be compatible sequences $(x_{n})$.
That is, $x_{n}\in\mathscr{P}_{\mathsf{f}}^{n}1$ and
$\mathscr{P}_{\mathsf{f}}^{n}!(x_{n+1})=x_{n}$ for every $n<\omega$. To save
on notation, we write $x$ for $(x_{n})$. We consider the relation $\leadsto$
on $V_{\omega}$ defined by

$x\leadsto y\quad\mbox{iff}\quad\mbox{for all $n$, $y_{n}\in x_{n+1}$}.$ (5)

  2. 2.

Let $L^{+}$ be the set of nonempty finite sequences from $V_{\omega}$. We
write such a sequence with the notation $\langle{x^{1},\ldots,x^{n}}\rangle$.
We consider the relation $\Rightarrow$ on $L^{+}$ defined by

$\langle{x^{1},\ldots,x^{n}}\rangle\Rightarrow\langle{y^{1},\ldots,y^{m}}\rangle\quad\mbox{iff}\quad\mbox{$m=n+1$,
$x^{1}=y^{1}$, $\ldots$, $x^{n}=y^{n}$, and $x^{n}\leadsto y^{n+1}$}.$

In other words, $m=n+1$,
$\langle{y^{1},\ldots,y^{m-1}}\rangle=\langle{x^{1},\ldots,x^{n}}\rangle$, and
$x^{n}\leadsto y^{m}$.

  3. 3.

For each $x\in V_{\omega}$, let $\mathsf{tr}_{x}$ be the tree whose nodes are
the sequences $\langle{x,x^{2},\ldots,x^{n}}\rangle\in L^{+}$ whose first
entry is $x$, with root the one-point sequence $\langle{x}\rangle$, and with
graph relation the restriction of $\Rightarrow$. For readers familiar with
tree unfoldings of pointed graphs, $\mathsf{tr}_{x}$ is the tree unfolding of
the graph $(V_{\omega},\leadsto)$ at the point $x$.

  4. 4.

Finally, let

$T=\\{\mathsf{tr}_{x}:x\in V_{\omega}\\}.$ (6)

Recall the connecting maps
$\mathscr{P}_{\mathsf{f}}^{n}!\colon\mathscr{P}_{\mathsf{f}}^{n+1}1\to\mathscr{P}_{\mathsf{f}}^{n}1$.

######  Lemma A.8.

Let $x\in V_{\omega}$.

  1. 1.

For all $k$ and all $\langle{x,x^{2},\ldots,x^{n}}\rangle\in\mathsf{tr}_{x}$,
$\rho^{\mathsf{tr}_{x}}_{k}(\langle{x,x^{2},\ldots,x^{n}}\rangle)=x^{n}_{k}$.

  2. 2.

Let $R$ be a tree bisimulation on $\mathsf{tr}_{x}$. If
$\langle{x,x^{2},\ldots,x^{n}}\rangle\ R\
\langle{x,y^{2},\ldots,y^{n}}\rangle$, then for all $k$,

$\rho^{\mathsf{tr}_{x}}_{k}(\langle{x,x^{2},\ldots,x^{n}}\rangle)=\rho^{\mathsf{tr}_{x}}_{k}(\langle{x,y^{2},\ldots,y^{n}}\rangle).$

  3. 3.

The tree $\mathsf{tr}_{x}$ is strongly extensional and compactly branching,
and
$\partial_{\omega}(\mathsf{tr}_{x})=\rho^{\mathsf{tr}_{x}}_{\omega}(\langle{x}\rangle)=x$.

######  Proof A.9.

  1. 1.

By induction on $k$. For $k=0$, our result is clear: the codomain of
$\rho_{k}$ is $1$. Assume our result for $k$, fix $x\in L^{+}$ and
$\langle{x^{1},\ldots,x^{n}}\rangle\in\mathsf{tr}_{x}$. We first prove that

$\\{y_{k}:x^{n}\leadsto y\\}=x^{n}_{k+1}.$ (7)

Indeed, if $x^{n}\leadsto y$, then $y_{k}\in x^{n}_{k+1}$. Conversely, if
$a\in x^{n}_{k+1}$, we construct $y\in V_{\omega}$ such that $x^{n}\leadsto y$
with $y_{k}=a$. Note that

$x^{n}_{k}=\mathscr{P}_{\mathsf{f}}^{k}!(x^{n}_{k+1})=\mathscr{P}\mathscr{P}_{\mathsf{f}}^{k-1}!(x^{n}_{k+1})=\mathscr{P}_{\mathsf{f}}^{k-1}![x^{n}_{k+1}].$

Since $a\in x^{n}_{k+1}$, we have $\mathscr{P}_{\mathsf{f}}^{k-1}!(a)\in
x^{n}_{k}$. So we let $y_{k-1}=\mathscr{P}_{\mathsf{f}}^{k-1}!(a)$. We repeat
this argument to define $y_{k-2}$, $\ldots$, $y_{1}$, $y_{0}$; the point is
that $y_{k-i}\in x^{n}_{k-i+1}$ for $i=0,\ldots,k$. Choices are needed when we
go the other way from $k$. Note that

$\mathscr{P}_{\mathsf{f}}^{k+1}![x^{n}_{k+2}]=\mathscr{P}_{\mathsf{f}}(\mathscr{P}_{\mathsf{f}}^{k+1}!)(x^{n}_{k+2})=\mathscr{P}_{\mathsf{f}}^{k+2}!(x^{n}_{k+2})=x^{n}_{k+1}.$

Every set functor preserves surjective functions, and so
$\mathscr{P}_{\mathsf{f}}^{k+1}!$ is surjective. Thus there is some
$y_{k+1}\in x^{n}_{k+2}$ such that
$\mathscr{P}_{\mathsf{f}}^{k+1}!(y_{k+1})=y_{k}$. The same argument enables us
to find by recursion on $i$ a sequence $y_{k+i+1}\in x^{n}_{k+i+2}$ such that
$\mathscr{P}_{\mathsf{f}}^{k+i+1}!(y_{k+i+1})=y_{k+i}$. This defines $y$ such
that $x^{n}\leadsto y$ according to (5) with $y_{k}=a$.

The induction step is now easy:

$\displaystyle\rho^{\mathsf{tr}_{x}}_{k+1}(\langle{x,x^{2},\ldots,x^{n}}\rangle)$
$\displaystyle=\\{\rho^{\mathsf{tr}_{x}}_{k}(\langle{x,x^{2},\ldots,x^{n},y}\rangle):x^{n}\leadsto
y\\}$ $\displaystyle=\\{y_{k}:x^{n}\leadsto y\\}$ by induction hypothesis
$\displaystyle=x^{n}_{k+1}$ $\displaystyle\text{by\leavevmode\nobreak\
\eqref{eq:aux}}.$

  2. 2.

This again is an induction on $k$, and the steps are similar to what we have
just seen. We also note that tuples in $\mathsf{tr}_{x}$ related by a tree
bisimulation must have the same length.

  3. 3.

Note first that by item 1 with $n=1$, we have
$\rho^{\mathsf{tr}_{x}}_{k}(\langle{x}\rangle)=x_{k}$ for all $k$. This
implies that $\rho^{\mathsf{tr}_{x}}_{\omega}(\langle{x}\rangle)=x$. For the
strong extensionality, let $R$ be a tree bisimulation on $\mathsf{tr}_{x}$.
Suppose that $\langle{x,x^{2},\ldots,x^{n}}\rangle$ and
$\langle{x,y^{2},\ldots,y^{n}}\rangle$ are related by $R$. Using item 1 and 2,
we see that for all $k$, we have $x^{n}_{k}=y^{n}_{k}$. Thus $x^{n}=y^{n}$. In
addition, since $R$ is a tree bisimulation, the parents of the two nodes under
consideration are also related by $R$. So the same argument shows that
$x^{n-1}=y^{n-1}$. Continuing in this way shows that $x^{n-2}=y^{n-2}$,
$\ldots$, $x^{2}=y^{2}$. Hence
$\langle{x,x^{2},\ldots,x^{n}}\rangle=\langle{x,y^{2},\ldots,y^{n}}\rangle$.

Finally, we verify that $\mathsf{tr}_{x}$ is compactly branching. To simplify
the notation a little, we shall show this for children of the root
$\langle{x}\rangle$. So suppose we have an infinite sequence
${\langle{x,y^{1}}\rangle}$, ${\langle{x,y^{2}}\rangle}$, $\ldots$. Recall
that each set $\mathscr{P}_{\mathsf{f}}^{n}1$ is finite. By successively
thinning the sequence $y^{1}$, $y^{2}$, $\ldots$, we may assume that for all
$n\in\omega$ and all $p,q\geq n$, $y^{n}_{p}=y^{n}_{q}$. Let $z\in V_{\omega}$
be the ‘diagonal’ sequence $z_{n}=y^{n}_{n}$. Since every
$\langle{x,y^{n}}\rangle$ is a child of the root $\langle{x}\rangle$ (in
symbols: $\langle{x}\rangle\Rightarrow\langle{x,y^{n}}\rangle$), we have
$x\leadsto y^{n}$. This implies that for all $n$, we have $z_{n}=y^{n}_{n}\in
x_{n+1}$, whence $x\leadsto z$. Thus, $\langle{x,z}\rangle$ is a child of the
root of $\mathsf{tr}_{x}$. Recall from item 1 that
$\rho^{\mathsf{tr}_{x}}_{n}(\langle{x,z}\rangle)=z_{n}$. So we obtain the
desired conclusion: $\lim\langle{x,y^{n}}\rangle=\langle{x,z}\rangle$.

######  Lemma A.10.

For every tree $t$ there is a Barr-equivalent tree $t^{*}\in T$ such that
$t^{*}$ is strongly extensional and compactly branching.

######  Proof A.11.

Given any tree $t$, we have $x=\partial_{\omega}(t)\in V_{\omega}$. For all
$n$, $x_{n}=\partial_{n}(t)$. The tree $t^{*}=\mathsf{tr}_{x}$ in A.8.3 is
strongly extensional and compactly branching. Recall that the root of $t^{*}$
is $\langle{x}\rangle$. By A.8.1, we have that for all $n<\omega$,

$\partial_{n}(t^{*})=\rho^{t^{*}}_{n}(\mbox{\sf
root}(\mathsf{tr}_{x}))=\rho^{t^{*}}_{n}(\langle{x}\rangle)=x_{n}=\partial_{n}(t).$

This completes the proof.

######  Lemma A.12.

The set $T$ defined in (6) is the set of all compactly branching, strongly
extensional trees.

######  Proof A.13.

By A.8.3 we know that every tree in $T$ is strongly extensional and compactly
branching. For the reverse inclusion, let $t$ be compactly branching and
strongly extensional. Let $t^{*}$ be as in Lemma A.10 for $t$. By A.1 and A.5,
$t=t^{*}$. Thus $t\in T$.

######  Definition 26.

Let $D$ be the set of finitely branching strongly extensional trees. Let
$\delta\colon D\to\mathscr{P}_{\mathsf{f}}D$ take a strongly extensional tree
$t$ to the (finite) set of its subtrees $t_{x}$.

In this definition, we use 22.2: a subtree of a strongly extensional tree is
strongly extensional.

######  Theorem A.14 ([26]).

For the finite power set functor $\mathscr{P}_{\mathsf{f}}$ the following
hold:

  1. 1.

the maps $\partial_{n}\colon T\to\mathscr{P}_{\mathsf{f}}^{n}1$ given by
$\partial_{n}(\mathsf{tr}_{x})=x_{n}$ form a limit of (2); thus,
$V_{\omega}\cong T$,

  2. 2.

the coalgebra $(D,\delta)$ is terminal.

######  Proof A.15.

  1. 1.

The map $\varphi\colon V_{\omega}\to T$ given by $\varphi(x)=\mathsf{tr}_{x}$
is obviously surjective. Suppose that $\mathsf{tr}_{x}=\mathsf{tr}_{y}$. The
roots of these trees are $\langle{x}\rangle$ and $\langle{y}\rangle$. For all
$n$, we have that

$x_{n}=\rho^{\mathsf{tr}_{x}}_{n}(\langle{x}\rangle)=\rho^{\mathsf{tr}_{y}}_{n}(\langle{y}\rangle)=y_{n}.$

Thus
$\partial_{\omega}(\langle{x}\rangle)=\partial_{\omega}(\langle{y}\rangle)$.
By A.1 and A.5, $x=y$. So $\varphi$ is injective. The formula for
$\partial_{n}$ comes from A.8.1.

  2. 2.

We use Theorem 3.2. The map $m\colon V_{\omega+1}\to V_{\omega}$ in (2)
assigns to a finite set of trees in $V_{\omega}$ their tree-tupling. Its image
is the set of all strongly extensional, compactly branching trees which are
finitely branching at the root. An easy induction on $n$ shows that
$V_{\omega+n}$ is the set of all compactly branching, strongly extensional
trees $t$ with the property that the topmost $n$ levels of $t$ are finitely
branching. With this description, $V_{\omega+n}\subseteq D$, and the limit
$V_{\omega+\omega}$ is simply the intersection $D=\bigcap_{n}V_{\omega+n}$.
This shows that the carrier set of $\nu\mathscr{P}_{\mathsf{f}}$ is $D$. For
the structure map $\delta$, note that
$m\colon\mathscr{P}_{\mathsf{f}}V_{\omega}\to V_{\omega}$ in (2) is tree-
tupling, as are $\mathscr{P}_{\mathsf{f}}m$,
$\mathscr{P}_{\mathsf{f}}\mathscr{P}_{\mathsf{f}}m$, etc. It follows that in
the intersection, $D$, the coalgebra structure is the inverse of tree-tupling.

This concludes our work showing that for the finite power set functor
$\mathscr{P}_{\mathsf{f}}$, $V_{\omega}$ is the set $T$ of strongly
extensional, compactly branching trees, and the terminal coalgebra
$\nu\mathscr{P}_{\mathsf{f}}$ is the set $D$ of finitely branching, strongly
extensional trees.

## References

  * [1] Samson Abramsky.  A Cook’s Tour of the finitary non-well-founded sets.  In We Will Show Them: Essays in honour of Dov Gabbay, volume 1, pages 1–18. College Publications, 2005.
  * [2] Jiří Adámek.  Free algebras and automata realizations in the language of categories.  Comment. Math. Univ. Carolin., 15:589–602, 1974.
  * [3] Jiří Adámek, Miroslav Hušek, Jiří Rosický, and Walter Tholen.  Smallness in topology.  preprint; available at https://arxiv.org/abs/2302.00050, 2023.
  * [4] Jiří Adámek, Stefan Milius, and Lawrence S. Moss.  Initial algebras without iteration.  In Fabio Gaducci and Alexandra Silva, editors, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO), volume 211 of LIPIcs, pages 5:1–5:20. Schloss Dagstuhl, 2021.  URL: https://www.dagstuhl.de/dagpub/978-3-95977-212-9.
  * [5] Jiří Adámek, Stefan Milius, Lawrence S. Moss, and Henning Urbat.  On finitary functors and their presentations.  J. Comput. System Sci., 81(5):813–833, 2015.  http://dx.doi.org/10.1016/j.jcss.2014.12.002.
  * [6] Jiří Adámek and Jiří Rosický.  Approximate injectivity and smallness in metric-enriched categories.  J. Pure Appl. Algebra, 226(6), 2022.  Article 106974.
  * [7] Michael F. Barnsley.  Fractals Everywhere.  Morgan Kaufmann, 2nd edition, 1993.
  * [8] Michael Barr.  Coequalizers and free triples.  Math. Z., 116:307–322, 1970.
  * [9] Michael Barr.  Terminal coalgebras in well-founded set theory.  Theoret. Comput. Sci., 114(2):299–315, 1993.
  * [10] Samuel Eilenberg and Norman Steenrod.  Foundations of Algebraic Topology.  Princeton University Press, 1952.
  * [11] Felix Hausdorff.  Grundzüge der Mengenlehre.  Veit & Comp., Leipzig, 1914.
  * [12] Dirk Hofmann, Renato Neves, and Pedro Nora.  Limits in categories of Vietoris coalgebras.  Math. Structures Comput. Sci., 29(4):552–587, 2019.
  * [13] Bart Jacobs.  Introduction to Coalgebra. Towards Mathematics of States and Observation.  Cambridge University Press, 2016.
  * [14] Peter Johnstone.  Stone Spaces.  Cambridge Univ. Press, 1986.
  * [15] G. Max Kelly.  A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on.  Bull. Austral. Math. Soc., 22:1–83, 1980.
  * [16] Clemens Kupke, Alexander Kurz, and Yde Venema.  Stone coalgebras.  Theoret. Comput. Sci., 327(1–2):109–132, 2004.
  * [17] Michael Makkai and Robert Paré.  Accessible Categories: the Foundation of Categorical Model Theory, volume 104 of Contemporary Math. Amer. Math. Soc., Providence, RI, 1989.
  * [18] Ernest Michael.  Topologies on spaces of subsets.  Trans. Amer. Math. Soc., 71:152–182, 1951.
  * [19] Dimitrie Pompeiu.  Sur la continuité des fonctions de variables complexes.  Annales de la Faculté des Sciences de la Université de Toulouse pour les Sciences Mathématiques et les Sciences Physiques, 2ième Série, 7(3):265–315, 1905.
  * [20] Luis Ribes and Pavel Zalesskii.  Profinite Groups, volume 40 of Ergebnisse der Mathematik und ihrer Grenzgebiete.  Springer, 2nd edition, 2010.
  * [21] Martin Rößiger.  Coalgebras and modal logic.  In Horst Reichel, editor, Proc. Coalgebraic Methods in Computer Science (CMCS 2000), volume 33 of Electron. Notes Theor. Comput. Sci., pages 294–315. Elsevier, 2000.
  * [22] Věra Trnková, Jiří Adámek, Václav Koubek, and Jan Reiterman.  Free algebras, input processes and free monads.  Comment. Math. Univ. Carolin., 16:339–351, 1975.
  * [23] Franck van Breugel.  De Bakker-Zucker processes revisited.  Inform. and Comput., 188(1):68–76, 2004.
  * [24] Franck van Breugel, Camillo Costantini, and Stephen Watson.  Isometries between a metric space and its hyperspace, function space, and space of measures.  Topology Appl., 137(1-3):51–57, 2004.  IV Iberoamerican Conference on Topology and its Applications.  doi:10.1016/S0166-8641(03)00198-6.
  * [25] Leopold Vietoris.  Bereiche zweiter Ordnung.  Monatsh. Math. Phys., 32(1):258–280, 1922.
  * [26] James Worrell.  On the final sequence of a finitary set functor.  Theoret. Comput. Sci., 338:184–199, 2005.
  * [27] Phillip Zenor.  On the completeness of the space of compact subsets.  Proc. Amer. Math. Soc., 26(1):190–192, 1970.

##  Appendix B Cofree Comonads

A closely related topic to terminal coalgebras are cofree comonads. Given an
endofunctor $F$ on a category $\mathscr{A}$, a comonad $F_{\sharp}$ together
with a natural transformation $\varepsilon\colon F_{\sharp}\to F$ is _cofree_
provided that for every comonad $C$ and every natural transformation
$\varphi\colon F_{\sharp}\to F$, there is a unique comonad morphism
$\overline{\varphi}\colon C\to F_{\sharp}$ for which the triangle below
commutes:

${C}$${F_{\sharp}}$${F}$$\scriptstyle{\varphi}$$\scriptstyle{\varepsilon}$$\scriptstyle{\overline{\varphi}}$

######  Proposition B.1 (Dual to Barr [8]).

An endofunctor $F$ on a cocomplete category generates cofree comonads iff all
cofree coalgebras exist, in other words,
$U_{F}\colon\mathop{\mathsf{Coalg}}F\to\mathscr{A}$ has a right adjoint.

######  Corollary B.2.

Let $\mathscr{A}$ be a cocomplete category with finite products. An
endofunctor $F$ generates a cofree comonad iff for every object $Y$ of
$\mathscr{A}$ a terminal coalgebra for $F(-)\times Y$ exists. Moreover, the
cofree comonad $F_{\sharp}$ is given by $F_{\sharp}Y=\nu(F(-)\times Y).$

#### Cofree Comonad Construction

From the above the following construction of $F_{\sharp}$ was derived [22].
Let $F$ be an endofunctor on a complete category $\mathscr{A}$. Define an
ordinal-indexed chain $F_{i}$ ($i\in\mathsf{Ord}^{\mathsf{op}}$) of
endofunctors and connection natural transformations $f_{i,j}\colon F_{i}\to
F_{j}$ ($i\geq j$) by transfinite recursion: put

$\begin{array}[]{l@{\,}l@{\qquad}l}F_{0}&=\mathsf{Id},\\\
F_{j+1}&=FF_{j}\times\mathsf{Id}&\text{for all ordinals $j$,}\\\
F_{j}&=\lim_{i<j}F_{i}&\text{for all limit ordinals $j$, and}\\\\[10.0pt]
\lx@intercol\text{$f_{1,0}\colon F_{1}=F\times\mathsf{Id}\to\mathsf{Id}$ is
the projection,}\hfil\lx@intercol\\\ \lx@intercol
f_{k+1,j+1}=Ff_{k,j}\times\operatorname{\mathsf{id}}\colon
FF_{k}\times\mathsf{Id}\to FF_{j}\times\mathsf{Id},\hfil\lx@intercol\\\
\lx@intercol\text{$f_{j,i}\colon F_{j}\to F_{i}$ ($j>i$) is the limit cone for
every limit ordinal $j$.}\hfil\lx@intercol\end{array}$

If $F$ preserves the limit $F_{\omega}X=\lim_{n<\omega}F_{n}X$ for every
object $X$, then it generates a cofree comonad carried by $F_{\omega}$, and we
say that the cofree comonad is _obtained in $\omega$ steps._

Analogously, if $F$ preserves the limit
$F_{\omega+\omega}X=\lim_{n<\omega}F_{\omega+n}X$ for every object $X$, then
the cofree comonad is carried by $F_{\sharp}=F_{\omega+\omega}$, and we say
that it is _obtained in $\omega+\omega$ steps_.

######  Corollary B.3.

Every Kripke polynomial functor has a cofree comonad obtained in
$\omega+\omega$ steps.

This follows from Theorem 3.2 and B.2: if $F$ is a Kripke polynomial functor,
then so is $F(-)\times Y$ for every set $Y$.

######  Example B.4.

  1. 1.

For the set functor $FX=X+1$ a cofree comonad $F_{\sharp}$ is obtained in
$\omega$ steps:

$F_{\sharp}X=X^{*}+X^{\omega}$

is the set of all finite and infinite words on the set $X$.

  2. 2.

For a polynomial set functor $H_{\Sigma}$, a cofree comonad is obtained in
$\omega$ steps: $F_{\sharp}Y$ is the set of all $\Sigma_{Y}$-trees where
$\Sigma_{Y}$ is the signature obtained from $\Sigma$ by adding a new constant
symbol for every $y\in Y$.

######  Corollary B.5.

The restriction of a $T_{2}$ Vietoris polynomial functor to $\mathsf{Haus}$
generates a cofree comonad obtained in $\omega$ steps.

Indeed, if $F$ is a $T_{2}$ Vietoris polynomial functor, then so is the
functor $F(-)\times A$ for every Hausdorff space $A$. Now apply B.2 and
Theorem 4.8.

######  Corollary B.6.

Every Hausdorff polynomial functor $F$ on $\mathsf{Met}$, $\mathsf{CMS}$ or
$\mathsf{UMet}$ generates a cofree comonad obtained in $\omega+\omega$ steps.

The same argument works, but we use Theorem 5.5.

##  Appendix C Omitted Proofs and Details

### Details for 3

Consider the functor $G$ assigning to a set $X$ the set of _nonempty_ finite
subsets of $X$. We verify that $G$ is not naturally isomorphic to a Kripke
polynomial functor. This follows from the result below and the observation
that $|G\\{\emptyset\\}|=1$.

######  Proposition C.1.

Let $F$ be a Kripke polynomial functor $F$. Suppose that $|FX|=1$ for some
nonempty set $X$. Then $F$ is naturally isomorphic to the constant functor
with value $1$.

######  Proof C.2.

With each Kripke polynomial functor $F$ we associate a number
$n(F)\in\\{0,1,2,3\\}$. The inductive definition of $n(F)$ follows the grammar
in 1. Following the definition, we show four points by induction on $F$:

  1. 1.

If $n(F)=0$, then $FX=\emptyset$ for all sets $X$.

  2. 2.

If $n(F)=1$, then $|FX|=1$ for all sets $X$.

  3. 3.

If $n(F)=2$, then $FX$ is finite for all finite sets $X$, $FX$ is infinite for
all infinite sets $X$; and for all sets $X$ with $|X|\geq 1$, $|FX|>1$.

  4. 4.

If $n(F)=3$, then $FX$ is infinite for all sets $X$.

Here is our definition:

$\displaystyle n(\mathscr{P}_{\mathsf{f}})$ $\displaystyle=2$ $\displaystyle
n(\mathsf{Id})$ $\displaystyle=2$ $\displaystyle n(\prod_{i\in I}F_{i})$
$\displaystyle=\begin{cases}0&\text{if for some $i\in I$, $n(F_{i})=0$}\\\
1&\text{if $n(F_{i})=1$ for all $i\in I$ (including the case
$I=\emptyset$)}\\\ 2&\parbox[t]{284.52756pt}{if $n(F_{i})\in\\{1,2\\}$ for all
$i$, and $n(F_{i})=1$ for all but finitely many $i$ and $n(F_{i})=2$ for some
$i\in I$,}\\\ 3&\parbox[t]{284.52756pt}{if $n(F_{i})\in\\{1,2,3\\}$ for all
$i$, and either $n(F_{i})=2$ for infinitely many $i$, or there is some $i\in
I$ with $n(F_{i})=3$}\end{cases}$ $\displaystyle n(\coprod_{i\in I}F_{i})$
$\displaystyle=\begin{cases}0&\text{if $n(F_{i})=0$ for all $i\in I$
(including the case $I=\emptyset$)}\\\ 1&\text{if $I$ is a singleton set
$\\{i\\}$ and $n(F_{i})=1$}\\\
2&\parbox[t]{284.52756pt}{$n(F_{i})\in\\{0,1,2\\}$ for all $i\in I$, and
$n(F_{i})=0$ for all but finitely many $i$; and either $n(F_{i})=1$ for two
distinct $i\neq j\in I$, or $n(F_{i})=2$ for some $i\in I$}\\\ 3&\text{if for
some $i\in I$, $n(F_{i})=3$, or if for infinitely many $i$,
$n(F_{i})\in\\{1,2\\}$}\end{cases}$ $\displaystyle n(FG)$
$\displaystyle=\begin{cases}0&\text{if $n(F)=0$}\\\ 1&\text{if either
$n(F)=1$; or $n(F)=2$, $n(G)=1$, and $|F2|=1$}\\\ 2&\parbox[t]{284.52756pt}{if
either $n(F)=2$ and $n(G)=2$; or $n(F)=2$, $n(G)=1$, and $|F2|\neq 1$}\\\
3&\text{if either $n(F)=3$, or $n(F)\geq 2$ and $n(G)=3$}\\\ \end{cases}$

We now turn to the assertions stated before the definition of $n(F)$. For
$\mathscr{P}_{\mathsf{f}}$ and $\mathsf{Id}$, our assertions are clear. For a
functor $\prod_{i\in I}F_{i}$, the verifications use the induction hypothesis
and the following facts: the product of any family of sets is empty if any
factor in the product is empty; the product of any family of singleton sets is
a singleton set; an arbitrary product is finite and non-empty if all but
finitely many factors are singletons and the remaining factors are finite; a
product of non-empty sets is infinite if either there are infinitely many
finite factors of size $\geq 2$, or if one of the factors is infinite.

The verifications for the coproduct and composition steps are similar.

We return to the proof our our result. If $|F(X)|=1$ for some $X\neq 1$, then
$n(F)$ cannot be $0$, $2$ or $3$. Thus $n(F)=1$, and our result follows.

### Details for 4.14

The terminal coalgebra for $\mathscr{V}$ itself was identified by Abramsky
[1]. By what we have shown, it is $V_{\omega}=\lim\mathscr{V}^{n}1$. An easy
induction on $n$ shows that $\mathscr{V}^{n}1$ is
$\mathscr{P}_{\mathsf{f}}^{n}1$ with the discrete topology; the key point is
that each set $\mathscr{P}_{\mathsf{f}}^{n}1$ is finite. We know that
$V_{\omega}$ is thus the set $T$ in (6) of all compactly branching, strongly
extensional trees. The topology was described in section 2.2: it has as a base
the sets $\partial_{n}^{-1}(U)$ as $U$ ranges over the subsets of
$\mathscr{P}_{\mathsf{f}}^{n}1$. By Theorem 4.8, $\nu F$ is a Stone space.

We also can explicate the terminology of ‘compactly branching’ (25). We have
formulated this using convergence in a formal sense, and here we connect this
to a metric. The collection $\mathcal{C}$ of all strongly extensional trees is
a proper class. Setting this aside, it has a pseudo-metric $d$ given by

$d(s,t)=\inf\\{2^{-n}:\partial_{n}(t)=\partial_{n}(u)\\}.$

This pseudo-metric has been defined by Worrell [26].

######  Proposition C.3.

The relation $\approx$ on the class $\mathcal{T}$ of all trees has
$2^{\aleph_{0}}$ equivalence classes, and $d$ is a metric on
$\mathcal{T}/{\approx}$.

######  Proof C.4.

We have a well-defined injective map

$b\colon\mathcal{T}/{\approx}\to V_{\omega}$

assigning to an equivalence class of a tree $t$ the sequence
$(\partial_{n}t)_{n<\omega}$. Hence, $|\mathcal{T}/{\approx}|\leq
2^{\aleph_{0}}.$ We check the reverse inequality. For every set
$A\subseteq\mathds{N}\setminus\\{0\\}$, let $t_{A}$ be an infinite path with
additional leaves of depth $n$ for each $n\in A$. Then one can check that for
$A\neq B$, $t_{A}$ and $t_{B}$ are not Barr equivalent. Hence
$|\mathcal{T}/{\approx}|\geq 2^{\aleph_{0}}$ since the set
$\mathds{N}\setminus\\{0\\}$ has $2^{\aleph_{0}}$ subsets.

The general construction of a metric space from a pseudo-metric space takes
equivalence classes of points of distance $0$. In our setting, points (trees)
have distance $0$ in $\mathcal{T}$ exactly when they are Barr-equivalent.

######  Theorem C.5.

The metric space $(\mathcal{T}/{\approx},d)$ is compact.

######  Proof C.6.

  1. 1.

The space $\mathcal{T}/{\approx}$ is totally bounded: for every
$\varepsilon>0$, there is a finite cover by $\varepsilon$-balls. Indeed,
choose $n$ with $2^{-n}<\varepsilon$ and take the (finite) set $A$ of all
extensional trees of height at most $n$. Then every tree $t$ satisfies
$\partial_{n}t\in A$ and $d(t,\partial_{n}t)\leq 2^{-n}<\varepsilon$.

  2. 2.

We recall that a metric space is compact iff it is totally bounded and
complete. Towards showing that $\mathcal{T}/{\approx}$ is complete, let
$(t_{n})$ be a Cauchy sequence. For each fixed $k$, the sequence
$(\partial_{k}(t_{n}))$ is eventually constant. Let $x_{k}\in V_{k}$ be such
that for all but finitely many $n$, $(\partial_{k}(t_{n}))=x_{k}$. We may
choose the sequence $(x_{k})$ so that it is compatible:
$\partial_{k}(x_{k+1})=x_{k}$. Then A.10 provides us with a single tree $t$
such that $\partial_{k}(t)=x_{k}$ for all $k$. This tree $t$ is a limit of the
original sequence $(t_{n})$.

######  Corollary C.7.

A set $M\subseteq\mathcal{T}$ is compact iff for every sequence $(t_{n})$ from
$M$, if $\lim_{n}t_{n}=s$, there exists $t\in M$ such that $t\approx s$.

######  Proof C.8.

The quotient map $q\colon\mathcal{T}\to\mathcal{T}/{\approx}$ is continuous
and closed, and thus $M$ is compact iff its image $q[M]$ is. The latter holds
iff $q[M]$ is a closed set. This is what the condition in our corollary
states.

It is a standard fact that for metric spaces, compactness and sequential
compactness are equivalent. Thus, for all trees $t$ and all nodes $x$ of $t$,
$\\{t_{y}:\text{$y$ a child of $x$ in $t$}\\}$ is compact iff it is
sequentially compact. This explains why we were able to define the compactly
branching trees using sequential compactness.

### Example: Terminal Coalgebra for a Hausdorff Polynomial Functor

Here we present a description of a terminal coalgebra for a Hausdorff
polynomial functor related to the type functor for finitely branching labelled
transition systems (3.1). First note that the terminal coalgebra for the
Kripke polynomial set functor given by
$FX=\mathscr{P}_{\mathsf{f}}(\Sigma\times X)$ has a description which is
analogous to the one for $\mathscr{P}_{\mathsf{f}}$. We work, for the label
alphabet $\Sigma$, with trees having edges labelled in $\Sigma$, and identify
again isomorphic trees. The concept of extensionality is defined w.r.t.
isomorphism of labelled trees, and tree bisimulation also takes into account
the labelling of egdes:

######  Definition C.9.

A _tree bisimulation_ between two $\Sigma$-labelled trees $t$ and $u$ is a
relation between the nodes of $t$ and the nodes of $u$ with the following
properties:

  1. 1.

whenever $x$ and $y$ are related: for every $a\in\Sigma$ (a) every
$a$-child222An $a$-child of a node $x$ is a child node connected to $x$ by an
edge labelled by $a$. of $x$ is related to some $a$-child of $y$, and (b)
every $a$-child of $y$ is related to some $a$-child of $x$;

  2. 2.

the roots of $t$ and $u$ are related; the roots are not related to other
nodes; and

  3. 3.

whenever two nodes are related, their parents are also related.

The notions of tree bisimilarity and strong extensionality are now defined
completely analogously as for unlabelled trees using the above notion of tree
bisimulation. The terminal coalgebra for
$\mathscr{P}_{\mathsf{f}}(\Sigma\times X)$ consists of all finitely branching
strongly extensional labelled trees, and the limit $V_{\omega}$ consists of
all compactly branching strongly extensional trees, with the limit cone given
by $\partial_{n}$ $(n<\omega)$.

The proof is completely analogous to that in Appendix A.

######  Example C.10.

Let $\Sigma=\\{0,1\\}$ be the metric space with $d(0,1)=\delta<1$. We describe
the terminal coalgebra of $F(X)=\mathcal{H}(\Sigma\times X)$. The elements of
$\nu F$ are finitely branching strongly extensional trees $t$ whose edges are
labelled in $\Sigma$. We denote by $|t|$ the underlying non-labelled tree. The
metric is the given for $t\neq s$ by

$d(t,s)=\biggl{\\{}\begin{array}[]{ll}\delta&\mbox{if $|t|=|s|$,}\\\
\infty&\mbox{otherwise.}\end{array}\biggr{.}$ (8)

The coalgebra structure assigns to a tree $t$ with maximum subtrees
$t_{1},\ldots,t_{n}$ the set of pairs
$\\{(\sigma_{1},t_{1}),\ldots,(\sigma_{n},t_{n})\\}$, where $\sigma_{i}$ is
the label of the corresponding edge from the root.

Here is the proof. We denote by $V_{i}$ the $i^{th}$ entry in the terminal-
coalgebra chain for $F$ (in $\mathsf{Met}$) and by $\overline{V}_{i}$ the
corresponding entry in the terminal-coalgebra chain for
$\mathscr{P}_{\mathsf{f}}(\Sigma\times X)$ (in $\mathsf{Set}$). Analogously,
we denote by $v_{i,j}\colon V_{i}\to V_{j}$ and
$\overline{v}_{i,j}\colon\overline{V}_{i}\to\overline{V}_{j}$ the connecting
maps for all $j\leq i<\omega+\omega$. (Thus, $v_{\omega+1},\omega$ is $m$ from
(2) in the Introduction.) We prove by transfinite induction on $i$ that the
$V_{i}$ can be chosen to have the underlying set $\overline{V}_{i}$ with the
metric in (8), and that the connecting morphisms $v_{ij}$ are carried by the
corresponding functions $\overline{v}_{ij}$.

  1. 1.

For $i=0$, we can choose $\overline{V}_{0}=\\{t_{r}\\}$, the root-only tree as
a metric space, and $V_{0}=\\{t_{r}\\}$.

  2. 2.

The isolated step. Since all positive distances in $\Sigma\times V_{i}$ are
$\delta$ or $\infty$, every compact subset of this space is finite. Thus the
underlying set of the space $V_{i+1}$ is
$\mathscr{P}_{\mathsf{f}}(\Sigma\times\overline{V}_{i})=\overline{V}_{i+1}$.
Given distinct trees $t$ and $s$, where
$t=\\{(\tau_{i},t_{i}):i=1,\ldots,n\\}$ and
$s=\\{(\sigma_{i},s_{i}):i=1,\ldots,m\\}$ in $\mathcal{H}(\Sigma\times
V_{i})$, we prove that their distance is $d(t,s)$ as given above. This is
clear if $n=0$ or $m=0$. In that case, $|t|$ and $|s|$ are not bisimilar, and
$d(t,s)=\infty$.

Let $n>0$ and $m>0$. Then $d(s,t)$ is the Hausdorff distance of the given sets
in $\mathcal{H}(\Sigma\times V_{i})$. Suppose that the corresponding maximum
distance between a maximum branch of one tree to the other tree is obtained at
$t_{1}$, so that $\bar{d}(t,s)=d((\tau_{1},t_{1}),s)$. We know that distances
in $\Sigma\times V_{i}$ are $0$, $\delta$, or $\infty$. It follows that
$\mathcal{H}(\Sigma\times V_{i})$ has this property also. We thus have two
cases: $\bar{d}(t,s)=\delta$, or $\bar{d}(t,s)=\infty$.

    1. (a)

Case $\bar{d}(t,s)=\delta$. Since $i=1$ maximizes the distance of a branch of
$t$ to $s$, for every $i=1,\ldots,n$ there exists $j=1,\ldots,m$ such that
$d(t_{i},s_{j})\leq\delta$. Conversely, for every $j$ there exists $i$ such
that $d(t_{i},s_{j})\leq\delta$. Put

$T=\\{(i,j):\text{$i\leq n$, $j\leq m$ and $d(z_{i},s_{j})\leq\delta$}\\}.$

By the induction hypothesis, for each $(i,j)\in T$ there exists a tree
bisimulation $R_{i,j}\subseteq|t_{i}|\times|s_{j}|$. Then the following is a
tree bisimulation $R\subseteq|t|\times|s|$:

$R=\\{(x_{r},y_{r})\\}\cup\bigcup_{(i,j)\in T}R_{i,j}.$

Therefore the above distance formula agrees: $d(t,s)=\delta=\bar{d}(t,s)$.

    2. (b)

Case $\bar{d}(t,s)=\infty$. Since the minimum distance of $(\tau_{1},t_{1})$
to $(\sigma_{j},s_{j})$ is $\infty$, we conclude from
$d(\tau_{i},\sigma_{j})\leq\delta<\infty$ that $d(t_{1},s_{j})=\infty$ for
$j=1,\ldots,m$. Our task is to prove that $|t|$ is not tree-bisimilar to
$|s|$. Assuming the contrary, $|t_{1}|$ is tree-bisimilar to $|s_{j}|$ for
some $j$. By the induction hypothesis, this contradicts
$d(t_{1},s_{j})=\infty$.

  3. 3.

The limit step. Since the chain $\overline{V}_{i}$ converges in
$\omega+\omega$ steps, we need only consider the cases $i=\omega$ and
$i=\omega+\omega$.

For $i=\omega$, note that the forgetful functor $\mathsf{Met}\to\mathsf{Set}$
preserves limits. Thus we may assume that the underling set of
$V_{\omega}=\lim_{m<\omega}V_{n}$ is
$\lim_{m<\omega}\overline{V}_{n}=\overline{V}_{\omega}$. This is the set of
all compactly branching strongly extensional, $\Sigma$-edge-labelled trees
(cf. 3.5). The limit cone is given by

$\ell_{\omega,n}=\partial_{n}\colon V_{\omega}\to V_{n}\quad(n<\omega).$

The distance between trees $t\neq s$ is therefore
$d(t,s)=\sup_{n<\omega}d_{n}(\partial_{n}t,\partial_{n}s).$ Whenever the trees
$|t|$ and $|s|$ are tree-bisimilar, $|\partial_{n}(t)|$ and
$|\partial_{n}(s)|$ are also tree-bisimilar. Thus, the supremum above is
$\delta$, as required. If $|t|$ and $|s|$ are not tree-bisimilar, then there
exists some $n<\omega$ such that $|\partial_{n}(t)|$ and $|\partial_{n}(s)|$
are not tree-bisimilar. In this case, $d(t,s)=\infty$, as required.

Let $i=\omega+\omega$. We know that
$\overline{v}_{\omega+1}\colon\overline{V}_{\omega+1}\to\overline{V}_{\omega}$
represents the subset of all trees that are finitely branching at the root
(cf. the proof of Theorem A.14.2). The connecting map
$\bar{v}_{\omega+1,\omega}\colon\overline{V}_{\omega+1}\to\overline{V}_{\omega}$
preserves distances because for all $n$ we have $\partial_{n}\cdot
v_{\omega+1,\omega}=F\partial_{n}$. (For this, use
$F\partial_{n}=Fv_{\omega,n}=v_{\omega+1,n+1}=v_{\omega,n}\cdot
v_{\omega+1,\omega}$.) Thus $v_{\omega+1,\omega}$ represents the metric
subspace of $V_{\omega}$ on trees which are finitely branching at the root.
The functor $F$ preserves isometric embeddings. Hence
$v_{\omega+2,\omega}=Fv_{\omega+1,\omega,\omega}\cdot v_{\omega+1,\omega}$ is
an isometric embedding. Analogously, $v_{\omega+n,\omega}\colon
V_{\omega+n}\to V_{\omega}$ represents the metric subspace of all trees
finitely branching up to level $n$. The $\omega$-chain $V_{\omega+n}$
($n<\omega$) consists of isometric embeddings. Thus the limit
$V_{\omega+\omega}=\lim_{n}V_{\omega+n}$ is the metric subspace of
$V_{\omega}$ on the intersection of the subspaces $V_{\omega+n}$. This is
precisely the metric space described at the beginning of this discussion.