MFPS 2013

Coinductive Predicates andFinal Sequences in a Fibration
Ichiro Hasuo

Kenta Cho

Toshiki Kataoka

Department of Computer Science, University of Tokyo, Japan

Bart Jacobs
ICIS, Radboud University Nijmegen, The Netherlands

Abstract
Coinductive predicates express persisting “safety” specifications of transition systems. Previous observations by Hermida and Jacobs identify coinductive predicates as suitable final coalgebras in a fibration—acategorical abstraction of predicate logic. In this paper we follow the spirit of a seminal work by Worrell andstudy final sequences in a fibration. Our main contribution is to identify some categorical “size restriction”
axioms that guarantee stabilization of final sequences after ω steps. In its course we develop a relevant
categorical infrastructure that relates fibrations and locally presentable categories, a combination that does
not seem to be studied a lot. The genericity of our fibrational framework can be exploited for: binary
relations (i.e. the logic of “binary predicates”) for which a coinductive predicate is bisimilarity; constructive
logics (where interests are growing in coinductive predicates); and logics for name-passing processes.
Keywords: coalgebra; (co)recursive predicate; modal logic; fibration; locally presentable category

1Introduction

Coinductive predicates postulate properties of state-based dynamic systems thatpersist after a succession of transitions. In computer science, safety properties ofnonterminating, reactive systems are examples of paramount importance. This has
led to an extensive study of specification languages in the form of fixed point logics
and model-checking algorithms.
In this paper we follow [26,27] (further extended in [5,20]; see also [32, Chap. 6])
and take a categorical view on coinductive predicates. Here coalgebras represent
transition systems; a fibration is a “predicate logic”; and a coinductive predicate is
identified as a suitable coalgebra in a fibration. Our contribution is the study of
final sequences—an iterative construction of final coalgebras that is studied notablyin [2, 44]—in such a fibrational setting.
Coalgebras have been successfully used as a categorical abstraction of transition
systems (see e.g. [32,41]): by varying base categories and functors, coalgebras bring
general results that work for a variety of systems at once. Fixed point logics (orThis paper is electronically published inElectronic Notes in Theoretical Computer Science
URL: www.elsevier.nl/locate/entcs

Hasuo, Cho, Kataoka, Jacobs

modal logics in general), too, have been actively studied coalgebraically: coalgebraic
modal logic is a prolific research field (see [12]); their base category is typically Sets
but works like [34] go beyond and use presheaf categories for processes in namepassing calculi; and literature including [11, 13, 43] studies coalgebraic fixed point
logics.
Unlike most of these works, we follow [26, 27] and parametrize the underlying“predicate logic” too with the categorical notion of fibration. The conventional
Predsetting of classical logic is represented by the fibration ↓ (see Appendix A.3 for
Sets
an introduction to fibrations).
However there are various other “logics”
P
Pred
Rel
↓p
↓
↓
fibrationmodeled as fibrations, and hence the fibraSets
Sets
Ctional language provides a uniform treatment
coalgebra
invariant bisimulation
final
coindutiveof these different settings. An example is bibisimilarity
coalgebra
predicatenary relations (instead of unary predicates)
Relthat form a fibration ↓ (see Appendix A.3). In this case coinductive predicatesSets
are bisimilarity (see the table, and Example 5.12 later).
Another example is predicates in constructive logics. They are modeled by thesubobject fibration of a topos. In fact, coinductive predicates in constructive logics
are an emerging research topic: coinduction is supported in the theorem prover
Coq (based on the constructive calculus of constructions), see e.g. [6]; and, working
in Coq, some interesting differences between classically equivalent (co)inductive
predicates have been studied e.g. in [39].
Yet another example is modal logics for processes in various name-passing calculi.
They are best modeled by the subobject fibration of a suitable (pre)sheaf category
like SetsI and SetsF .
1.1

Coinductive Predicates and Their Construction, Conventionally

In order to illustrate our technical contributions (§3) we first present a special case,with classical logic and Kripke models. We first introduce syntax.
Definition 1.1 (Rudimentary logic Rν) This fragment of the µ-calculus allows
only one greatest fixed-point operator at the outermost position.
Rνu ∋ α ::= a | a | 2u | 3u | α ∧ α | α ∨ α ;Rν ∋ β ::= νu. α .

(1)Here a belongs to the set AP of atomic propositions; a stands for the negation of a;and u is the only fixed-point variable (with possibly multiple occurrences).
An Rν-formula can be thought of as a recursive definition of a coinductive predicate. Later we will model such a “definition” categorically as a predicate lifting.
A specification expressible in Rν is (may-) deadlock freedom (“there is an infinitepath”). It is expressed by νu. 3u and is our recurring example.
An Rν-formula is interpreted in Kripke models. Let c = (X, →, V ) be a Kripke
model, where X is a state space, → ⊆ X × X is a transition relation and V : X →P(AP) is a valuation. The conventional interpretation [νu.α]c of Rν-formulas in the2

Hasuo, Cho, Kataoka, Jacobs

Kripke model c is given as follows (see e.g. [9]). Firstly, we interpret α ∈ Rνu as afunction [α]c : PX → PX. Concretely:[a]c (P ) = {x | a ∈ V (x)}[a]c (P ) = {x | a 6∈ V (x)}[2u]c (P ) = {x | ∀y ∈ X. (x → y implies y ∈ P )} [3u]c (P ) = {x | ∃y ∈ X. (x → y and y ∈ P )}[α ∧ α′ ]c (P ) = [α]P ∩ [α′ ]P[α ∨ α′ ]c (P ) = [α]P ∪ [α′ ]PThis function [α]c is easily seen to be monotone, since u occurs only positively in
α. Finally we define [νu.α]c ⊆ X to be the greatest fixed point of the monotonefunction [α]c : PX → PX.
The Knaster-Tarski theorem guarantees the existence of such a greatest fixed
point [νu.α]c in a complete lattice PX. However its proof is highly nonconstructive.
In contrast, a well-known construction [14] by Cousot and Cousot computes [νu.α]c
as the limit of the following descending chain (see also [9]). Here ⊤ denotes thesubset X ⊆ X.
⊤ ≥ [α]c ⊤ ≥ [α]2c ⊤ ≥ · · ·(2)
V
An issue now is the length of the chain. If [α]c preserves limitsc1(which is the case with α ≡ 2u), clearly ω steps are enough and yields···Vii∈ω ([α]c ⊤) as the greatest fixed point. This is not the case withα ≡ 3u. Indeed, for the Kripke model c1 on the right [νu. 3u]c1 6=Viii∈ω ([3u]c1 ⊤): there is no infinite path from the root; but it satisfies [3u]c1 ⊤(‘there is a path of length ≥ i’) for each i.
Yet the chain (2) eventually stabilizes, bounded by the size of the poset PX.
Therefore the calculation of [νu.α]c is, in general, via transfinite induction. This iswhat we call a state space bound for (2).
Besides a state space bound, another (possibly better and seemingly less known)bound can be obtained from a behavioral view. One realizes that not only the sizeof the state space X but also the branching degree can be used to bound the lengthof the chain (2). For example, a result similar to [24, Thm. 2.1] states that the
chain stabilizes after ω steps if the Kripke model c is finitely branching. This holds
however large the state space X is; and also for any Rν-formula νu.α. Notice thatthe model c1 (depicted above) is not finitely branching.
1.2

Final Sequences in a Fibration

This paper is about putting the observations in §1.1 in general categorical terms.
Our starting observation is that the chain (2) resembles a final sequence, a classic
construction of a final coalgebra.
In the theory of coalgebra a final F -coalgebra is of prominent importance since
it is a fully abstract domain with respect to the F -behavioral equivalence. Therefore
a natural question is if a final F -coalgebra exists; the well-known Lambek lemmaprohibits e.g. a final P-coalgebra. What matters is the size of F : when it is suitablybounded, it is known that a final coalgebra can be constructed via the following final
F -sequence.
i−1
i
(3)
1 ! F 1 F ! · · · F ! F i1 F ! · · ·Here 1 is a final object in C, and ! is the unique arrow. In particular, if F isfinitary, a final coalgebra arises as a suitable quotient of the ω-limit of the final
3

Hasuo, Cho, Kataoka, Jacobs

sequence (3). This construction in Sets is worked out in [44]; it is further extended
to locally presentable categories (those are categories suited for speaking of “size”)
with additional assumptions in [2].
Turning back to coinductive predicates, indeed, the fibrational view [26,27] identifies coinductive predicates as final coalgebras in a fibration. This leads us to
scrutinize final sequences in a fibration. Our main result (Thm. 3.7) is a categorical generalization of the behavioral ω-bound (§1.1)—more precisely we axiomatize
categorical “size restrictions” for that bound to hold.
The conditions are formulated in the language of locally presentable categories(see e.g. [4]; also Appendix A.2); and the combination of fibrations and locallypresentable categories does not seem to have been studied a lot (an exception is [37,§5.3]). We therefore develop a relevant categorical infrastructure (§5.1). Our results
there include a sufficient condition for the total category Sub(C) of a subobject
fibration to be locally (finitely) presentable, and the same for a family fibration
Fam(Ω) too. Via these results, in §5.2 we list some concrete examples of fibrations
to which our results in §3 on the behavioral bounds apply. They include:

Pred
↓
Sets

Sub(C)
Rel↓↓(for bisimulation and bisimilarity);
for C that is(classical logic);
Sets
C

locally finitely presentable and locally Cartesian closed (a topos is a special case);
Fam(Ω)↓
andfor a well-founded algebraic lattice Ω.
Sets

1.3

Summary and Future WorkTo summarize, our contributions are: 1) combination of the mathematical observations in [26,27] and [32, Chap. 6] for a general formulation of coinductive predicates;
2) categorical behavioral bounds for final sequences that approximate coinductive
predicates; and 3) a categorical infrastructure that relates fibrations and locallypresentable categories.
While our focus is on coinductive predicates, inductive ones are just as importantin system verification; so are their combinations. Such mixture of induction andcoinduction is studied fibrationally in [25], but over mixed inductive and coinductive
data types, and not over a coalgebra. We have obtained some preliminary fibrational
observations in this direction.
Search for useful coinduction proof principles is an active research topic (seee.g. [8, 28]). We are interested in the questions of whether these principles are
sound in a general fibrational setting, and what novel proof principles a fibrationalview can lead to.
Coalgebraic modal logic is more and more often introduced based on a Stone-likeduality (see e.g. [34]). Fibrational presentation of such dualities will combine thebenefits of duality-based modal logics and the current results. We are also interested
in the relationship to coalgebraic infinite traces [10, 30].
Kozen’s metric coinduction [35] is a construction of coinductive predicates by
the Banach fixed point theorem and is an alternative to the current paper’s ordertheoretic one. Its fibrational formulation is an interesting future topic.
4Hasuo, Cho, Kataoka, Jacobs

Practical applications of our categorical behavioral bounds shall be pursued, too.
Our results’ precursor—the bounds for the final sequences in Sets [2,44]—have beenused to bound execution of some algorithms e.g. for state minimization [3, 15, 16].
We aim at similar use. Finally, games are an extremely useful tool in fixed point
logics (also in their coalgebraic generalization, see [11,13,43]; also [36]). We plan toinvestigate the use of games in the current (even more general) fibrational setting.
Organization of the Paper
In §2 we identify coinductive predicates as final coalgebras in a fibration, following
the ideas of [26, 27, 32]. The main technical results are in §3, where we axiomatize
size restrictions on fibrations and functors for a final sequence to stabilize after ω
steps. These results are reorganized in §4 as a fibration of invariants. §5 is devoted
to examples: first we develop a necessary categorical infrastructure then we discuss
concrete examples.
In Appendix A we present minimal introductions to the theories of coalgebras,
locally presentable categories and fibrations—the three topics that our technicaldevelopments rely on. Most proofs are deferred to Appendix B.

2

Coinductive Predicates as Final Coalgebras

In this section we follow the ideas in [26, 27, 32] and characterize coinductive predicates in various settings (for different behavior types, and in various underlying
logics) in the language of fibration. An introduction to fibration is e.g. in [29]; seealso Appendix A.3. In this paper for simplicity we focus on poset fibrations. It
should however not be hard to move to general fibrations.
Definition 2.1 (Fibration) We refer to poset fibrations (where each fiber is aposet rather than a category) simply as fibrations.
P
Definition 2.2 (Predicate lifting) Let ↓p be a fibration and
C

P
p

ϕ

P
p

(4)

F be an endofunctor on C. A predicate lifting of F along p is aC
CFfunctor ϕ : P → P such that (ϕ, F ) is an endomap offibrations. This means: that the diagram on the right commutes; and that ϕpreserves Cartesian arrows, that is, ϕ(f ∗ Q) = (F f )∗ (ϕQ). See below.
P

f ∗Q

fQ

ϕ(f ∗ Q)Q

(F f )∗ (ϕQ)

p

C

X

f

Y

FX

Pred

ϕ(f Q)ϕQ

F f (ϕQ)
Ff

(5)

FY

In the prototype example ↓ , the above definition coincides (see [32]) withSets
the one used in coalgebraic modal logic (see e.g. [12])—presented as a (monotone)ϕnatural transformation 2( ) ⇒ 2F ( ) : Setsop → Sets.
We think of predicate liftings as (co)recursive definitions of coinductive predicates (see Example 2.4). On top of it, we identify coinductive predicates (andinvariants) as coalgebras in a fiber.
5

Hasuo, Cho, Kataoka, Jacobs

Definition 2.3 (Invariant, coinductive predicate) Let ϕ be a predicate liftingof F alongPc↓p ; and X →F X be a coalgebra in C. They together induce an
C
∗
ϕ

c

endofunctor (a monotone function) on the fiber PX , namely PX → PF X → PX ,where ϕ restricts to PX → PF X because of (4).
(i) A ϕ-invariant in c is a (c∗ ◦ ϕ)-coalgebra in PX , that is, an object P ∈ PX
such that P ≤ c∗ (ϕP ) in PX .
(ii) The ϕ-coinductive predicate in c is the final (c∗ ◦ ϕ)-coalgebra (if it exists). Its
carrier shall be denoted by JνϕKc . It is therefore the largest ϕ-invariant in c;
Lambek’s lemma yields that JνϕKc = (c∗ ◦ ϕ)(JνϕKc ).
Example 2.4 (Rν) The conventional interpretation [νu.α]c (described in §1.1) ofRν-formulas is a special case of Def. 2.3. Indeed, let us work in the fibration

Pred
↓ ,
Sets
c

and with the endofunctor FK = P(AP) × P( ) on Sets. An FK -coalgebra X →P(AP) × PX is precisely a Kripke model: c combines a valuation X → P(AP) andthe map X → PX that carries a state to the set of its successors. To each formulaα ∈ Rνu we associate a predicate lifting ϕα of FK . This is done inductively as
follows.
ϕa (U ⊆ X) = {V ∈ FK X | a ∈ π1 (V )} ⊆ FK X

ϕ2u (U ⊆ X) = {V | π2 (V ) ⊆ U } ⊆ FK X
ϕα∧α′ (U ⊆ X) = (ϕα U ∩ ϕα′ U ) ⊆ FK X

ϕa (U ⊆ X) = {V | a 6∈ π1 (V )} ⊆ FK X

ϕ3u (U ⊆ X) = {V | ∃x ∈ U. x ∈ π2 (V )} ⊆ FK X
ϕα∨α′ (U ⊆ X) = (ϕα U ∪ ϕα′ U ) ⊆ FK X
(6)

In the above, π1 and π2 denote the projections from FK X = P(AP) × PX. Then it
is easily seen by induction that Jνϕα Kc in Def. 2.3 coincides with the conventional
interpretation [νu.α]c described in §1.1.
In fact, the predicate liftings ϕα in (6) are the ones commonly used in coalgebraic
modal logic (where they are presented as natural transformations).
We point
out that the same definition of ϕα —they are written in the internal language of

Sub(C)↓
toposes—works for the subobject fibrationof any topos C. Therefore theCcategorical definition of coinductive predicates (Def. 2.3) allows us to interpret thelanguage Rν in constructive underlying logics. Suitable completeness of C ensuresthat a final (c∗ ◦ ϕ)-coalgebra in Def. 2.3 exists.
P

Proposition 2.5 Let ϕ be a predicate lifting of F along ↓p ; X → F X be aC
coalgebra in C; and P ∈ PX . We have P ≤ JνϕKc if and only if there exists a
ϕ-invariant Q such that P ≤ Q.
2c

The proposition is trivial but potentially useful. It says that an invariant canbe used as a “witness” for a coinductive predicate. This is how bisimilarity iscommonly established; and it can be used e.g. in [1, §6] as an alternative to themetric coinduction principle used there. 1
1 To be precise: only if we take PE in [1] as an atomic proposition (and that is essentially what is done in
the proofs in [1, §6]). Our future work on nested µ’s and ν’s will more adequately address the situation.

6

Hasuo, Cho, Kataoka, Jacobs

Remark 2.6 The coalgebraic modal logic literature exploits the fact that there
can be many predicate liftings (in the form of natural transformations) of the samefunctor F . Different predicate liftings correspond to different modalities (such as
2 vs. 3 for the same functor P). This view of predicate liftings is also the current
paper’s (see Example 2.4).
In contrast, in fibrational studies like [5, 20, 26, 27], use of predicate liftings has
focused on the validity of the (co)induction proof principle. For such purposes it isnecessary to choose a predicate lifting ϕ that is “comprehensive enough,” covering
all the possible F -behaviors. In fact, it is common in these studies that “the”
predicate lifting, denoted by Pred(F ), is assigned to a functor F . An exception
is [31].

3

Final Sequences in a Fibration

Here we present our main technical result (Thm. 3.7). It generalizes known behavioral ω-bounds (like [24, Thm. 2.1]; see §1.1); and claims that the chain (2) fora coinductive predicate stabilizes after ω steps, assuming that the behavior typePfunctor F and the underlying logic ↓p are “finitary” in a suitable sense (but noCsize restriction on ϕ).
3.1

Size Restrictions on a Fibration

We axiomatize finitariness conditions in the language of locally presentable categories (see Appendix A.2 for a minimal introduction). Singling out these conditions
lies at the heart of our technical contribution.
Definition 3.1 (LFP category) A category C is locally finitely presentable(LFP) if it is cocomplete and it has a (small) set F of finitely presentable (FP)objects such that every object is a directed colimit of objects in F.
Definition 3.2 (Finitely determined fibration) A (poset) fibration
finitely determined if it satisfies the following.

P
↓p
C

is

(i) C is LFP, with a set F of FP objects (as in Def. 3.1).
(ii)

P↓p has fiberwise limits and colimits.
C(iii) For arbitrary X ∈ C, let (XI )I∈I be the canonical diagram for X with respectκ
to F (i.e. I = (F ↓ X)), with a colimiting cocone (XI →I X)I∈I . Then for any
P, Q ∈ PX ,
P ≤Q

⇐⇒

κ∗I P ≤ κ∗I Q in PXI for each I ∈ I.

The intuition of Cond. iii) is that a predicate P ∈ PX (over arbitrary X ∈ C) is
determined by its restrictions (κ∗I P )I∈I to FP objects XI . One convenient sufficientcondition for Cond. iii) is that the total category P is itself LFP, with its FP objects
above the FP objects in C (Cor. 5.3). We note that Cond. i) guarantees, since LFP
implies completeness, an (ω op -)limit F ω 1 of the final F -sequence (3). However this7

Hasuo, Cho, Kataoka, Jacobs

does not mean (nor we need for later) that F ω 1 carries a final F -coalgebra (it fails
for F = Pω ; see [44]).
Definition 3.3 (Well-founded fibration) A well-founded fibration is a finitelydetermined fibration that further satisfies:(iv) If X ∈ F (hence FP), the fiber PX is such that: the category Pop
X consists solely
of FP objects.
Since PX is complete, this is equivalent to: there is no (ω op -)chain P0 >P1 > · · · in PX that is strictly descending.
We note that the following stronger variant of the condition(iv’) For any X ∈ C, there is no strictly descending ω op -chain in PX
Pred

rarely holds (it fails in ↓ ). The original Cond. iv) holds in many examples (asSets
we will see later in §5) thanks to the restriction that X is FP.
The following trivial fact is written down for the record.
P

Lemma 3.4 A finitely determined fibration ↓p is well-founded if PX is a finiteCcategory for each X ∈ F.
2
3.2

Final Sequences in a Fibration

The following result from [29, Prop. 9.2.1] is crucial in our development.
P

Lemma 3.5 Let ↓p be a fibration, with C being complete. Then p has fiberwiseClimits if and only if P is complete and p : P → C preserves limits. If this is the case,a limit of a small diagram (PI )I∈I in P can be given byV∗I∈I (πI PI )over LimI∈I XI .

π

Here XI := pPI ; (LimI∈I XI →I XI )I∈I is a limiting cone in C; andthe limit in the fiber PLimI XI .
PVI∈I denotes

2

Fig. 1 presents two sequences. Here we assume that ↓p is finitely determined
C(Def. 3.2) and that ϕ is a predicate lifting of F . In the bottom diagram (in C), theϕω ⊤ 1P⊤1

ϕ⊤1

ϕi ⊤ 1

···

···

b′

ϕω+1 ⊤1
C
1

πi
!

F1

··· F

i−1 !

F i1

F ω1

Fi !

···

F πi−1ω+1FFigure 1. Final sequences in a fibration

8

b

1

Hasuo, Cho, Kataoka, Jacobs!

object 1 ∈ C is a final one (it exists since LFP implies completeness); F 1 → 1 isthe unique map; F ω+1 1 := F (F ω 1); and b is a unique mediating arrow to the limitF ω 1. In the top diagram (in P), the object ⊤1 is the final object in the fiber P1 ; byLem. 3.5 this is precisely a final object in the total category P. Hence this diagram
is nothing but a final sequence for the functor ϕ in P. A limit ϕω ⊤1 of this final
sequence exists, again by Lem. 3.5, and moreover it can be chosen above F ω 1. We
define ϕω+1 ⊤1 := ϕ(ϕω ⊤1 ).
P

Lemma 3.6 (Key lemma) Let ↓p be a well-founded fibration; F : C → C be
C
finitary; and ϕ be a predicate lifting of F . Then the final ϕ-sequence stabilizes afterω steps. More precisely: in Fig. 1, we have ϕω+1 ⊤1 = b∗ (ϕω ⊤1 ).
The object ϕω ⊤1 is a “prototype” of ϕ-coinductive predicates in various coalgebras.
This is one content of the following main theorem.
c
It is standard that a coalgebra X → F X in C induces a cone over the final
F -sequence, and hence a mediating arrow X → F ω 1 (see below). Concretely, ci :c0c
X → F i 1 is defined inductively by: X →1 is !; and ci+1 is the composite X →Fc

F X →i F i+1 1. The induced arrow to the limit F ω 1 is denoted by cω .
F ω1

πi

1

!

F1

F i1

···

···
ci

Theorem 3.7 (Main result) Let

(7)

cω

X

P
↓p be a well-founded fibration; F : C → C beCca finitary functor; ϕ be a predicate lifting of F along p; and X → F X be a coalgebrain C.
(i) The ϕ-coinductive predicate JνϕKc in c (Def. 2.3) exists. It is obtained by thefollowing reindexing of ϕω ⊤1 , where cω is the mediating map in (7).
JνϕKc = c∗ω (ϕω ⊤1 )(8)(ii) Moreover, the predicate JνϕKc is the limit of the following ω op -chain in the fiber
PX⊤X ≥ (c∗ ◦ ϕ)(⊤X ) ≥ (c∗ ◦ ϕ)2 (⊤X ) ≥ · · · ,that stabilizes after ω steps. That is, JνϕKc =Vi∈ω (c∗ ◦ ϕ)i (⊤

(9)
X ).

2

Example 3.8 (Rν) We continue Example 2.4 and derive from Thm. 3.7 the behavioral bound result described in §1.1: the chain (2) stabilizes after ω steps, foreach α ∈ Rνu and each finitely branching Kripke model c.
cIndeed, the latter is the same thing as a coalgebra X → FfbK X, where FfbK =P(AP) × Pω ( ). Compared to FK in Example 2.4 the powerset functor is restrictedfrom P to Pω ; this makes FfbK a finitary functor. Still the same definition of ϕα
defines a predicate lifting of FfbK . Thm. 3.7.ii can then be applied to the fibration
Pred↓(easily seen to be well-founded, Example 5.11), the finitary functor FfbK
Sets

and the predicate lifting ϕα for each α. It is not hard to see that the function[α]c : PX → PX in §1.1 coincides with c∗ ◦ ϕα : PredX → PredX (note that9

Hasuo, Cho, Kataoka, Jacobs

PredX ∼= PX); thus the chain (2) coincides with (9) that stabilizes after ω= 2X ∼
steps by Thm. 3.7.
Remark 3.9 The ω-bound of the length of the chain (9) is sharp.
A (counter)example is given in the setting of Example 3.8, by thepredicate lifting ϕ3u and the coalgebra (i.e. Kripke structure) c2 on
the right. There bi,i has no successors. Indeed, while Jνϕ3u Kc2 is{ai | i ∈ ω}, its i-th approximant ((c2 )∗i ◦ ϕi3u )(⊤X ) in (9) contains
bi,0 too.

c2

a0
b0,0

a1
b1,0
a2
b1,1 b2,0 ..
.
b2,1
b2,2

Remark 3.10 It is notable that Thm. 3.7 imposes no size restrictions on ϕ : P → P.
Being a predicate lifting is enough.
Final F -sequences are commonly used for the construction of a final F -coalgebra.
It is not always the case, however, that the limit F ω 1 is itself the carrier of a final
coalgebra (even for finitary F ; see [44, §5]). One obtains a final coalgebra either by:1) quotienting F ω 1 by the behavioral equivalence (see e.g. [40]); or 2) continuing
the final sequence till ω + ω steps. The latter construction is worked out in [44](in Sets) and in [2] (in LFP C with additional assumptions). Its relevance to thecurrent work is yet to be investigated.
Coalgebra morphisms are compatible with coinductive predicates. This fact, like
Prop. 2.5, is potentially useful in establishing coinductive predicates.
cProposition 3.11 Let f : X → Y be a coalgebra morphism from X → F Y tod
Y → F Y . In the setting of Lem. 3.6 and Thm. 3.7:(i) If Q ∈ PY is a ϕ-invariant in d, so is f ∗ Q ∈ PX in c.
(ii) We have JνϕKc = f ∗ JνϕKd .

2

Remark 3.12 The current paper focuses on finitely presentable objects, finitary
functors, etc.—i.e. the ω-presentable setting (see [4, §1.B]). This is for the simplicity
of presentation: the results, as usual (as e.g. in [34]), can be easily generalized tothe λ-presentable setting for an arbitrary regular cardinal λ. In such an extended
setting we obtain a behavioral λ-bound.

4

A Fibration of Invariants

We organize the above observations in a more abstract fibered setting. The technicalresults are mostly standard; see e.g. [26, 27] and [32, Chap.6].
We write Coalg(F ) for the category of F -coalgebras.
Proposition 4.1 Let ϕ be a predicate lifting of F alongP↓p . Then the fibration
C

Coalg(ϕ)
P↓p is lifted to a fibration↓p, with two forgetful functors forming a map ofC
Coalg(F )fibrations from the latter to the former.

2

The next observation explains the current section’s title.
10

Hasuo, Cho, Kataoka, Jacobs
Coalg(ϕ)↓pbe the lifted fibration in Prop. 4.1. For each coalProposition 4.2 Let
Coalg(F )cgebra X → F X, the fiber over c coincides with the poset of ϕ-invariants in c. That∼=c
Coalg(c∗ ◦ ϕ)
Coalg(ϕ)X →F
X
.
2
is:
PX
Coalg(ϕ)↓phas fiberwise
Therefore Thm. 3.7.i) and Prop. 3.11.ii) state the fibration
Coalg(F )final objects. (At least part of) this statement itself is shown quite easily using theKnaster-Tarski theorem (each fiber is a complete lattice). Our contribution is its
concrete construction as an ω op -limit (Thm. 3.7.ii).
The following is an immediate consequence of Lem. 3.5.
P

Corollary 4.3 Let ϕ be a predicate lifting of F along ↓p ; and assume that a finalCF -coalgebra exists. The following are equivalent.
(i) The coinductive predicate JνϕKc exists for each coalgebra c : X → F X. Moreover they are preserved by reindexing (along coalgebra morphisms).
(ii) There exists a final ϕ-coalgebra that is above a final F -coalgebra.

5

Examples of Fibrations

5.1

Examples at Large

2

Here are several results that ensure a fibration to be finitely determined or wellfounded, and hence enable us to apply Thm. 3.7. Some of them are well-known;others—especially those which relate fibrations and locally (finitely) presentable
categories, including Lem. 5.4 and Cor. 5.7—seem to be new.
Lemma 5.1 [29, Prop. 5.4.7] An (elementary) topos is a locally Cartesian closed
category (LCCC).
2
The following results provide sufficient conditions for a fibration to be finitelydetermined (Def. 3.2). Recall that a full subcategory F of P is said to be dense if
each object P ∈ P is a colimit of a diagram in F.
P

Lemma 5.2 Let ↓p be a fibration with fiberwise limits and colimits. AssumeCfurther that C is LFP with a set FC of FP objects (as in Def. 3.1). If the total
category P has a dense subcategory FP such that every R ∈ FP is above FC (i.e.
pR ∈ FC ), then p is finitely determined.
2
P

Corollary 5.3 Let ↓p be a fibration with fiberwise limits and colimits, where C isC
LFP with a set FC of FP objects (in Def. 3.1). If the total category P is also LFP,
with a set FP of FP objects (as in Def. 3.1) chosen so that every R ∈ FP is above
FC , then p is finitely determined.
2
The following is one of the results that are less trivial.
11Hasuo, Cho, Kataoka, Jacobs

Lemma 5.4 Let C be an LFP category with F being a set of FP objects (as inDef. 3.1). Assume that C is at the same time an LCCC. Then the total category
Sub(C) of the subobject fibration is LFP: the set FSub(C) := { (P ֌ X) | P, X ∈ F}
consists of FP objects in Sub(C); and every object (Q ֌ Y ) ∈ Sub(C) is a colimitof a directed diagram in FSub(C) .
2
It follows from Lem. 5.1, 5.4, and Cor. 5.3 that the internal logic of a topos that is
LFP is finitely determined.
Corollary 5.5 Let C be LFP and at the same time a topos (or more generally an
Sub(C)↓
is finitely determined.
LCCC). Then the subobject fibration
C

We turn to the family fibration

2

Fam(Ω)↓
over a poset Ω (see Appendix A.3).
Sets

Lemma 5.6 Let Ω be an algebraic lattice, i.e. a complete lattice in which eachelement is a join of compact elements. (Equivalently, Ω is LFP when considered asa category.) Then the set
FFam(Ω) :=

f : X → Ω | X is finite; for each x ∈ X, f (x) is compact in Ω

(10)

consists of finitely generated objects and is dense in Fam(Ω). Therefore by Lem. 5.2,
Fam(Ω)↓
is finitely determined.
Sets

2

It is known that the existence of a dense set of FG objects (like FFam(Ω) in Lem. 5.6)
ensures the category to be locally λ-presentable. This is however for some regularcardinal λ that is possibly bigger than ω. See [4, Thm. 1.70].
Corollary 5.7 Let Ω be an algebraic lattice. Then the total category Fam(Ω) of
Fam(Ω)↓
is locally presentable.
Sets

2

We turn to the notion of well-founded fibration (Def. 3.3; see also Lem. 3.4).
Example 5.8 (Presheaf categories) Let A be small. The presheaf category
SetsA is LFP: the set F of finite colimits of representable presheaves yA, where
yA = A(A, ), satisfies the conditions of Def. 3.1.
The coming results are less trivial, too.
Lemma 5.9 Let A be small. For any X ∈ A, Sub(yX) is finite if and only if theyfsubset {Im(yA → yX) | A ∈ A, f : X → A} ⊆ Sub(yX) is finite.
As a special case, if every arrow f with domain X ∈ A factors f = m ◦ e as asplit mono m followed by an epi e, then Sub(yX) is finite if and only if Quot(X)is finite. Here Quot(X) denotes the set of quotient objects of X.
2
Sub(SetsA )↓Corollary 5.10 If one of the conditions in Lem. 5.9 holds, the fibration
SetsA

is well-founded.

2

12

Hasuo, Cho, Kataoka, Jacobs

5.2

Concrete Examples
Pred

Example 5.11 (Pred) The fibration ↓ for the conventional setting of classiSets
cal logic is easily seen to be well-founded. In particular, PredX ∼= PX is finite if
X is FP (i.e. finite). Therefore to any finitary F and any predicate lifting ϕ, theresults in §3 apply.
The (interpretations of the) formulas in Rν (see Example 3.8) are examples ofPredcoinductive predicates in ↓ . Besides them, the study of coalgebraic modal logic
Sets
has identified many predicate liftings for many functors F (probabilistic systems,
neighborhood frames, strategy frames, weighted systems, etc.; see e.g. [12] and thereferences therein). These “modalities” all define coinductive predicates, to which
the results in §3 may apply.
Pred

Rel

↓
via
Example 5.12 (Rel) The fibration ↓ can be introduced from
Sets
Sets
change-of-base; concretely, an object of Rel is a pair (X, R) of a set X and a
relation R ⊆ X × X; an arrow f : (X, R) → (Y, S) is a function f : X → Y suchthat xRx′ implies f (x)Sf (x′ ). See [29, p. 14].
This fibration is also easily seen to be well-founded; therefore to any finitary FRel

the results in §3 apply. A predicate lifting ϕ along ↓ is more commonly calledSets
a relation lifting [27]; by choosing a suitable ϕ (a “sufficiently comprehensive” one)like in [27], a ϕ-invariant is precisely a bisimulation relation, and the ϕ-coinductive
predicate is bisimilarity. We expect that the ω-behavioral bound in Thm. 3.7 can beused to bound execution of bisimilarity checking algorithms by partition refinement(for many different functors F ).
In the following example, one can think of Ω as a Heyting algebra, and then theunderlying logic becomes constructive.
Example 5.13 (Fam(Ω)) Let Ω be an algebraic lattice that has no strictly deFam(Ω)↓
scending (ω op -)chains. Then the family fibration
is well-founded (seeSetsLem. 5.6). Therefore to any finitary F the results in §3 apply. It is not hardto interpret the language Rν in this setting, by defining predicate liftings similar
Fam(Ω)↓.
to (6). This gives examples of coinductive predicates in
Sets

Presheaf Examples
Let F be the category of natural numbers as finite sets (i.e. n = {0, 1, . . . , n−1}) andall functions between them; F+ be its full subcategory of nonzero natural numbers;
and I be the category of natural numbers and injective functions. Coalgebras in
the presheaf categories SetsF , SetsF+ and SetsI are commonly used for modelingprocesses in various name-passing calculi. For the π-calculus SetsI has been foundappropriate (see e.g. [17, 18]); while for the fusion calculus we do need non-injectivefunctions in F or F+ (see [38, 42]).
13

Hasuo, Cho, Kataoka, Jacobs

Inspired by [34], we are interested in coinductive predicates for such processes.
They are naturally modeled in the subobject fibration of a presheaf category. Here
we find a distinction: the subobject fibrations of SetsF and SetsF+ are wellfounded; but that of SetsI is not. In view of Cor. 5.5 and Example 5.8, the only
condition to check is Cond. iv) in Def. 3.3.
Example 5.14 (Sub(SetsF ), Sub(SetsF+ )) The

subobject

Sub(SetsF+ )↓is well-founded: this is shown by Cor. 5.10.
SetsF+

fibration

An important fact

here is that in Sets a mono with a nonempty domain splits.

Sub(SetsF )↓The subobject fibration
is well-founded, too.
SetsF

To show that

Sub(y0) is finite, we appeal to the first half of Lem. 5.9: we observe that theid
set {Im yf | n ∈ F, f : 0 → n} is equal to the two-element set Im(y(0 →0!

!

!

0)), Im(y(0 → 1)) since 0 → n and 0 → m factor through each other, for eachn, m ≥ 1.
We turn to functors F and ϕ. In modeling processes of name-passing calculi
as coalgebras in these categories, one typically uses endofunctors F that are constructed from the following building blocks. Let N ∈ {F, F+ , I}.
•

Constant functors, binary sum +, binary product ×, and exponentials ( )X .
These are much like for polynomial functors on Sets. An important example ofthe first is the name presheaf N = Hom(1, ) ∈ SetsN .

•The abstraction functor δ : SetsN → SetsN given by δX = X( + 1).

The free semilattice functor Pf for finite branching. This captures Kuratowski
finiteness and suitable in SetsI . See e.g. [17, 42].
e is more• In SetsF and SetsF+ , another choice of a “finite powerset functor” K•

appropriate. See [38]; also [42, p. 4].

All such functors are known to be finitary (see e.g. [38]).
Coinductive predicates in this setting can be introduced much like Rν in Example 2.4 (note that SetsN is a topos), for properties like deadlock freedom. Sucha language can be extended further through the modalities proposed in [34]: theycorrespond to constructions specific to presheaves and include the modality ha(b)ifor a binding ‘input’ operation. More examples will be worked out in our future
paper.
Example 5.15 (Sub(Setsω ), Sub(SetsI )) Consider the presheaf category Setsω
Sub(Setsω )↓over the ordinal ω as a poset. The fibration
is finitely determinedSetsω

but not well-founded. It fails to satisfy Cond. iv) in Def. 3.3: let Pn : ω → Sets be
the family of presheaves defined byPn (m) :=0 if m < n;

1 if n ≤ mfor each n ∈ ω. Then P0 > P1 > · · · is a strictly descending chain in Sub(y0). The
same counterexample works for Sub(SetsI ).
14

Hasuo, Cho, Kataoka, Jacobs

In contrast, the subobject fibration for Setsω

opis well-founded by Lem. 5.9.

Remark 5.16 Well-foundedness fails in Sub(Setsω ), Sub(SetsI ), and in Fam(Ω)
for Ω that does have a strictly descending ω op -chain. This means the logics modeledby the fibrations are inherently “big.” Still, extensions of our results in §3 arepossible from finitary (i.e. ω-presentable) to the λ-presentable setting for bigger λ,so that they apply to the (current) nonexamples.
Acknowledgments
Thanks are due to Kazuyuki Asada, Keisuke Nakano, Keiko Nakata, Ana
Sokolova, and the participants of Dagstuhl Seminar 12411 “Coalgebraic Logics” (including Samson Abramsky, Vincenzo Ciancia, Corina Cı̂rstea, Ernst-Erich
Doberkat, Clemens Kupke, Alexander Kurz, and Yde Venema) for useful discussions. We are grateful to the anonymous referees for their careful reading anduseful suggestions, too. I.H., K.C. and T.K. are supported by Grants-in-Aid forYoung Scientists (A) No. 24680001 and Grants-in-Aid for Challenging Exploratory
Research No. 23654033, JSPS, and by Aihara Innovative Mathematical Modeling
Project, FIRST Program, JSPS/CSTP.

References[1] S. Abramsky and V. Winschel. Coalgebraic analysis of subgame-perfect equilibria in infinite games
without discounting, 2012. ArXiv:1210.4537.
[2] J. Adámek. On final coalgebras of continuous functors. Theor. Comp. Sci., 294:3–29, 2003.
[3] J. Adámek, F. Bonchi, M. Hülsbusch, B. König, S. Milius and A. Silva. A coalgebraic perspective on
minimization and determinization. In Birkedal [7], pp. 58–73.
[4] J. Adámek and J. Rosický. Locally Presentable and Accessible Categories, vol. 189 of London Math.
Soc. Lect. Note Series. Cambridge Univ. Press, 1994.
[5] R. Atkey, N. Ghani, B. Jacobs and P. Johann. Fibrational induction meets effects. In Birkedal [7], pp.
42–57.
[6] Y. Bertot and E. Komendantskaya. Inductive and coinductive components of corecursive functions in
Coq. Elect. Notes in Theor. Comp. Sci., 203(5):25–47, 2008.
[7] L. Birkedal, editor. Foundations of Software Science and Computational Structures - 15th International
Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practiceof Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, vol. 7213 of Lect.
Notes Comp. Sci. Springer, 2012.
[8] F. Bonchi and D. Pous. Checking nfa equivalence with bisimulations up to congruence. In Giacobazzi
and Cousot [21], pp. 457–468.
[9] J. Bradfield and C. Stirling. Modal mu-calculi. In P. Blackburn, J. van Benthem and F. Wolter, editors,
Handbook of Modal Logic, vol. 3 of Studies in Logic and Practical Reasoning, chap. 12. Elsevier, 2006.
[10] C. Cı̂rstea. Maximal traces and path-based coalgebraic temporal logics.
412(38):5025–5042, 2011.

Theor. Comput. Sci.,[11] C. Cı̂rstea, C. Kupke and D. Pattinson. Exptime tableaux for the coalgebraic µ-calculus. In E. Grädeland R. Kahle, editors, CSL, vol. 5771 of Lecture Notes in Computer Science, pp. 179–193. Springer,
2009.
[12] C. Cı̂rstea, A. Kurz, D. Pattinson, L. Schröder and Y. Venema. Modal logics are coalgebraic. Comput.
J., 54(1):31–41, 2011.
[13] C. Cı̂rstea and M. Sadrzadeh. Modular games for coalgebraic fixed point logics. Electr. Notes Theor.
Comput. Sci., 203(5):71–92, 2008.

15

Hasuo, Cho, Kataoka, Jacobs[14] P. Cousot and R. Cousot. Constructive versions of Tarski’s fixed point theorems. Pacific Journal of
Mathematics, 82(1):43–57, 1979.
[15] G.L. Ferrari, U. Montanari and M. Pistore. Minimizing transition systems for name passing calculi: A
co-algebraic formulation. In M. Nielsen and U. Engberg, editors, FoSSaCS, vol. 2303 of Lect. Notes
Comp. Sci., pp. 129–158. Springer, 2002.
[16] G.L. Ferrari, U. Montanari and E. Tuosto. Coalgebraic minimization of hd-automata for the pi-calculus
using polymorphic types. Theor. Comp. Sci., 331(2–3):325–365, 2005.
[17] M. Fiore and D. Turi. Semantics of name and value passing. In Logic in Computer Science, pp. 93–104.
IEEE, Computer Science Press, 2001.
[18] M.P. Fiore and S. Staton. Comparing operational models of name-passing process calculi. Inf. &Comp., 204(4):524–560, 2006.
[19] M.P. Fiore and S. Staton. A congruence rule format for name-passing process calculi. Inf. & Comp.,
207(2):209–236, 2009.
[20] C. Fumex, N. Ghani and P. Johann. Indexed induction and coinduction, fibrationally. In A. Corradini,
B. Klin and C. Cı̂rstea, editors, CALCO, vol. 6859 of Lect. Notes Comp. Sci., pp. 176–191. Springer,
2011.
[21] R. Giacobazzi and R. Cousot, editors. The 40th Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013. ACM, 2013.
[22] I. Hasuo. Generic forward and backward simulations II: Probabilistic simulation. In P. Gastin and
F. Laroussinie, editors, CONCUR, vol. 6269 of Lect. Notes Comp. Sci., pp. 447–461. Springer, 2010.
[23] I. Hasuo, B. Jacobs and A. Sokolova. Generic trace semantics via coinduction. Logical Methods inComp. Sci., 3(4:11), 2007.
[24] M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journ. ACM,
32(1):137–161, 1985.
[25] U. Hensel and B. Jacobs. Proof principles for datatypes with iterated recursion. In E. Moggi and
G. Rosolini, editors, Category Theory and Computer Science, no. 1290 in Lect. Notes Comp. Sci., pp.
220–241. Springer, Berlin, 1997.
[26] C. Hermida. Fibrations, Logical Predicates and Indeterminates. PhD thesis, Univ. Edinburgh, 1993.
Techn. rep. LFCS-93-277.
[27] C. Hermida and B. Jacobs. Structural induction and coinduction in a fibrational setting. Inf. & Comp.,
145:107–152, 1998.
[28] C.K. Hur, G. Neis, D. Dreyer and V. Vafeiadis. The power of parameterization in coinductive proof.
In Giacobazzi and Cousot [21], pp. 193–206.
[29] B. Jacobs. Categorical Logic and Type Theory. North Holland, Amsterdam, 1999.
[30] B. Jacobs. Trace semantics for coalgebras. In J. Adámek and S. Milius, editors, Coalgebraic Methods
in Computer Science, vol. 106 of Elect. Notes in Theor. Comp. Sci. Elsevier, Amsterdam, 2004.
[31] B. Jacobs. Predicate logic for functors and monads, March 2010. Preprint.
[32] B. Jacobs. Introduction to coalgebra. Towards mathematics of states and observations, 2012. Draft ofa book (ver. 2.0), available online.
[33] P. Johnstone. Sketches of an Elephant: A Topos Theory Compendium. Oxford Logic Guides. Clarendon
Press, 2002.
[34] B. Klin. Coalgebraic modal logic beyond Sets. In MFPS XXIII, vol. 173, pp. 177–201. Elsevier,
Amsterdam, 2007.
[35] D. Kozen and N. Ruozzi. Applications of metric coinduction. Logical Methods in Computer Science,
5(3), 2009.
[36] C. Kupke. Terminal sequence induction via games. In P. Bosch, D. Gabelaia and J. Lang, editors,
TbiLLC, vol. 5422 of Lecture Notes in Computer Science, pp. 257–271. Springer, 2007.
[37] M. Makkai and R. Paré. Accessible categories: the foundations of categorical model theory. Contemp.
Math., 104, 1989.
[38] M. Miculan. A categorical model of the fusion calculus. Elect. Notes in Theor. Comp. Sci., 218:275–293,
2008.

16

Hasuo, Cho, Kataoka, Jacobs[39] K. Nakata, T. Uustalu and M. Bezem. A proof pearl with the fan theorem and bar induction—walking
through infinite trees with mixed induction and coinduction. In H. Yang, editor, APLAS, vol. 7078 of
Lecture Notes in Computer Science, pp. 353–368. Springer, 2011.
[40] D. Pattinson. An introduction to the theory of coalgebras. Course notes for NASSLLI, 2003. Available
online.
[41] J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theor. Comp. Sci., 249:3–80, 2000.
[42] S. Staton. Relating coalgebraic notions of bisimulation. Logical Methods in Comp. Sci., 7(1), 2011.
[43] Y. Venema. Automata and fixed point logic: A coalgebraic perspective. Inf. Comput., 204(4):637–678,
2006.
[44] J. Worrell. On the final sequence of a finitary set functor. Theor. Comp. Sci., 338(1–3):184–199, 2005.

17

Hasuo, Cho, Kataoka, Jacobs

A

Appendix: Preliminaries

A.1

Theory of Coalgebra

Given a category C and an endofunctor F : C → C, an F -coalgebra is a pair of X ∈ C
cand an arrow c : X → F X (we shall denote a coalgebra simply by X → F X). The
notion has turned out to be a useful categorical abstraction of state-based dynamiccsystems. In an F -coalgebra X → F X, the carrier object X ∈ C is understood asa state space; the functor F specifies the behavior type; and the arrow c represents
actual dynamics. In the most common setting of C = Sets, examples of functors F(and the corresponding behavior types) are:•A × ( ) for A-stream automata;•P(AP) × P( ) for Kripke models;•P(AP) × Pω ( ) for finitely branching Kripke models, with where Pω is the finite
powerset functor;•P(A × ) for labeled transition systems;•

D(A × ) for generative probabilistic systems;

and so on. See [32, 41] for detailed introduction.
In the theory of coalgebra as a categorical theory of (state-based dynamical)
systems, the notion of final coalgebra plays a prominent role. A final F -coalgebraζc

Z → F Z is one such that, for any F -coalgebra X → F X, there is a unique morphismof coalgebras from c to ζ.
FX
c

X

Fc
c

FZ

(A.1)

final ζZ

Its system-theoretic significance is that: 1 Z is often the collection of “all possible
F -behaviors”; and 2 the induced arrow c assigns, to each state in X, its behavior.
The “behaviors” here follow a black-box view on systems (it ignores internal states)and often captures the natural notion of “F -bisimilarity.”
Therefore a question arises if a final F -coalgebra exists. The well-known Lambek
lemma (that ζ is necessarily an iso) prohibits e.g. a final P-coalgebra. What mattershere is the size of F : when it is suitably bounded, a concrete construction of a final
coalgebra is known. It obtains a final coalgebra via a final F -sequence (Here 1 is a
final object in C).
1

!

F1

··· F

i−1 !

i

F i1 F ! · · ·(A.2)

In particular, if F is finitary (a size restriction described later), a final coalgebra
arises as a suitable quotient of the limit of the final sequence (3). This construction
in Sets is worked out in [44]; it is further extended to locally presentable categories(those are categories suited for speaking of “size”) with additional assumptionsin [2]. The current paper’s goal is to apply this construction also to coinductive
predicates.
18

Hasuo, Cho, Kataoka, Jacobs

A.2

Locally Finitely Presentable Categories

The theory of coalgebra has been mainly developed in the base category C = Sets.
Exceptions include the category of nominal sets or (pre)sheaf categories (e.g. [18,19])
for name-passing calculi, and Kleisli categories (e.g. [22,23]) for trace semantics andsimulation. The current paper follows [2, 34] and finds locally finitely presentable
categories a convenient abstract setting. Here we follow [4] and list a minimal setof definitions and results on locally finitely presentable categories.
The following is a categorical formalization of “finiteness” of objects. Examples
are finite sets (in Sets), and algebras presented by finitely many generators andfinitely many equations (in suitable categories of algebras).
Definition A.1 (Finitely presentable object) An object X ∈ C is finitely presentable (FP) if the functor C(X, ) : C → Sets preserves filtered colimits.
Definition A.2 (Locally finitely presentable category) A category C is locally finitely presentable (LFP) if it is cocomplete and it has a (small) set F of
FP objects such that every object is a directed colimit of objects in F.
Lemma A.3 Let C be LFP, with a set F of FP objects as in Def. 3.1; and X ∈ C.
The canonical diagram for X with respect to Fπ

(F ↓ X) −→ F ֒−→ C(A.3)

has X as its colimit. Here π is the projection.
Proof The proof of [4, Prop. 1.22] yields the claim.

2

Lemma A.4 [4, Cor. 1.28 & Prop. 1.61] Let C be LFP.
(i) C is complete.
(ii) C has (StrongEpi, Mono)- and (Epi, StrongMono)-factorization structures. 2
The following notion (which is already in Def. A.1) is about the “size” of functors.
An intuition (when C = Sets) is: a functor F is finitary if F ’s action F X on anarbitrary set X is determined by its action F X ′ on all the finite subsets X ′ ⊆ X.
Definition A.5 (Finitary functor) An endofunctor F : C → C is finitary if it
preserves filtered colimits.
This notion is commonly used to bound the “branching degree” of systems as F coalgebras. For example, the finite powerset functor Pω is finitary; the (full) powerset functor P is not.
There are many LFP categories, among which are Sets, the category Posetsof posets and monotone maps, and categories of algebras with finitary operations.
See [4] for more examples.
Example A.6 (Presheaf categories) Let A be a small category. The presheaf
category SetsA is LFP: the set
F := {finite colimits of representable presheaves yA} ,where yA = A(A, ), satisfies the conditions of Def. A.1.
19

Hasuo, Cho, Kataoka, Jacobs

Definition A.7 (Finitely generated object) An object X ∈ C is finitely generated (FG) if the functor C(X, ) : C → Sets preserves directed colimits of monos—that is, directed colimits of diagrams in which every (connecting) arrow is a mono.
It is clear that FP implies FG. In algebraic terms, FP objects are algebras presented
by finitely many generators and finitely many equations; while for FG objects only a
set of generators is required to be finite. The two notions coincide in “non-algebraic”
examples such as Sets. See [4, §1.E].

A.3

Fibrations

We follow [29], although we focus on the simpler notion of poset fibration.
Introduction (via Indexed Posets)
This paper’s interest is in coinductive predicates, hence in predicate logic. The
most straightforward formalization of predicate is as a subset P ⊆ X of a set (a‘universe’) X: an element x ∈ X satisfies P if x ∈ P . Accompanying is the natural
notion of entailment: P entails Q if P ⊆ Q. This way we obtain the poset (2X , ⊆)of predicates over X.
However it is not on a single universe X that we consider predicates. For
example, in a situation where there are two Kripke models c = (X, →, VX ),d = (Y, →, VY ) and a “homomorphism” f : X → Y , a natural question is if theinterpretation of a formula νu.α is preserved by f . (It is; see Prop. 3.11). Here weare comparing the predicate Jνu.αKc ⊆ X with the predicate Jνu.αKd ⊆ Y reindexed
via f : X → Y . The latter is concretely described as the inverse imagef −1 Jνu.αKd



=



x ∈ X f (x) ∈ Jνu.αKd.

Therefore a reindexing structure is also relevant to predicate logic: a function f :X → Y induces reindexing f −1 : 2Y → 2X . Additionally, the map f −1 is monotone.
To summarize: 1) predicates on a universe X form a poset; 2) a function f : X →Y between universes induces a monotone reindexing function from the collectionof predicates over X to that over Y . Such a situation is nicely described as a(contravariant) functor
Φ : Cop −→ Posets ,(A.4)

where Posets is the category of posets and monotone functions. The functor Φ
assigns, to each ‘universe’ X ∈ C, the poset ΦX of predicates over X. Moreover,f : X → Y in C induces a reindexing map Φf : ΦY → ΦX. This functor Φ is a
special case of an indexed category [29, §1.10].
In the current paper, however, we favor an equivalent presentation of such astructure by a fibration, since we find the latter to be more amenable to generalization of structures in ordinary category theory (such as limits). The equivalence between index categories and fibrations are well-known; here we sketch theGrothendieck construction from the former to the latter. Its idea is to “patch up”
20Hasuo, Cho, Kataoka, Jacobs

the posets (ΦX)X∈C and form a big category P, as in the following figure.
•
•

ΦX
•

•
Φf

←−

•
X

ΦY

•
“patch up”

•

=⇒

•
f

Y

P

•

•
•
•

•

p

•

C

X

f

Y

On the right we add some arrows (denoted by 99K) so that we have an arrow(Φf )(Q) → Q in P for each Q ∈ ΦY . (On the left the arrows p99K depicts the actionof the map Φf .) The above diagram in P should be understood as a Hasse diagram:
those arrows which arise from composition are not depicted.
Formally:
Definition A.8 (The Grothendieck construction) Given Φ : Cop → Posets,
we define the category PΦ by•

its object is a pair (X, P ) of an object X ∈ C and an element P of the poset ΦX;
and•its arrow f : (X, P ) → (Y, Q) is an arrow f : X → Y in C such thatP ≤ (Φf )(Q) .
Here ≤ refers to the order of ΦX.

Thus arises a category PΦ that incorporates: the order structure of each of theposets (ΦX)X∈C ; and the reindexing structure by (Φf )f : C-arrow . For fixed X ∈ C,
the objects of the form (X, P ) and the arrows idX between them form a subcategoryof P. This is denoted by PX and called the fiber over X. It is obvious that PX is aposet that is isomorphic to ΦX.
Moreover, there is a canonical projection functor p : P → C that carries (X, P )to X.
Formal Definition of (Poset) Fibration
We axiomatize those structures which arise in the way described above.
P

Definition A.9 ((Poset) fibration) A (poset) fibration ↓p consists of two catC
egories P, C and a functor p : P → C, that satisfy the following properties.
•

Each fiber PX is a poset. Here the fiber PX for X ∈ C is the subcategory of P
consisting of objects P ∈ P such that pP = X and arrows f : P → Q such that
pf = idX (such arrows are said to be vertical ).

•Given f : X → Y in C and Q ∈ PY , there is an object f ∗ Q ∈ PX and a P-arrowf Q : f ∗ Q → Q with the following universal property. For any P ∈ PX andg : P → Q in P, if pg = f then g factors through f (Q) uniquely via a verticalarrow. That is, there exists a unique g ′ such that g = f (Q) ◦ g ′ and pg ′ = idX .
f ∗Q

Q

P

g
p

C

=⇒

X

f

Y

Q

g

P
X

21

f (Q)

′

f

Y

Hasuo, Cho, Kataoka, Jacobs•

The correspondences ( )∗ and ( ) are functorial:
id∗Y Q = Q ,(g ◦ f )∗ (Q) = f ∗ (g ∗ Q) ,g ◦ f (Q) = gQ ◦ f (g ∗ Q) .

idY (Q) = idQ ,The last equality can be depicted as follows.
Pf ∗ (g ∗ Q)p(g ◦ f )∗ Q

f (g ∗ Q)

gQ

Qg◦f (Q)
f

X

C

g∗ Q

Y

g

Z

The category P is called the total category of the fibration; C is the base category.
The arrow f Q : f ∗ Q → Q is called the Cartesian lifting of f and Q. An arrow in P
is Cartesian (or reindexing) if it coincides with f Q for some f and Q.
P

In the case where ↓p is induced by an indexed category Φ : Cop → Posets via
CDef. A.8, a Cartesian lifting is obviously given by f ∗ (Q) = (Φf )(Q).
In the current paper we focus on poset fibrations (which we shall simply call
fibrations). In a (general) fibration a fiber PX is not just a poset but a category,
and this elicits a lot of technical subtleties. Nevertheless, it should not be hard togeneralize the current paper’s results to general, not necessarily poset, fibrations(especially to the split ones).
We shall often denote a vertical arrow in P (i.e. an arrow inside a fiber) by ≤.
ExamplesExample A.10 (Subobject fibration) Let C be a (well-powered) category withfinite limits. The category Sub(C) is defined by: its object is a pair (P, X) of
X ∈ C and its subobject P ֌ X (we write (P ֌ X) ∈ Sub(C)); and its arrowf(P ֌ X) → (V ֌ Y ) is a C-arrow f : X → Y that restricts to P → Q. That is,given an arrow f : X → Y in C,
f is an arrow in Sub(C)mfn(P ֌ X) → (Q ֌ Y )P⇐⇒ ∃f ′ s.t. m
X

f′

Q

(A.5)

n.

Y

f

The projection (P ֌ X) 7→ X defines a functor; thus arises the
Sub(C)

f↓of C. In particular, given X → Y in C
subobject fibrationCand (Q ֌ Y ) ∈ Sub(Y ), the Cartesian lifting f ∗ Q is defined by apullback.

f ∗Q

fQ

Q

m

X

n
f

Y

A special case is the following most straightforward modeling of predicate logic. It
arises from the contravariant powerset functor 2( ) : Setsop → Posets via Def. A.8.

22

Hasuo, Cho, Kataoka, Jacobs
Sub(Sets)
Pred↓↓of Sets is denoted by) The subobject fibration
Example A.11 (
Sets
Sets
Pred
↓ . An object of its total category is often denoted by (U ⊆ X). Reindexing is
Setsgiven by inverse images.
More concretely, in the category Pred, an object is a pair (P, X) of a set X andff

its subset P ⊆ X; an arrow (P ⊆ X) → (Q ⊆ Y ) is a function X → Y that restricts
to P → Q (i.e. P ⊆ f −1 Q).
Rel

Pred

Example A.12 (Rel) The fibration ↓ can be introduced from ↓ via the
Sets
Sets
following change-of-base.
Pred
Rel
Sets X7→X×X Sets
Concretely, an object of Rel is a pair (X, R) of a set X and a relation R ⊆ X × X;
an arrow f : (X, R) → (Y, S) is a function f : X → Y such that xRx′ implies
f (x)Sf (x′ ). See [29, p. 14].
Fam(Ω)↓
Example A.13 (Family fibration) The family fibration
over a poset Ω
Sets

is introduced as follows. An object in the fiber Fam(Ω)X is a function f : X → Ω;fkg

and an arrow (X → Ω) → (Y → Ω) in the total category Fam(Ω) is a function
k : X → Y such that f (x) ≤ g(k(x)) for each x ∈ X. See e.g. [29, Def. 1.2.1] formore details.
Structures in a Fibration
P

f∗

f

In a fibration ↓p , a C-arrow X → Y induces a correspondence PY → PX via
Creindexing. This is easily seen to be a monotone map (i.e. a functor between posets
as categories).
P

Definition A.14 (Fiberwise (co)limits) A fibration ↓p is said to have fiberC
wise limits if:V• each fiber PX has, as a category, all limits (meaning it has arbitrary inf’s); and•f∗f

for each C-arrow X → Y , the reindexing functor PY → PX preserves these limits.

In this case each fiber PX has a final object (denoted by ⊤X ).
Similarly, a fibration has fiberwise colimits if each fiber has them and they arepreserved by reindexing.
The following notions must be distinguished from “fiberwise (co)products.”
P

Definition A.15 ((Co)products between fibers) A fibration ↓p is said toChave products (between fibers) if
Q• each reindexing functor f ∗ : PY → PX has a right adjoint f ∗ ⊣f ; andQ• the functors (f )f satisfy the so-called Beck-Chevalley condition. See [29, §1.9].
23

Hasuo, Cho, Kataoka, Jacobs

Similarly, a fibration has coproducts (between fibers) if each reindexing has a left`
adjoint f and they satisfy the Beck-Chevalley condition.
Pred

The prototype example ↓ has fiberwise (co)limits: each fiber is a complete
Sets
V
W
`
lattice; andandare preserved by inverse images. It has (co)products`
between fibers, too: specifically f is given by the direct image of the function f .
See [29, §1.9].
Throughout the paper we rely on the following result. It follows from [29,Lem. 9.1.2 & Prop. 9.2.1], and extends Lem. 3.5.
P

Lemma A.16 Let ↓p be a fibration. Assume that C is complete; then the followC
ing are equivalent.
(i) The fibration p has fiberwise limits.
(ii) The total category P is complete and p : P → C preserves limits.
If this is the case, a limit of a small diagram (PI )I∈I in P can be given byV∗I∈I (πI PI )over LimI∈I XI .

V
πHere XI := pPI ; (LimI∈I XI →I XI )I∈I is a limiting cone in C; and I∈I denotes
the limit computed in the fiber PLimI XI .
P`
(Sort of ) dually, let ↓p be a fibration with coproducts
between fibers, andCassume that C is cocomplete. Then p has fiberwise colimits if and only if P iscocomplete and p : P → C preserves colimits. In this case a colimit of a small
diagram (PI )I∈I in P can be given by
W

I∈I (

`

κI PI )

over ColimI XI ,

κ

where XI := pPI and (XI →I ColimI XI )I∈I is a colimiting cocone in C.

B

Appendix: Omitted Proofs

B.1

Proof of Lem. 3.62

Proof We proceed by steps.
a) We observe that, in Fig. 1, the top diagram is carried to the one below by thefunctor p : P → C. This is straightforward: the arrow ϕ⊤1 → ⊤1 must be carried
to the unique arrow ! : F 1 99K 1; on the mediating arrow b′ in P, since pb′ is again
a mediating arrow in C, it must coincide with b.
b) Before moving on, we observe that Cond. iii) in Def. 3.2 yields a seemingly
stronger statement (Cond. iii’) below).
Sublemma B.1 For a finitely determined fibrationP↓p the following holds.
Ciii’) Let X ∈ C; P, Q ∈ PX ; and (YJ )J∈J be an arbitrary filtered diagram in C suchγJthat ColimJ YJ = X, with a colimiting cocone (YJ →X)J∈J . Then P ≤ Q if and24

Hasuo, Cho, Kataoka, Jacobs

only if for each J ∈ J, γJ∗ P ≤ γJ∗ Q in PYJ .
Proof (Of Sublem. B.1) The only nontrivial statement is the ‘if’ part of the direction iii) ⇒ iii’). It suffices to show that γJ∗ P ≤ γJ∗ Q (for each J ∈ J) implies
κ∗I P ≤ κ∗I Q (for each I ∈ I), where κI and I are as in Cond. iii).
Let I ∈ I. Since XI is FP, an arrow κI : XI → X to a filtered colimit X =γJColimJ YJ factors through some YJI →I X, as in the diagram below.
κI

XI
hI

YJ I

γJ

X = ColimJ YJ
I

Now we have κ∗I P = h∗I γJ∗I P ≤ h∗I γJ∗I Q = κ∗I Q, where the inequality is by theassumption that γJ∗ P ≤ γJ∗ Q for each J ∈ J. This proves Sublem. B.1.
2c) By Step a) we see that ϕω+1 ⊤1 ≤ b∗ (ϕω ⊤1 ) by the universality of a Cartesian
arrow. In what follows we shall prove its converse:b∗ (ϕω ⊤1 ) ≤ ϕω+1 ⊤1in PF ω+1 1 .

(B.1)

Let us take a directed diagram (XI )I∈I in C such that XI ∈ F (for each I ∈ I) andκ
F ω 1 = ColimI∈I XI , with (XI →I F ω 1)I∈I being the colimiting cocone. Then wehaveF ω+1 1 = F (Colim XI ) = Colim F XI ,
I∈I

I∈I

Fκ

by the assumption that F is finitary; moreover (F XI →I F ω+1 1)I∈I is a colimiting
cocone. The diagram (XI )I∈I is directed, and so is the latter diagram (F XI )I∈I .
Thus by Cond. iii’) in Sublem. B.1, showing the following proves (B.1).
(F κI )∗ b∗ (ϕω ⊤1 )≤ (F κI )∗ (ϕω+1 ⊤1 )for each I ∈ I.

(B.2)d) To prove (B.2) we first prove the following fact: for each I ∈ I there exists
iI ∈ ω such that
in PXI .
κ∗I (ϕω ⊤1 ) = κ∗I πi∗I (ϕiI ⊤1 )(B.3)

That is: the final sequence in P (Fig. 1), when restricted to XI (that is FP), stabilizes
within finitely many steps. Indeed, by Lem. A.16 the limit ϕω ⊤1 is described as an
inf in PF ω 1 :V(B.4)
ϕω ⊤1 = i∈ω πi∗ (ϕi ⊤1 ) .
V
∗
∗
ω
∗
i
∗
Therefore we have κI (ϕ ⊤1 ) = i∈ω κI πi (ϕ ⊤1 ) since reindexingκI preserves fiber
V
i∗∗wise limits . Now we claim that the sequence κI πi (ϕ ⊤1 ) i∈ω in PXI is descend
ing: it follows from the fact that πi∗ (ϕi ⊤1 ) i∈ω in PF ω 1 is descending, which inturn is shown from the universality of the Cartesian arrow πi (ϕi ⊤1 ). See below.
πi∗ (ϕi ⊤1 )

πi (ϕi ⊤1 )!

∗ (ϕi+1 ⊤ )
πi+1
1

P
ϕi ⊤ 1

ϕi+1 ⊤1
πi

C

F i1

Fi !

F i+1 1

25

F ω1
πi+1

Hasuo, Cho, Kataoka, Jacobs

Therefore, by p being a well-founded fibration (Def. 3.3), there exists iI ∈ ω atwhich the descending sequence stabilizes, that is,
V

∗ i
∗
iI
i∈ω πi (ϕ ⊤1 ) = πiI (ϕ ⊤1 )in PF ω 1 .

Combined with (B.4), this proves (B.3).
e) Finally let us prove (B.2). For each I ∈ I,(F κI )∗ b∗ (ϕω ⊤1 )V
by (B.4)= (F κI )∗ b∗ i∈ω πi∗ (ϕi ⊤1 )VVreindexing preserves= i∈ω (F κI )∗ b∗ πi∗ (ϕi ⊤1 )V= i∈ω (F κI )∗ (F πi−1 )∗ (ϕi ⊤1 )by πi ◦ b = F πi−1 (see Fig. 1)
by Def. 2.2= i∈ω ϕ (πi−1 ◦ κI )∗ (ϕi−1 ⊤1 )
≤ ϕ (πiI ◦ κI )∗ (ϕiI ⊤1 )letting i = iI + 1 on the LHS= ϕ κ∗I πi∗I (ϕiI ⊤1 ) = ϕ κ∗I (ϕω ⊤1 )by (B.3)
V= (F κI )∗ (ϕω+1 ⊤1 )by Def. 2.2 and ϕω+1 ⊤1 = ϕ(ϕω ⊤1 ).
This proves (B.2) and concludes the proof of Lem. 3.6.
B.2

2

Proof of Thm. 3.7

Proof We proceed by steps.
ia) We first show that c∗ω (ϕω ⊤1 ) indeed carries a (c∗ ◦ ϕ)-coalgebra.
c∗ ϕ(c∗ω (ϕω ⊤1 ))



by Def. 2.2= c∗ (F cω )∗ (b∗ (ϕω ⊤1 ))by Lem. 3.6= c∗ (F cω )∗ (ϕ(ϕω ⊤1 ))

= (b ◦ F cω ◦ c)∗ (ϕω ⊤1 )= c∗ω (ϕω ⊤1 ) .
For the last equality we used b ◦ F cω ◦ c = cω , which is proved by showing thatb ◦ F cω ◦ c is also a mediating map in (7). Indeed, for each i ∈ ω,
πi ◦ b ◦ F c ω ◦ c= F πi−1 ◦ F cω ◦ c= F ci−1 ◦ c= ci

by (7)

by def. of ci .
26

see Fig. 1

Hasuo, Cho, Kataoka, Jacobsib) We show that the coalgebra obtained in Step a) is final. Let U ≤ c∗ (ϕU ) be
an arbitrary (c∗ ◦ ϕ)-coalgebra (i.e. a ϕ-invariant in c), where U ∈ PX . We aim toestablish the following diagram in P and see that it is above the one in (7).
ϕω ⊤ 1⊤1

ϕ⊤1ϕi ⊤ 1

···

···

c′ω

(B.5)

U

We first show thatU ≤ c∗i (ϕi ⊤1 )for each i ∈ ω.

(B.6)

The proof is by induction. The base case i = 0 is obvious since reindexing c∗ipreserves ⊤. For the step case:U ≤ c∗ (ϕU )U carries a (c∗ ◦ ϕ)-coalgebra≤ c∗ ϕ c∗i (ϕi ⊤1 )by induction hypothesis= c∗ (F ci )∗ (ϕi+1 ⊤1 ) by Def. 2.2= (ci+1 )∗ (ϕi+1 ⊤1 )by def. of ci+1 .

This proves (B.6) and establishes the arrows U → ϕi ⊤1 in (B.5), for each i. Therefore we obtain a mediating map c′ω : U 99K ϕω ⊤1 to the limit ϕω ⊤1 , too. The arrowc′ω is easily shown to be above cω (much like b′ in Fig. 1 is shown to be above b); thismeans U ≤ c∗ω (ϕω ⊤1 ). Since PX is a poset, this arrow ≤ is necessarily a coalgebramorphism from U to c∗ω (ϕω ⊤1 ); moreover it is a unique such. This proves i).
ii) We haveJνϕKc
= c∗ω (ϕω ⊤1 ) by i)V= c∗ω i∈ω πi∗ (ϕi ⊤1 ) by Lem. A.16
VV
= i∈ω c∗ω πi∗ (ϕi ⊤1 ) since reindexing preservesV= i∈ω c∗i (ϕi ⊤1 ) by def. of cω .

(B.7)

Furthermore, c∗i (ϕi ⊤1 ) in the above is seen to be equal to (c∗ ◦ ϕ)i (⊤X ). This isshown by induction on i ∈ ω. For i = 0 the claim amounts to !∗ (⊤1 ) = ⊤X , whichholds since reindexing preserves ⊤. For the step case,c∗i+1 (ϕi+1 ⊤1 )= c∗ (F ci )∗ (ϕi+1 ⊤1 ) by ci+1 = F ci ◦ c= c∗ ϕ c∗i (ϕi ⊤1 ) by Def. 2.2= (c∗ ◦ ϕ) (c∗ ◦ ϕ)i (⊤X )by induction hypothesis.
27

Hasuo, Cho, Kataoka, Jacobs

Finally let us check that the chain (9) stabilizes after ω steps.
(c∗ ◦ ϕ)V

= (c∗ ◦ ϕ)i∈ω (cV∗ ◦ ϕ)i ⊤X∗ ii∈ω ci (ϕ ⊤1 )= (c∗ ◦ ϕ) c∗ω (ϕω ⊤1 )







by the previous paragraphby (B.7)



by Def. 2.2= c∗ (F cω )∗ b∗ (ϕω ⊤1 )by Lem. 3.6= c∗ (F cω )∗ ϕ(ϕω ⊤1 )= c∗ω (ϕω ⊤1 ) by b ◦ F cω ◦ c = cω , see Step 1a)V= c∗ω ( i∈ω πi∗ (ϕi ⊤1 )) by (B.4)
V= i∈ω c∗ω πi∗ (ϕi ⊤1 )V
= i∈ω c∗i (ϕi ⊤1 )V
= i∈ω (c∗ ◦ ϕ)i ⊤X by the previous paragraph.
This concludes the proof.
B.3

2

Proof of Prop. 3.11

Proof 1)f ∗ Q ≤ f ∗ d∗ (ϕQ)

Q is an invariant= c∗ (F f )∗ (ϕQ)

f is a homomorphism= (c∗ ◦ ϕ)(f ∗ Q)

by Def. 2.2.
d

c

ω
ω
F ω 1,F ω 1 and Y →2) The coalgebras give rise to mediating arrows X →respectively, as in (7). It is easy to see that cω = dω ◦ f (using the universality of
the limit F ω 1); using (8) the claim follows.
2

Proof of Prop. 4.1

B.4

c

f

c
Proof It is easy to check each fiber Coalg(ϕ)X →F
is a poset. Let (X → F X) →
X

d

s

d

(Y → F Y ) be an arrow in Coalg(F ), and P → ϕP be above Y → F Y . A Cartesian
lifting of f are obtained as in the following diagram.
P

ϕf ∗ P
t
f ∗P

C

FX

ϕf (P )ϕPsf (P )
Ff

P
FY

c

X

d
f

Y

Here we used the universality of the Cartesian lifting ϕf (P ) (see Def. 2.2).
28

Hasuo, Cho, Kataoka, Jacobs

The two forgetful functors constitute a map of fibrations: the commutativity (4)is obvious, and Cartesian liftings inbased on the Cartesian liftings in
B.5

Coalg(ϕ)↓p(which we constructed above) are
Coalg(F )

P
↓p .
C

2

Proof of Prop. 4.2sc

Proof Given a ϕ-coalgebra P → ϕP above X → F X, we use the universality of
the Cartesian lifting of c to obtain a (c∗ ◦ ϕ)-coalgebra as in the following diagram.
c∗ ϕP
Pc(ϕP )ϕPst

Conversely, given a (c∗ ◦ ϕ)-coalgebra Q → c∗ (ϕQ), we obtain a ϕ-coalgebra abovec
X → F X as the following composite.
c∗ ϕQ

c(ϕQ)

ϕQ

t

Q
Then it is straightforward to see that the mappings are monotone and inverse toeach other. The mappings commute with the forgetful functors since they do notchange the carriers.
2
B.6

Proof of Lem. 5.4

Proof The proof is by steps.
a) First we show that Sub(C) is complete and cocomplete. We rely on Lem. A.16.
Sub(C)↓
We start with fiberwise limits in; the proof is like in [29, ExamC

ple 1.8.3(iii)]. By Lem. A.4 an LFP category C is complete. This equips eachVfiber Sub(X) with arbitrary inf’s
computed as wide pullbacks. A reindexing
functor (by pullbacks) preserves these inf’s since limits commute. Therefore by
Lem. A.16 the total category Sub(C) is complete.
Sub(C)
Q↓
has products f ⊢ f ∗ between
By the assumption that C is an LCCC,
C

fibers [29, Cor. 1.9.9].

Sub(C)↓
Next we show thathas fiberwise colimits. Each fiber (which is a poset)C
has arbitrary inf’s; hence it is a complete lattice and arbitrary sup’s also exist.
These sup’s (i.e. colimits in a fiber) are preserved by reindexing f ∗ since the latterQ
is a left adjoint f ∗ ⊣ f .
Sub(C)`↓
We further show thathas coproducts
between fibers. An abstract
C
proof can be given by Freyd’s adjoint functor theorem (note that each fiber Sub(X)29

Hasuo, Cho, Kataoka, Jacobs

is a complete lattice, and that reindexing f ∗ preserves inf’s). Instead we explicitly`
introduce
exploiting a factorization structure of LFP C (Lem. A.4.ii). Namely,`mgiven (P ֌ X) ∈ Sub(X) and f : X → Y , the coproduct f P is defined by the(StrongEpi, Mono)-factorization of f ◦ m, as below.
`

P
m

X

f P

(B.8)

Y

f

`
The fact that f P ≤ Q if and only if P ≤ f ∗ Q is easily proved using the diagonal`
ization property of the factorization structure. This establishes f as a left adjoint`
to reindexing f ∗ . These coproducts
satisfy the Bech-Chevalley condition sinceQ
the products
do [29, Lem. 1.9.7]. Using Lem. A.16 we conclude that Sub(C) is
cocomplete.
mb) First we prove that, if P and X are both FP in C, then (P ֌ X) is FP innIn

Sub(C). Let (QI ֌ YI )I∈I be a filtered diagram in Sub(C); (Q ֌ Y ) its colimit;mnand g : (P ֌ X) → (Q ֌ Y ) an arrow in Sub(C). By Lem. A.16 the colimit(Q ֌ Y ) can be explicitly described as_`(B.9)
Y = Colim YI ,Q=
κI Q I ,
I∈I

I∈I

κ

where (YI →I Y )I∈I is a colimiting cocone.
Sublemma B.2 The object Q ∈ C is a colimit ColimI∈I QI computed in C.
Proof (Of the sublemma) Both (QI )I∈I and (YI )I∈I are I-shaped diagrams in CnI

with a monotransformation (QI ֌ YI )I . Therefore by [4, Cor. 1.60], the induced arrow ColimI QI → ColimI YI is monic, establishing ColimI QI ∈ Sub(Y ). It suffices
to find arrows a, b in the diagram below.
aColimI QI

Q

b(B.10)nY

The arrow a is obtained in the following way. Since κI is an arrow (QI ֌ YI ) →(Q ֌ Y ) in Sub(C), by (A.5) we have an arrow QI → Q in C, for each I ∈ I. These
arrows induce a as a mediating arrow.
W `To obtain b in (B.10), since Q = I∈I κI QI (see (B.9)), it suffices to find bI
below for each I ∈ I.
`

bI

κI QI

ColimI QIYThis is obtained as the following diagonal fill-in. Recall that Y = ColimI YI .
nI

QI

`

YI

κI QI

bI

κI

ColimI QI [κ ◦n ] ColimI YII

I IThis proves Sublem. B.2.

230

Hasuo, Cho, Kataoka, Jacobsmn

We are back in Step b). Since g : (P ֌ X) → (Q ֌ Y ) is an arrow in Sub(C),we also have an arrow g ′ : P → Q, such that n ◦ g ′ = g ◦ m, by (A.5). Now Q
and Y are filtered colimits of (QI )I∈I and (YI )I∈I , respectively (the former is bySublem. B.2). Since P and X are FP, I0 ∈ I can be chosen such that g factors
through YI0 → Y and g ′ factors through QI0 → Q. That is,
g′
h′

P

QI 0

Q

YI 0

Y

nI 0

m

X

h

g

n
κI0

.

It is not (yet) necessarily the case that the square on the left commutes, i.e. nI0 ◦h′ = h ◦ m. The two arrows give factorizations of the arrow n ◦ g ′ = g ◦ m : P → Y
κI
via YI0 →0 Y ; since P is FP, there exists I1 ∈ I with i : I0 → I1 such that
(Y i) ◦ nI0 ◦ h′ = (Y i) ◦ h ◦ m(essential uniqueness of factorization, [4, Def. 1.1]). It is clear that, for such I1 , theκIarrow g in Sub(C) factors through (QI1 ֌ YI1 ) →1 (Q ֌ Y ). This concludes Stepb) that (P ֌ X) is FP in Sub(C).
c) Recall that
(B.11)FSub(C) := { (P ֌ X) | P, X ∈ F} .

The set FSub(C) in (B.11) is small, since F is small and C is well-powered [4,Rem. 1.56].
nd) In the remainder of the proof we show that every object (Q ֌ Y ) ∈ Sub(C)is a colimit of the canonical diagram with respect to FSub(C) from (B.11). LetnJ(QJ ֌ YJ )J∈J be the canonical diagram (i.e. J = (FSub(C) ↓ n)), with the canonicalcoconenJ
nfJ(B.12)(QJ ֌ YJ ) −→(Q ֌ Y ) J∈J .

Let us denote the canonical diagram for Y ∈ C with respect to F by (YI′ )I∈I (i.e.
κ
I = (F ↓ Y )), with a canonical cocone (YI′ →I Y )I∈I . The cocone is colimiting (Y =ColimI∈I YI′ ) since C is LFP. In this Step d) we show ColimJ∈J YJ ∼= ColimI∈I YI′ =Y.

κIA cocone (YJ →J ColimI∈I YI′ )J∈J can be defined by finding (unique) IJ ∈ I
fI′

f

J
Y . In order to see that this cocone is colimiting,such that YI′J →J Y is equal to YJ →gJ
let (YJ →Z)J∈J be another cocone (recall that J = (FSub(C) ↓ n)).

Sublemma B.3 If the indices J, J ′ ∈ J satisfy YJ = YJ ′ and fJ = fJ ′ (cf. (B.12)),then gJ = gJ ′ .
Proof (Of the sublemma) Let 0 be an initial object in C. We first prove that 0 is a
subobject of any object of C. Indeed, since C is an LCCC (hence a CCC), its initial
object 0 is strict, meaning that if U → 0 exists then U is also initial (a standard
result; see e.g. [33, Lem. 1.5.12]). This makes any arrow 0 → V in C a mono.
Therefore we have an object (0 ֌ YJ ) in Sub(C) induced by initiality. In view31Hasuo, Cho, Kataoka, Jacobsof (A.5), an arrow fJ in C induces an arrownfJ =fJ ′(0 ֌ YJ )in Sub(C);(Q ֌ Y )nJ ′′therefore there exists an index J ′′ ∈ J = (FSub(C) ↓ n) such that (0 ֌ YJ ) = (QJ ′′ ֌
YJ ′′ ), and fJ ′′ = fJ = fJ ′ .
This gives us the following diagram in J = (FSub(C) ↓ n).
nJ(QJ ֌ YJ )

nJ ′′

idYJ

(QJ ′′ ֌ YJ ′′ )

idY ′

nJ ′

J

(QJ ′ ֌ YJ ′ )gJZ)J∈J is a cocone, the following diagram in C must commute.
Therefore, since (YJ →

id

YJ
gJ

YJ ′′

id

gJ ′′

Z

YJ ′
gJ ′

This proves gJ = gJ ′ = gJ ′′ , as required in Sublem. B.3.

2

f′

I
Y in (F ↓ Y ), there exists JI ∈ J such
We are back in Step d). For each YI′ →′′that YJI = YI and fJI = fI (one can take the initial object 0, which is FP, as QJI ).
Using such JI we obtain an arrow[gJI ]I∈I : Colim YI′ −→ Z .
I∈IThat this is a mediating arrow, i.e. that the diagram
YJ

gJ
κI

J

ColimI∈I YI′Z[gJ ]I∈I
I

commutes, is precisely the content of Sublem. B.3. Uniqueness of a mediating arrowis easy, too. This proves ColimJ∈J YJ ∼= ColimI∈I YI′ .
e) By Step d) we obtain Y = ColimJ∈J YJ . In view of Lem. A.16, we are done ifW`
we show that Q = J∈J fJ QJ .
W`
One direction Q ≥ J∈J fJ QJ is easy: since fJ in (B.12) is an arrow in Sub(C)`we have QJ ≤ fJ∗ Q, that is, fJ QJ ≤ Q, for each J ∈ J.
W`
To prove the other direction (Q ≤ J∈J fJ QJ ), let (QK )K∈K be the canonicaldiagram for Q with respect to F (i.e. K = (F ↓ Q)), with the canonical cocone
cK(QK →Q)K∈K . Then Q = ColimK∈K QK since C is LFP; furthermore, much likeW`
the proof of Sublem. B.2, we can show that ColimK∈K QK ∼= K∈K cK QK . Henceit suffices to show`

c K QK ≤

W

J∈J

`

fJ QJ

in Sub(Y ), for each K ∈ K.

It is easy to see (using (A.5)) that n ◦ cK is an arrow
id

n◦c

n

K
(QK ֌ QK ) −→(Q ֌ Y )32(B.13)

Hasuo, Cho, Kataoka, Jacobs

in Sub(C). Since QK ∈ F, this arrow n ◦ cK is an object of the index category
J = (FSub(C) ↓ n). This yields`

n◦cK QK ≤Now the following diagram shows that
via the uniqueness of factorization.

W

`

J∈J

`

fJ QJ

.

(B.14)`cK QK as a subobject of Y ,n◦cK QK =

cK

`

QK

cK QK

Q

n

Y

∼
=

`

n◦cK QK

Therefore (B.14) proves (B.13). This concludes the proof.
B.7

2

Proof of Lem. 5.2

Proof The only nontrivial part is the ⇐ direction of Cond. iii). For that it suffices
to show that arbitrary P ∈ P is a colimit of the diagram (κ∗I P )I∈I . Here I and κI
are as in Cond. iii).
W `By Lem. A.16 the colimit ColimI∈I κ∗I P is described as I∈I κI κ∗I P using a
W
`
κ
sup
in PX , since (XI →I X)I∈I is colimiting. We have κI κ∗I P ≤ P as a counitof an adjunction; therefore ColimI∈I κ∗I P ≤ P .
Thus it suffices to show that P ≤ ColimI∈I κ∗I P in PX . Let (PJ )J∈J be a diagramgJ
in P such that PJ ∈ FP and there is a colimiting cocone (PJ →P )J∈J . Such adiagram exists since FP is dense.
By the assumption, for each J the object PJ ∈ FP lies above an object in
FC . Therefore the arrow pgJ : pPJ → pP = X is an object of (FC ↓ X); sincegJ
I = (FC ↓ X), we can choose IJ ∈ I such that κIJ = pgJ . Now an arrow PJ →P in
P induces(B.15)PJ ≤ (pgJ )∗ P = κ∗IJ P
by the universality of Cartesian arrows. We proceed as follows.
(∗) W

P = ColimJ∈J PJ =

J∈J

`

(†) W

pgJ PJ ≤J∈J`∗κIJ κIJ P

≤

_`

(∗)
∗
∗
κI κI P = ColimI∈I κI P.

I∈I

For (∗) we used Lem. A.16; (†) holds since IJ is chosen so that κIJ = pgJ and (B.15)
hold. This concludes the proof.
2
B.8

Proof of Lem. 5.6

Proof 1a) Let us first see that Fam(Ω) is cocomplete. In view of Lem. A.16, it
Fam(Ω)`↓
suffices to show thathas fiberwise colimits and coproducts
betweenSets
fibers (the base category Sets is cocomplete). The former follows from Ω being acomplete lattice; the latter is shown from [29, Lem. 1.9.5].
1b) Before going on we prove the following.
33

Hasuo, Cho, Kataoka, Jacobs

Sublemma B.4 An arrow in Fam(Ω) is a mono if and only if its underlying function is a mono in Sets.
f

Proof (Of Sublem. B.4) The ‘if’ part is obvious. For the ‘only if’ part, let (X →mgΩ) ֌ (Y → Ω) be a monic arrow in Fam(Ω), and k, l : U → X be arrows in Sets
such that m ◦ k = m ◦ l. This induces the following situation in Fam(Ω):(⊥ : U → Ω)kl(f : X → Ω)m(g : Y → Ω),

where ⊥ : U → Ω is the constant function to the least element ⊥ ∈ Ω. Therefore2
k = l; this proves Sublem. B.4.
f1c) We prove that each (X → Ω) ∈ FFam(Ω) is FG (Def. A.7) in Fam(Ω). Let

gI
g
h
(YI →
Ω) →I (Y → Ω) I∈I be a colimiting cocone from a directed diagram I whosefgkarrows are all monos; and (X → Ω) → (Y → Ω) be an arrow in Fam(Ω). We aim
at showing that k factors through some hI .
By Lem. A.16 we obtain that Y = ColimI∈I YI ; and that

`
W `
W
g(y) = ( I∈I hI gI )(y) = I∈I ( hI gI )(y)WW
= I∈I y′ ∈h−1 (y) gI (y ′ ) for each y ∈ Y .

(B.16)I

The first equality is by Lem. A.16; the second is because the order in the fiber
Fam(Ω)Y = ΩY is pointwise; and the third is by the concrete description [29,Lem. 1.9.5] of`in

Fam(Ω)↓.
Setsh

We observe that each hI is a mono in Fam(Ω). To see it, (YI →I Y )I∈I is acolimiting cocone in Sets from a directed diagram of monos; since Sets is LFP, we
can use [4, Prop. 1.62]; and then we use Sublem. B.4.
Now we havef (x) ≤ g(k(x)) =

W

I∈I

W

gI (y ′ )y ′ ∈h−1
I (k(x));

here the first inequality is because k is an Fam(Ω)-arrow; and the second equality
is from (B.16). By the assumptions that f (x) is compact and that X is finite, thereW
exists I0 ∈ I such that f (x) ≤ y′ ∈h−1 (k(x)) gI0 (y ′ ) for each x ∈ X (recall that I is
I0kfiltered). Furthermore, since X → Y = ColimI∈I YI is an arrow from an FP object(in Sets) to a directed colimit, it factors through some hI1 :
X

lI 1
k

Y I1
Y

hI 1

.

By choosing I2 such that I0 , I1 ≤ I2 , we havef (x) ≤W

gI2 (y ′ ) = gI2 (lI2 (x))
y ′ ∈h−1
I (k(x))2

34

for each x ∈ X;

Hasuo, Cho, Kataoka, Jacobs

here the last equality holds since hI is an injection and hI (lI (x)) = k(x). ThisgI

fproves that lI2 is a Fam(Ω)-arrow (X → Ω) → (YI2 →2 Ω), hence k = hI2 ◦ lI2 in
Fam(Ω). This concludes Step 1c).
1d) The collection FFam(Ω) is obviously small.
1e) We are done if we prove that every object P ∈ Fam(Ω) is a directed colimitof its subobjects from FFam(Ω) . This easily follows from the fact that the same istrue in Sets (obvious) and in Ω (being an algebraic lattice).
2
B.9

Proof of Lem. 5.9

Proof Any presheaf P ∈ SetsA has a canonical isomorphism Colim(A,p)∈R P yA ∼=P induced by (yA)(B)
=
A(A,
B)
∋
g
→
7
P
(g)(p)
∈
P
(A)
for
A
∈
A
and
R
p ∈ P (A), where P is the category of elements of P . (Remark: The categoryof elements of covariant functor P : A → Sets consists of objects (A, p) in theabove and arrows h : (A, p) → (B, q) for all arrows h : B → A in A such that
P (h)(q) = p.) In the situation, we assume that P is a subpresheaf of yX. Then
P (g) = (yX)(g) = (g ◦ ) shows that arrows {( ◦ f ) = yf : yA → yX}(A,f )induce the composition (Colim(A,f )∈R P yA) ∼= P ֒→ yX. Regarding P as the im
R
age Im (Colim(A,f )∈ P yA) ֌ yX , the following component-wise calculation onS
objects B ∈ A shows P = (A,f )∈R P Im yf :Im ( Colim
R yA) → yX (B)(A,f )∈ P

= Im ( Colim
R yA)(B) → yX(B)(∗)(A,f )∈ P



Colim
= Im
yA(B) → yX(B)R(†)(A,f )∈ P

 `

R
yA(B)
/∼
→
yX(A)
= Im
(A,f )∈ P

 `


`
yA(B) ։yA(B) /∼ → yX(A)= Im
S= (A,f )∈R P Im yA(B) → yX(B)


S
S
R
= (A,f )∈R P (Im yf )(B) =(A,f )∈ P Im yf (B),
(†)

(∗)

where ∼ is a suitable equivalence relation in the explicit formula of colimits in Sets.
Note that Im in the first line and the last line are the images in SetsA while they
denote the images in Sets elsewhere; and that (∗) and (†) holds because limits andcolimits are component-wise, with a fact for (∗) that an image is an equalizer ofa cokernel pair in both Sets and SetsA . Therefore, there are only finitely many
subpresheaves P of yX if {Im yf | A ∈ A, f : X → A} is finite.
For the special case in the second half, we first prove the following.
Sublemma B.5 The inclusion relation on {Im yf | A ∈ A, f : X → A} is derived
from a preorder . on {f | A ∈ A, f : X → A} such that (f : X → A) . (g : X → B)
iff f = h ◦ g for some h : B → A.
Proof (Of Sublem. B.5) If Im yf ⊆ Im yg, then f = (yf )A (idA ) ∈ Im(yf )(A) ⊆Im(yg)(A) = {h ◦ g | h : B → A}. Conversely, for f = h ◦ g, any arrow k ◦ f =35

Hasuo, Cho, Kataoka, Jacobs(yf )C (k) ∈ Im(yf )(C) is in Im(yg)(C) because k ◦ f = k ◦ h ◦ g = (yg)C (k ◦ h). 2
It is enough to show that Quot(X) ∋ Y 7→ Im(yY ֌ yX) ∈ {Im yf | A ∈A, f : A → X} is a bijection. It is obviously injective because epis e : X ։ Y ande′ : X ։ Y ′ factor through each other if and only if e and e′ are the same objects in
Quot(X). We shall prove the mapping is surjective. Let f : X → A be an arbitrary
arrow and f = m ◦ e be its factorization. Then, Im yf ⊆ Im ye and conversely,
we also have Im ye ⊆ Im yf by e = r ◦ f for a retraction r of m. Therefore,
Im yf = Im ye is a image of the mapping.
2
B.10

Proof of Cor. 5.10

Sublemma B.6 Let (XI )I be a finite diagram in SetsA . If Sub(XI ) is finite foreach I, then so is Sub(ColimI XI ).
Proof (Of Sublem. B.6) In a topos (hence a regular category) SetsA coproducts
are disjoint (see e.g. [29]); thus we have
Sub(X1 + · · · + Xn ) ∼= Sub(X1 ) × · · · × Sub(Xn ) .
e

Let X ⇒ Y ։ Z be a coequalizer in SetsA . The correspondence e∗ : Sub(Z) →Sub(Y ) is easily seen to be injective. Indeed, assume P ∼6 P ′ in Sub(Z); then=′P A 6∼= P A for some A ∈ A in Sets, and since eA is surjective, we have′∗∼(e∗ P )A = e−1
6 e−1
A (P A) = (e P )A .
A (P A) =Therefore if Sub(Y ) is finite, so is Sub(Z). This concludes the proof of the sublemma.
2
Proof (Of Cor. 5.10) By Example 5.8, Lem. 5.1, Sublem. B.6, and Cor. 5.5.

362