Math. Struct. in omp. Science (2018), vol. 28, pp. 562 611. c ambridge University Press 2017 doi:10.1017/s0960129517000056 First published online 18 April 2017 oinductive predicates and final sequences in a fibration IHIRO HASUO, TOSHIKI KATAOKA, and KENTA HO Department of omputer Science, The University of Tokyo, Tokyo 113-8656, Japan Email: ichiro@is.s.u-tokyo.ac.jp Research Fellow of Japan Society for the Promotion of Science, 5-3-1, Kouji-machi, hiyoda-ku, Tokyo 102-0083, Japan Email: toshikik@is.s.u-tokyo.ac.jp Institute for omputing and Information Sciences, Radboud University, P.O.Box 9010, 6500 GL Nijmegen, the Netherlands Email: K.ho@cs.ru.nl Received 9 January 2015; revised 22 November 2016 oinductive predicates express persisting safety specifications of transition systems. Previous observations by Hermida and Jacobs identify coinductive predicates as suitable final coalgebras in a fibration a categorical abstraction of predicate logic. In this paper, we follow the spirit of a seminal work by Worrell and study 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. 1. Introduction oinductive predicates postulate properties of state-based dynamic systems that persist after a succession of transitions. In computer science, safety properties of non-terminating, 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 Hermida and Jacobs (1998) and Hermida (1993) whose results are further extended in Fumex et al. (2011) and Atkey et al. (2012), see also Jacobs (2012, hap. 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 notably in Worrell (2005) and Adámek (2003) in such a fibrational setting. oalgebras have been successfully used as a categorical abstraction of transition systems (see e.g. Jacobs (2012); Rutten (2000)): By varying base categories and functors, coalgebras bring general results that work for a variety of systems at once. Fixed point logics (or modal logics in general), too, have been actively studied coalgebraically: oalgebraic
oinductive predicates and final sequences in a fibration 563 modal logic is a prolific research field (see îrstea et al. 2011); their base category is typically Sets but works like Klin (2007) go beyond and use presheaf categories for processes in name-passing calculi; and literature including îrstea and Sadrzadeh (2008), Venema (2006) and îrstea et al. (2009) studies coalgebraic fixed point logics. Unlike most of these works, we follow Hermida and Jacobs (1998) and Hermida (1993) and parameterize the underlying predicate logic too with the categorical notion of fibration. The conventional setting of classical logic is represented by the fibration Pred Sets (see Appendix for an introduction to fibrations). fibration P p Pred Sets Rel Sets coalgebra invariant bisimulation final coalgebra coinductive predicate bisimilarity However, there are various other logics modelled as fibrations, and hence the fibrational language provides a uniform treatment of these different settings. An example is binary relations (instead of unary predicates) that form a fibration Rel (see Appendix ). In this Sets case, coinductive predicates are bisimilarity relations (see the above table, and Example 7.2 later). Another example is predicates in constructive logics. They are modelled by the subobject fibration of a topos. In fact, coinductive predicates in constructive logics are an emerging research topic: oinduction is supported in the theorem prover oq (based on the constructive calculus of constructions), see e.g. Bertot and Komendantskaya (2008), and working in oq, some interesting differences between classically equivalent (co)inductive predicates have been studied, e.g. in Nakata et al. (2011). Yet another example is modal logics for processes in various name-passing calculi. They are best modelled by the subobject fibration of a suitable (pre)sheaf category like Sets I and Sets F (Fiore and Turi 2001; Fiore and Staton 2006; Miculan 2008; Stark 1996; Staton 2011). 1.1. oinductive predicates and their construction, conventionally In order to illustrate our technical contributions (Section 3), we here present a special case, with classical logic and Kripke models. We first introduce syntax. Definition 1.1 (Rudimentary logic Rν). In this tiny fragment of the μ-calculus, fixed-point operators are limited to the greatest one at the outermost position; and moreover, all the formulas are rank-1, that is, the fixed-point variable u occurs precisely under one modal operator. Rν u α ::= a a u u α α α α ; 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).
I. Hasuo, T. Kataoka and K. ho 564 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. Among specifications expressible in Rν is (may-) deadlock freedom (there is an infinite path). It is expressed by νu.u 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) isa valuation. The conventional interpretation [νu.α] c of Rν-formulas in the Kripke model c is given as follows (see e.g. Bradfield and Stirling (2006)). First, we interpret α Rν u as a function [α] c : PX PX. oncretely: [a] c (P )={x a V (x)} [a] c (P )={x a V (x)} [u] c (P )={x y X.(x y implies y P )} [α α ] c (P )=[α] c (P ) [α ] c (P ) [u] c (P )={x y X.(x y and y P )} [α α ] c (P )=[α] c (P ) [α ] c (P ) This 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 monotone function [α] 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 non-constructive. In contrast, a well-known iterative construction (ousot and ousot 1979) computes [νu.α] c as the limit of the following descending chain (see also Bradfield and Stirling (2006)). Here, denotes the subset X X. [α] c [α] 2 c. (2) An issue now is the length of the chain. If [α] c preserves limits (which is the case with α u), clearly ω steps are enough and yields i ω( [α] i c ) as the greatest fixed point. This is not the case with α u. Indeed, for the Kripke model c 1 below [νu.u] c1 i ω( [u] i c1 ) : there is no infinite path from the root; but it satisfies [u] i c 1 (there is a path of length i) foreachi. c 1 (3). Yet the chain (2) eventually stabilizes, bounded by the size of the poset PX: Ineachstep before stabilization, at least one element must be thrown away. Therefore, the calculation of [νu.α] c proceeds, in general, via transfinite induction. This is what we call a state space bound for the chain (2). Besides a state space bound, another (possibly better and seemingly less known) bound can be obtained from a behavioural view. One realizes that not only the size of the state space X but also the branching degree can be used to bound the length of the chain(2).
oinductive predicates and final sequences in a fibration 565 This is a result similar to the one in Hennessy and Milner (1985, Theorem 2.1); the latter is stated for bisimilarity as a coinductive relation, not for a coinductive predicate. We formally state (an instance of) the result for the record. Lemma 1.2 (Behavioural bound). Let c =(X,,V) be a finitely branching Kripke model. For α = u, the chain (2) stabilizes after ω steps and yields [νu.u] c as its limit, that is, i ω( [u] i c ) =[νu.u] c. Proof. The essence of the result lies in the fact that the limit i ω( [u] i c ) is a invariant, which we shall prove now. Assume that a state x satisfies i ω( [u] i c ) ( ;we have to show that x satisfies [u] c i ω( [u] i c )), that is, there is a successor x of x that satisfies the limit i ω( [u] i c ). Since x satisfies [u] i c (there is a path of length i) foreachi, foreachi 1, there is a successor x i of x that satisfies [u] c i 1. Byc being finitely branching, the set {x 1,x 2,...} of such successors turns out to be finite and there exists a successor x of x such that x = x i for infinitely many i. It follows (from [u] i c [u] j c if j i) that this x satisfies [u] i c for all i ω, and hence satisfies i ω( [u] i c ). This proves that the limit i ω( [u] i c ) is an invariant, and hence i ω( [u] i c ) [νu.u] c. For the last equality claimed in the lemma, the other direction [νu.u] c ( i ω [u] i c ) is easy: [νu.u] c [u] i c is easily shown by induction on i. This concludes the proof. Note that Lemma 1.2 holds however large the state space X is. Moreover, it easily generalizes from νu.u to an arbitrary Rν-formula νu.α. Note also that the counterexample c 1 in Equation (3) is not finitely branching and does not contradict with Lemma 1.2. 1.2. Final sequences in a fibration This paper is about putting the observations in Section 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-behavioural equivalence. Therefore, a natural question is if a final F-coalgebra exists; the well-known Lambek lemma prohibits e.g. a final P-coalgebra for the (full) powerset functor P. What matters is the size of F: When it is suitably bounded, it is known that a final coalgebra can be constructed via the following final F-sequence: 1! F1 F! F i 1! F i 1 F i!. (4) Here, 1 is a final object in, and! is the unique arrow. In particular, if F is finitary, a final coalgebra arises as a suitable subobject (or a quotient) of the ω-limit of the final sequence (4). These constructions in Sets are worked out in Pattinson (2003) and Worrell (2005); the one in Worrell (2005) is further extended to locally presentable categories (those are categories suited for speaking of size ) with additional assumptions in Adámek (2003).
I. Hasuo, T. Kataoka and K. ho 566 Turning back to coinductive predicates, indeed, the fibrational view (Hermida 1993; Hermida and Jacobs 1998) identifies coinductive predicates as final coalgebras in a fibration. This leads us to scrutinize final sequences in a fibration. Our main result (Theorem 3.9) is a categorical generalization of the behavioural ω-bound (Section 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. Adámek and Rosický (1994); also Appendix B); and the combination of fibrations and locally presentable categories does not seem to have been studied a lot (an exception is Makkai and Paré (1989, Section5.3)). We therefore develop a relevant categorical infrastructure (Section 6). Our results there include a sufficient condition for the total category Sub() of a subobject fibration to be locally (finitely) presentable, and the same for a family fibration Fam(Ω). Via these results, in Section 7, we list some concrete examples of fibrations to which our results in Section 3 on the behavioural bounds apply. They include Pred Rel Sub() (classical logic), Sets Sets (for bisimulation and bisimilarity), for that is locally finitely presentable (LFP) and locally artesian closed (a topos is a special case) Fam(Ω) and for a well-founded algebraic lattice Ω. Sets 1.3. ontributions To summarize, our contributions are (1) combination of the mathematical observations in Hermida (1993), Hermida and Jacobs (1998) and (Jacobs 2012, hap. 6) for a general formulation of coinductive predicates; (2) categorical behavioural bounds for final sequences that approximate coinductive predicates and (3) a categorical infrastructure that relates fibrations and locally presentable categories. ompared to the earlier version (Hasuo et al. 2013) of the current paper, the main differences are as follows. Here, we additionally address inductive predicates over coinductive datatypes (see Section 5). We identify them as coinductive predicates in the fibrewise P (op) opposite p (op) of the original fibration P p, so that the difference between inductive and coinductive predicates becomes a matter of categorical duality. The examples in Section 7 are extended accordingly, studying inductive predicates on top of coinductive ones. Besides, we include all the proofs that were omitted in Hasuo et al. (2013) for space reasons. 1.4. Organization of the paper In Section 2, we identify coinductive predicates as final coalgebras in a fibration, following the ideas of Hermida (1993), Hermida and Jacobs (1998) and Jacobs (2012). The main technical results are in Section 3, where we axiomatize size restrictions on fibrations and functors for a final sequence to stabilize after ω steps. These results are reorganized in Section 4 in a fibration of invariants. We see in Section 5, which is added to an earlier version of this paper (Hasuo et al. 2013), that the results in Section 2 4 apply to inductive
oinductive predicates and final sequences in a fibration 567 predicates too. The next two sections are devoted to examples: First in Section 6, we develop a necessary categorical infrastructure; and then in Section 7, we discuss concrete examples. In Section 8, we conclude with some directions of future work. In Appendices, we present minimal introductions to the theories of coalgebras, locally presentable categories and fibrations the three categorical disciplines that our technical developments rely on. 2. oinductive predicates as final coalgebras In this section, we follow the ideas in Hermida (1993), Hermida and Jacobs (1998), Jacobs (2012) and characterize coinductive predicates in various settings (for different behaviour types, and in various underlying logics) in the language of fibrations. An introduction to fibrations is e.g. in Jacobs (1999); see also Appendix. In this paper, for simplicity, we focus on poset fibrations. It should however not be hard to move to general fibrations. onvention 2.1 (Fibration). We refer to poset fibrations (where each fibre is a poset rather than a category) simply as fibrations. Definition 2.2 (Predicate lifting). Let P p be a fibration and F be an endofunctor on. A predicate lifting of F along p is a functor ϕ: P P such that (ϕ, F) is an endomap of fibrations. ϕ P P p p (5) F This means: that the above diagram commutes; and that ϕ preserves artesian arrows, that is, ϕ(f Q)=(Ff) (ϕq). See below. P p f Q fq Q ϕ(f Q) X f (Ff) (ϕq) Y FX Ff ϕ(fq) Ff(ϕQ) ϕq In the prototype example Pred, the above definition coincides (see Jacobs 2012) with Sets the one used in coalgebraic modal logic (see e.g. îrstea et al. (2011)), the latter being a (monotone) natural transformation 2 ( ) ϕ 2 F( ) : Sets op Sets. In particular, the naturality requirement corresponds to the preservation of artesian arrows (6); and monotonicity of ϕ comes from the functoriality of ϕ: P P. We think of predicate liftings as (co)recursive definitions of coinductive predicates (see Example 2.4). On top of it, we identify coinductive predicates (and invariants) as coalgebras in a fibre. FY (6)
I. Hasuo, T. Kataoka and K. ho 568 Definition 2.3 (Invariant, coinductive predicate). Let ϕ be a predicate lifting of F along P p ;andx c FX be a coalgebra in. They together induce an endofunctor (a monotone ϕ c function) on the fibre P X,namelyP X PFX P X,whereϕ restricts to P X P FX because of Equation (5). 1. A ϕ-invariant in c is a (c ϕ)-coalgebra in P X, that is, an object P P X such that P c (ϕp )inp X. 2. The ϕ-coinductive predicate in c is the final (c ϕ)-coalgebra (if it exists). Its carrier shall be denoted by νϕ c. It is therefore the largest ϕ-invariant in c; Lambek s lemma yields that νϕ c =(c ϕ)(νϕ c ). Example 2.4 (Rν). The conventional interpretation [νu.α] c (described in Section 1.1) of Rν-formulas is a special case of Definition 2.3. Indeed, let us work in the fibration Pred Sets, and with the endofunctor F K = P(AP) P( )onsets. AnF K -coalgebra X c P(AP) PX is precisely a Kripke model: c combines a valuation X P(AP) andthemapx PX that carries a state to the set of its successors. To each formula α Rν u,weassociatea predicate lifting ϕ α of F K. This is done inductively as follows: ϕ a (U X) = ( {V F K X a π 1 (V )} F K X ), ϕ a (U X) = ( {V F K X a π 1 (V )} F K X ), ϕ u (U X) = ( {V F K X π 2 (V ) U} F K X ), ϕ u (U X) = ( {V F K X π 2 (V ) U } F K X ), ϕ α α (U X) = ( (ϕ α U ϕ α U) F K X ), ϕ α α (U X) = ( (ϕ α U ϕ α U) F K X ). (7) In the above, π 1 and π 2 denote the projections from F K X = P(AP) PX. Then it is easily seen by induction that νϕ α c in Definition 2.3 coincides with the conventional interpretation [νu.α] c described in Section 1.1. In fact, the predicate liftings ϕ α in Equation (7) 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 toposes Sub() works for the subobject fibration of any topos. Therefore, the categorical definition of coinductive predicates (Definition 2.3) allows us to interpret the language Rν in constructive underlying logics. Suitable completeness of ensures that a final (c ϕ)-coalgebra in Definition 2.3 exists. Proposition 2.5. Let ϕ be a predicate lifting of F along P p ; X c FX be a coalgebra in ; andp P X. We have P νϕ c if and only if there exists a ϕ-invariant Q such that P Q. The proposition is trivial but potentially useful. It says that an invariant can be used as a witness for a coinductive predicate. This is how bisimilarity is commonly established
oinductive predicates and final sequences in a fibration 569 (namely by finding a bisimulation); and it can be used e.g. in Abramsky and Winschel (2015, Section 6) as an alternative to the metric coinduction principle used there. 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 same functor F. Different predicate liftings correspond to different modalities (such as vs. for the same functor P). This view of predicate liftings is also the current paper s concern (see Example 2.4). In contrast, in fibrational studies like Hermida (1993), Hermida and Jacobs (1998), Fumex et al. (2011) and Atkey et al. (2012), use of predicate liftings has focussed on the validity of the (co)induction proof principle. For such purposes, it is necessary to choose a predicate lifting ϕ that is comprehensive enough, covering all the possible F-behaviours. 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 Jacobs (2010). 3. Final sequences in a fibration Here, we present our main technical result (Theorem 3.9). It generalizes known behavioural ω-bounds (like Hennessy and Milner (1985, Theorem 2.1); see Section 1.1); and claims that the chain (2) for a coinductive predicate stabilizes after ω steps, assuming that the behaviour type functor F and the underlying logic P p are finitary in a suitable sense (but no size restriction on ϕ). 3.1. Size restrictions on a fibration We axiomatize finitariness conditions in the language of locally presentable categories (see Appendix B for a minimal introduction). Singling out these conditions lies at the heart of our technical contribution. Definition 3.1 (LFP category). Acategory is LFP if it is cocomplete and it has a (small) set F of finitely presentable (FP) objects such that every object is a filtered colimit of objects in F. Definition 3.2 (Finitely determined fibration). A (poset) fibration P p is finitely determined if it satisfies the following: 1. is LFP, with a set F of FP objects (as in Definition 3.1). 2. P p has fibrewise limits and colimits (as in Definition.9). 3. For arbitrary X, let(x I ) be the canonical diagram for X with respect to F κ I (i.e. I = F/X, see Lemma B.4), with a colimiting cocone (X I X). Then for any To be precise, only if we take PE in Abramsky and Winschel (2015) that is in fact, a least fixed-point specification as an atomic proposition (and that is essentially what is done in the proofs in Abramsky and Winschel (2015, Section 6)). Our future work on nested μ s and ν s will more adequately address the situation.
I. Hasuo, T. Kataoka and K. ho 570 P,Q P X, P Q κ IP κ IQ in P XI for each I I. The intuition behind ond. 3 is that a predicate P P X (over arbitrary X ) is determined by its restrictions (κ I P ) to FP objects X I. One convenient sufficient condition for ond. 3 is that the total category P is itself LFP, with its FP objects residing above the FP objects in (orollary 6.2). We note that ond. 1 guarantees, since LFP implies completeness, that an (ω op -)limit F ω 1 of the final F-sequence (4) exists. However, this does not mean (nor do we need) that F ω 1 carries a final F-coalgebra; it fails for F = P ω, see Worrell (2005). Definition 3.3 (Well-founded fibration). A well-founded fibration is a finitely determined fibration that further satisfies the following: 4. If X F (hence FP), the fibre P X is such that: the category P op X consists solely of FP objects. Since P X is complete, this is equivalent to: there is no (ω op -)chain P 0 >P 1 > in P X that is strictly descending. We note that the following stronger variant of the condition 3.3 rarely holds: 3.3 :Forany X, there is no strictly descending ω op -chain in P X (it fails in Pred ). The original ond. 3.3 holds in many examples (as we will see later Sets in Section 7), thanks to the restriction that X is FP. Remark 3.4. onditions 3 3.3 mention a fixed set F of FP objects. It is not hard to see that this is not necessary, and we can take as F the set of all FP objects without loss of generality. (Stating the conditions in terms of F is an advantage when it comes to checking them, though.) Let us first note that, by Adámek and Rosický (1994, Remark 1.9), any FP object Y is a split quotient of some X F, i.e. there exists q : X Y and i: Y X with q i = id Y. Then we indeed have the following. On ond. 3, for an FP object Y and κ : Y X, take X F with a splitting X q i Y X.ThenwecantakeI such that X I = X and κ I = κ q. Hence, κ I P κ I Q in P X I induces κ P κ Q in P Y because κ = κ I i. On ond. 3.3, for an FP object Y,takeX F with a splitting X q Y i X. Then a strictly decreasing chain Q 0 >Q 1 > in P Y induces a strictly decreasing chain q Q 0 >q Q 1 > in P X. Here, the strictness of the latter is by i q Q n = Q n. The following trivial fact is written down for the record. Lemma 3.5. A finitely determined fibration P p is well-founded if P X is a finite category for each X F.
oinductive predicates and final sequences in a fibration 571 Fig. 1. Final sequences in a fibration. P ϕ ω 1 1 ϕ 1 ϕ i 1 ϕ ω+1 1 F ω 1 π i 1! F1 F i 1! F i F 1 i! Fπ i 1 F ω+1 1 b b 3.2. Final sequences in a fibration The following result from Jacobs (1999, Proposition 9.2.1) is crucial in our development. Lemma 3.6. Let P p be a fibration, with being complete. Then p has fibrewise limits if and only if P is complete and p: P preserves limits. If this is the case, a limit of a small diagram (P I ) in P can be given by (πi P I ) over Lim X I. π I Here, X I := pp I ;(Lim X I XI ) is a limiting cone in ; and denotes the the inf in the fibre P LimI X I.Moreover, (π I P I) is a limit of the diagram of shape I, namely πi P I πj P J holds for any I J in I. Figure 1 presents two sequences. Here, we assume that P p is finitely determined (Definition 3.2) and that ϕ is a predicate lifting of F. In the bottom diagram (in ), the object 1 is a final one (it exists since LFP implies completeness); F1! 1isthe unique map; F ω+1 1:=F(F ω 1); and b is a unique mediating arrow to the limit F ω 1. In the top diagram (in P), the object 1 is the final object in the fibre P 1 ; by Lemma 3.6, 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 Lemma 3.6; and moreover, it can be chosen above F ω 1. We define ϕ ω+1 1 := ϕ(ϕ ω 1 ). Lemma 3.7 (Key lemma). Let P p be a well-founded fibration; F : be finitary; and ϕ be a predicate lifting of F. Then the final ϕ-sequence stabilizes after ω steps (modulo reindexing via b). Precisely, in Figure 1, we have ϕ ω+1 1 = b (ϕ ω 1 ). Proof. We proceed by steps. Step a. We observe that, in Figure 1, the top diagram is carried to the one below by the functor p: P. This is straightforward: The arrow ϕ 1 1 must be carried to the unique arrow!: F1 1; on the mediating arrow b in P, since pb is again a mediating arrow in, it must coincide with b.
I. Hasuo, T. Kataoka and K. ho 572 Step b. Before moving on, we observe that ond. 3 in Definition 3.2 yields a seemingly stronger statement (ond. 3 below). Sublemma 3.8. For a finitely determined fibration P p the following holds: 3 Let X ; P,Q P X ; and (Y J ) J J be an arbitrary filtered diagram in such that γ J olim J Y J = X, with a colimiting cocone (Y J X)J J. Then P Q if and only if for each J J, γj P γ J Q in P Y J. Proof. (Of Sublemma 3.8) The only non-trivial statement is the if part of the direction 3 3. It suffices to show that γj P γ J Q (for each J J) implies κ I P κ IQ (for each I I), where κ I and I are as in ond. 3. Let I I. Since X I is FP, an arrow κ I : X I X to a filtered colimit X = olim J Y J γ JI factors through some Y JI X, as in the diagram below. κ I X I X = olim J Y J h I Y JI γ JI Now, we have κ I P = h I γ J I P h I γ J I Q = κ IQ, where the inequality is by the assumption that γj P γ JQ for each J J. This proves Sublemma 3.8. Step c. By Step a, weseethatϕ ω+1 1 b (ϕ ω 1 ) by the universality of a artesian arrow. In what follows we shall prove its converse: b (ϕ ω 1 ) ϕ ω+1 1 in P F ω+1 1. (8) Let us take a filtered diagram (X I ) in such that X I F (for each I I) and F ω κ I 1=olim X I,with(X I F ω 1) being the colimiting cocone. Then we have F ω+1 1=F(olim X I )=olim FX I, Fκ I by the assumption that F is finitary; moreover, (FX I F ω+1 1) is a colimiting cocone. The diagram (X I ) is filtered, and so is the latter diagram (FX I ). Thus, by ond. 3 in Sublemma 3.8, showing the following proves Equation (8): (Fκ I ) ( b (ϕ ω 1 ) ) (Fκ I ) (ϕ ω+1 1 ) for each I I. (9) Step d. To prove Equation (9), we first prove the following fact: For each I I, there exists i I ω such that κ I(ϕ ω 1 )=κ I( π ii (ϕ i I 1 ) ) in P XI. (10) That is, the final sequence in P (Figure 1), when restricted to X I (that is FP), stabilizes within finitely many steps. Indeed, by Lemma 3.6, the ω op -limit ϕ ω 1 is described as an ω op -limit (i.e. an inf of a descending sequence) in P F ω 1: ϕ ω 1 = i ω π i (ϕ i 1 ). (11) Therefore, we have κ I (ϕω 1 )= i ω κ I π i (ϕi 1 ) since reindexing κ I preserves fibrewise limits. Here, the sequence ( κ I π i (ϕi 1 ) ) i ω in P X I is also descending. Therefore, by p
oinductive predicates and final sequences in a fibration 573 being a well-founded fibration (Definition 3.3) and X I being FP, there exists i I ω at which the descending sequence ( κ I π i (ϕi 1 ) ) i ω in P X I stabilizes, that is, κ ( I πi (ϕ i 1 ) ) = κ Iπi (ϕ i 1 )=κ I( π ii (ϕ i I 1 ) ) in P XI. i ω i ω ombined with Equation (11), this proves Equation (10). Step e. Finally, let us prove Equation (9). For each I I, (Fκ I ) ( b (ϕ ω 1 ) ) =(Fκ I ) ( b ( πi (ϕ i 1 ) )) by Equation (11) i ω = (Fκ I ) ( b ( πi (ϕ i 1 ) )) reindexing preserves i ω j ω(fκ I ) ( b ( π j+1(ϕ j+1 1 ) )) letting i = j +1fori 1 = j ω(fκ I ) ( (Fπ j ) (ϕ j+1 1 ) ) by π j+1 b = Fπ j (see Figure 1) = ϕ ( κ Iπj (ϕ j 1 ) ) by Definition 2.2 j ω ϕ ( κ Iπi I (ϕ i I 1 ) ) letting j = i I on the LHS = ϕ ( κ I(ϕ ω 1 ) ) by Equation (10) =(Fκ I ) (ϕ ω+1 1 ) by Definition 2.2 and ϕ ω+1 1 = ϕ(ϕ ω 1 ). This proves Equation (9) and concludes the proof of Lemma 3.7. The object ϕ ω 1 is a prototype of ϕ-coinductive predicates in various coalgebras. This is part of the main theorem below. It is standard that a coalgebra X c FX in induces a cone over the final F-sequence, and hence a mediating arrow X F ω 1 (see below). oncretely, c i : X F i 1 is defined inductively by X c 0 1is!;andc i+1 is the composite X c FX Fc i F i+1 1. The induced arrow to the limit F ω 1 is denoted by c ω. F ω 1 π i 1! F1 F i 1 c i X Note that F ω 1 does not necessarily carry a final F-coalgebra (see Remark 3.12). c ω (12) Theorem 3.9 (Main result). Let P p be a well-founded fibration; F : be a finitary functor; ϕ be a predicate lifting of F along p; andx c FX be a coalgebra in. 1. The ϕ-coinductive predicate νϕ c in c (Definition 2.3) exists. It is obtained by the following reindexing of ϕ ω 1,wherec ω is the mediating map in Equation (12). νϕ c = c ω(ϕ ω 1 ). (13)
I. Hasuo, T. Kataoka and K. ho 574 2. Moreover, the predicate νϕ c is the limit of the following ω op -chain in the fibre P X X (c ϕ)( X ) (c ϕ) 2 ( X ), (14) that stabilizes after ω steps. That is, νϕ c = i ω (c ϕ) i ( X ). Proof. We proceed by steps. Step a. We first show that the descriptions of νϕ c in the items 1 2 are the same: c ω(ϕ ω 1 )= i ω(c ϕ) i ( X ). (15) We have ( c ω(ϕ ω 1 )=c ω πi (ϕ i 1 ) ) by Lemma 3.6 i ω = c ( ω π i (ϕ i 1 ) ) since reindexing preserves i ω = i ω c i (ϕ i 1 ) by the definition of c ω. (16) Furthermore, c i (ϕi 1 ) in the above is seen to be equal to (c ϕ) i ( X ). This is shown by induction on i ω. Fori = 0, the claim amounts to! ( 1 )= X, which holds since reindexing preserves. For the step case, c i+1(ϕ i+1 1 )=c (Fc i ) (ϕ i+1 1 ) by c i+1 = Fc i c = c ( ϕ ( c i (ϕ i 1 ) )) by Definition 2.2 =(c ϕ) ( (c ϕ) i ( X ) ) by induction hypothesis. Therefore the Equation (15) holds. Step b. In order to show that i ω (c ϕ) i ( X )istheϕ-coinductive predicate in c, we shall exhibit that the chain (14) the final (c ϕ)-sequence in P X stabilizes after ω steps. By Equation (15), the claim (c ϕ) ( i ω (c ϕ) i ( X ) ) = i ω (c ϕ) i ( X ) reduces to (c ϕ) ( c ω(ϕ ω 1 ) ) = c ω(ϕ ω 1 ). (17) Step c. Finally, we shall prove Equation (17): c ( ϕ(c ω(ϕ ω 1 )) ) = c ( (Fc ω ) (ϕ(ϕ ω 1 )) ) by Definition 2.2 = c ( (Fc ω ) (b (ϕ ω 1 )) ) by Lemma 3.7 =(b Fc ω c) (ϕ ω (18) 1 ) = c ω(ϕ ω 1 ). For the last equality, we used b Fc ω c = c ω, which is proved by showing that b Fc ω c is also a mediating map in Equation (12). Indeed, for each i 1, This concludes the proof. π i b Fc ω c = Fπ i 1 Fc ω c see Figure 1 = Fc i 1 c by Equation (12) = c i by the definition of c i.
oinductive predicates and final sequences in a fibration 575 Example 3.10 (Rν). We shall continue Example 2.4 and derive from Theorem 3.9 the behavioural bound result described in Section 1.1: the chain (2) stabilizes after ω steps, for each α Rν u and each finitely branching Kripke model c. Indeed, the latter is the same thing as a coalgebra X c F fbk X,whereF fbk = P(AP) P ω ( ). ompared to F K in Example 2.4, the powerset functor is restricted from P to P ω ; this makes F fbk a finitary functor. Still the same definition of ϕ α defines a predicate lifting of F fbk. Theorem 3.9.2 can then be applied to the fibration Pred (easily seen to be Sets well-founded, Example 7.1), the finitary functor F fbk and the predicate lifting ϕ α for each α. It is not hard to see that the function [α] c : PX PX in Section 1.1 coincides with c ϕ α : Pred X Pred X (note that Pred X = 2 X = PX); thus the chain (2) coincides with Equation (14) that stabilizes after ω steps by Theorem 3.9. Remark 3.11. The ω-bound of the length of the chain (14) is sharp. A (counter)example is given in the setting of Example 3.10, by the predicate lifting ϕ u and the coalgebra (i.e. Kripke structure) c 2 below. There b i,i has no successors. Indeed, while νϕ u c2 is {a i i ω}, itsith approximant ((c 2 ) i ϕ i u)( X ) in Equation (14) contains b i,0 too. c 2 a 0 b 0,0 a 1 b 1,0 b 1,1 a 2 b 2,0 b 2,1 b 2,2. Remark 3.12. It is notable that Theorem 3.9 imposes no size restrictions on ϕ: P P. Being a predicate lifting is enough. To find an example such that ϕ is not finitary is future work. Our main theorem would not become trivial even if it turns out that ϕ is always finitary. 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 Worrell (2005, Section 5)). One obtains a final coalgebra either by (1) quotienting F ω 1 by the behavioural equivalence (see e.g. Pattinson (2003)); or (2) continuing the final sequence till ω + ω steps. The latter construction is worked out
I. Hasuo, T. Kataoka and K. ho 576 in Worrell (2005) (in Sets) and in Adámek (2003) in LFP with additional assumptions. Its relevance to the current work is yet to be investigated. We emphasize that a final ϕ-sequence stabilizes in ω steps relatively to the underlying final F-sequence. In fact, we can also show that the final ϕ-sequence absolutely stabilizes in ω + ω steps for some LFP including Sets; a proof can be done by observing that the final ϕ-sequence stabilizes as soon as the final F-sequence stabilizes, once we are beyond ω steps. To show directly the stabilization of the final ϕ-sequence in ω + ω steps, one may want to prove that P is strongly LFP as in Adámek (2003) and that ϕ is finitary. Neither of these seems easy. oalgebra morphisms are compatible with coinductive predicates. This fact, like Proposition 2.5, is potentially useful in establishing coinductive predicates. Proposition 3.13. Let f : X Y be a coalgebra morphism from X c FX to Y d FY. In the setting of Lemma 3.7 and Theorem 3.9: 1. If Q P Y is a ϕ-invariant in d, soisf Q P X in c. 2. We have νϕ c = f ( ) νϕ d. Proof. For the item 1, f Q f d (ϕq) Q is an invariant = c (Ff) (ϕq) f is a homomorphism = (c ϕ)(f Q) by Definition 2.2. For the item 2, the coalgebras give rise to mediating arrows X c ω F ω 1andY d ω F ω 1, respectively, as in Equation (12). It is easy to see that c ω = d ω f (using the universality of the limit F ω 1); using Equation (13) the claim follows. Remark 3.14. The current paper focusses on FP objects, finitary functors, etc. i.e. the ω-presentable setting (see Adámek and Rosický (1994, Section 1.B)). This is for the simplicity of presentation: the results, as usual (as e.g. in Klin (2007)), can be easily generalized to the λ-presentable setting for an arbitrary regular cardinal λ. In such an extended setting, we obtain a behavioural λ-bound. 4. A fibration of invariants We organize the above observations in a more abstract fibred setting. The technical results are mostly standard; see e.g. Hermida (1993), Hermida and Jacobs (1998) and Jacobs (2012, hap.6). We write oalg(f) for the category of F-coalgebras. Proposition 4.1. Let ϕ be a predicate lifting of F along P p. Then the fibration P p is lifted oalg(ϕ) to a fibration p, with two forgetful functors forming a map of fibrations from the oalg(f) latter to the former.
oinductive predicates and final sequences in a fibration 577 Proof. It is easy to check each fibre oalg(ϕ) c is a poset. Let (X X c FX) f (Y FX FY )beanarrowinoalg(f), and P s ϕp be above Y d FY. A artesian lifting of f is obtained as in the following diagram: P ϕf P ϕf(p ) ϕp t s f P P f(p ) d FX c X Ff f FY Y d Here, we used the universality of the artesian lifting ϕf(p ) (see Definition 2.2). The two forgetful functors constitute a map of fibrations: The commutativity (5) is oalg(ϕ) obvious, and artesian liftings in p (which we constructed above) are based on the oalg(f) artesian liftings in P p. The next observation explains the current section s title. oalg(ϕ) Proposition 4.2. Let p be the lifted fibration in Proposition 4.1. For each coalgebra oalg(f) X c FX, the fibre over c coincides with the poset of ϕ-invariants in c. Thatis, = oalg(ϕ) c X oalg(c ϕ) FX. P X Proof. Given a ϕ-coalgebra P s ϕp above X c FX, we use the universality of the artesian lifting of c to obtain a (c ϕ)-coalgebra as in the following diagram: c (ϕp ) c(ϕp ) ϕp s P onversely, given a (c ϕ)-coalgebra Q X c FX as the following composite: t c (ϕq), we obtain a ϕ-coalgebra above c (ϕq) c(ϕq) ϕq t Q Then it is straightforward to see that the mappings are monotone and inverse to each other. The mappings commute with the forgetful functors since they do not change the carriers.
I. Hasuo, T. Kataoka and K. ho 578 oalg(ϕ) Therefore, Theorem 3.9.1 and Proposition 3.13.2 state the fibration p has fibrewise oalg(f) final objects. (At least part of) this statement itself is shown quite easily using the Knaster Tarski theorem (each fibre is a complete lattice). Our contribution is their concrete construction as ω op -limits (Theorem 3.9.2). The following lemma is essentially a special case of Lemma 3.6, but see also Jacobs (1999, Proposition 9.2.1 and Exercise 9.2.4). Lemma 4.3. Let P p be a fibration; and assume that has a final object. Then P p has a fibrewise final object if and only if P has a final object that is above the final object of. oalg(ϕ) By applying the lemma to p, we obtain a basic relationship between coinductive oalg(f) predicates and final coalgebras. orollary 4.4. Let ϕ be a predicate lifting of F along P p; and assume that a final F-coalgebra exists. The following are equivalent: 1. The coinductive predicate νϕ c exists for each coalgebra c: X FX. Moreover, they are preserved by reindexing (along coalgebra morphisms). 2. There exists a final ϕ-coalgebra that is above the final F-coalgebra. As noted in Remark 3.12, however, our concrete construction of coinductive predicates does not rely on a final F-coalgebra. 5. Inductive predicates over coinductive datatypes The central topic of the current paper is coinductive predicates over coinductive datatypes, the latter identified as coalgebras in the base category of a fibration P p. Some variations are possible, namely: inductive/coinductive predicates over inductive/coinductive datatypes. For example, Hermida and Jacobs (1998) focus on: inductive predicates over inductive datatypes (the latter identified as algebras); and coinductive predicates over coinductive datatypes (as we have done in the previous sections). It turns out that, among these four variations, inductive predicates over coinductive datatypes allow a straightforward adaptation of our current categorical framework by P (op) taking the fibrewise opposite p (op) of the fibration P p we are interested in. We present these results in the current section. The study of the other two variations inductive predicates over inductive datatypes, and coinductive predicates over inductive datatypes is left as future work. In fact, we have preliminary observations that under certain assumptions these two variations coincide. Their details will be presented in another venue. The following is the definition of an inductive predicate (on a coinductive datatype). It is not hard to see that the definition generalizes e.g. the semantics of the μ operator of the modal μ-calculus in a Kripke model. Later in Lemma 5.4, we will identify it as a coinductive predicate in the fibrewise opposite.
oinductive predicates and final sequences in a fibration 579 Definition 5.1 (Inductive predicate). Let ϕ be a predicate lifting along a fibration P p ;and X c FX be a coalgebra in. Theϕ-inductive predicate in c is the initial (c ϕ)-algebra (if it exists). We denote its carrier by μϕ c. Hence, it is the smallest predicate P P X such that P c (ϕp )inp X. P (op) In what follows we utilize the notion of fibrewise opposite p (op) of a fibration P p (Bénabou (1975); see also (Jacobs 1999, Definition 1.10.11)). Intuitively, the fibrewise opposite p (op) is obtained by opposing the order in each fibre P X but leaving the base category, as well as the reindexing structure, as in the original fibration p. The precise definition is best stated via indexed categories and the Grothendieck construction. It is left to the appendix (Lemma.13). P (op) Some remarks are in order. First, the total category P (op) of the fibrewise opposite p (op) is in general different from the opposite category P op (in the usual sense) of P. The same applies to the functor p (op), that is different from the opposite functor p op. We emphasize P (op) p (op) that in the fibrewise opposite P (op) p (op), the base category stays the same. We also note that is a fibration, unlike the opposite functor P op p op of p that is canonically an opfibration. op Notation 5.2. For distinction, we denote reindexing functors in fibrations P P (op) p and p (op) by f and f #, respectively. They are in fact the same monotone functions between fibres as posets: (P (op) ) Y f # (P (op) ) X (P Y ) op (f ) op (PX ) op for f : X Y. The following result, although straightforward, is essential for the subsequent technical development. Lemma 5.3. Let P p be a fibration and F be an endofunctor on. For a predicate lifting ϕ: P P of F along p, there exists a canonical predicate lifting ϕ (op) : P (op) P (op), P (op) which we call the fibrewise opposite of ϕ, off along the fibration p (op). Proof. We give an explicit construction here, although the statement is almost trivial when stated in terms of indexed categories. On objects, we define ϕ (op) P = ϕp. For the action on arrows, we first note that an arrow P Q in P (op) above f : X Y exists if and only if P f # Q in (P (op) ) X =(P X ) op. Exploiting this fact, ϕ (op) s action on the arrow P Q is defined to be the unique arrow ϕ (op) P ϕ (op) Q above Ff: FX FY. The last (unique) arrow exists, indeed: We have ϕ (op) P (Ff) # ϕ (op) Q in (P (op) ) FX by ϕp ϕf Q =(Ff) ϕq in P FX. Here, the last equality is because ϕ is a predicate lifting.
I. Hasuo, T. Kataoka and K. ho 580 Lemma 5.4. Let P be a predicate over X. 1. The object P P X carries a (c ϕ)-algebra if and only if P (P X ) op =(P (op) ) X is a ϕ (op) -invariant in c. 2. The ϕ-inductive predicate in c is the ϕ (op) -coinductive predicate in c. Thatis,μϕ c = ν(ϕ (op) ) c as objects in P X. Proof. The category of (c ϕ)-algebras in P X is dually equivalent to the category of (c # ϕ (op) )-coalgebras in (P (op) ) X, since the following diagram (in Posets) commutes. (P (op) ) X (ϕ (op) ) X (P (op) ) FX c # (P (op) ) X (P X ) op ϕ op X (P FX ) op (c ) op (P X ) op Thanks to the previous characterization inductive predicates in P p as coinductive ones P (op) in p (op) we can apply all the results that we have obtained so far to inductive predicates. Notice again that the base category has remained the same. The characterization in Lemma 5.4 can be seen as a generalization of the duality μu. ϕ(u) = νu. ϕ( u) between least and greatest fixed points in classical logics the latter is a special case where fibres are self-dual, i.e. P P (op) p = p (op). Via the last characterization, our main result (Theorem 3.9) can also be used to show the stabilization of the ω-chain when calculating inductive predicates (see orollary 5.8). The inductive predicate on F ω 1 is not a limit nor a colimit in P, but it is a limit in P (op) (see Definition 5.7). Definition 5.5 (o-well-founded fibration). A co-well-founded fibration is a finitely determined fibration that further satisfies: 3.3. If X F (hence FP), the fibre P X is such that: the category P X consists solely of FP objects. Since P X is cocomplete, this is equivalent to: there is no (ω-)chain P 0 <P 1 < in P X that is strictly ascending. Lemma 5.6. For a finitely determined fibration P P (op) p, its fibrewise opposite p (op) is also finitely determined. Moreover, p (op) is well-founded if and only if the fibration p is cowell-founded. Proof. It is trivial that the fibration p (op) satisfies the condition 1 (of Definition 3.2) if and only if p satisfies it. For the condition 2, p (op) has fibrewise limits and colimits, because p has fibrewise colimits and limits, respectively. The condition 3 for p (op) is obviously equivalent to the one for p since reindexing functors κ I,κ# I are the same as functions. By (P (op) ) X =(P X ) op, p (op) satisfies the condition 3.3 if and only if p satisfies 3.3.
oinductive predicates and final sequences in a fibration 581 Definition 5.7. Let 1 be the least element of the fibre P 1 (hence the greatest in (P (op) ) 1 ). We denote by ϕ ω 1 P F ω 1 the limit of the following diagram in P (op). It is easily seen to reside above the final F-sequence in. 1 ϕ 1 ϕ i 1 in P (op) Note here that 1 is the final object in P (op), and the object ϕ 1 is the functor ϕ (op) applied to 1. Therefore, the above diagram is the final ϕ (op) -sequence in P (op). Using Lemma 3.6, it is not hard to see that ϕ ω 1 = i ω π i (ϕi 1 ) in the fibration P p, where (π i : F ω 1 F i 1) i ω is the limiting cone for the final F-sequence in. The following is our main result adapted to inductive predicates. In particular, it states that an inductive predicate is computed as a supremum of an ω-chain. orollary 5.8. Let P p be a co-well-founded fibration; F : be a finitary functor; ϕ be a predicate lifting of F along p; andx c FX be a coalgebra in. 1. The ϕ-inductive predicate μϕ c in c exists. It is obtained by the following reindexing of ϕ ω 1,wherec ω is the mediating map in Equation (12). μϕ c = c ω(ϕ ω 1 ) 2. Moreover, the predicate μϕ c is the colimit of the following ω-chain in the fibre P X X (c ϕ)( X ) (c ϕ) 2 ( X ), that stabilizes after ω steps. That is, μϕ c = i ω (c ϕ) i ( X ). Proof. By Lemmas 5.4 and 5.6 and Theorem 3.9. orollary 5.9. Let ϕ be a predicate lifting of F along P (oalg(ϕ(op)))(op) p;and p (op)(op) be the fibrewise oalg(f) P (op) opposite of the lift of the fibration p (op) (see Proposition 4.1 and Lemma 5.3). For each coalgebra X c FX, the following diagram commutes: ( (oalg(ϕ (op) ) ) ) (op) X FX c ((P X ) op ) op = Alg(c ϕ) P X Proof. Apply Proposition 4.2 for the predicate lifting ϕ (op) along oalg(ϕ (op) ) X c FX P (op) p (op) = oalg(c # ϕ (op) ), (P (op) ) X whose opposite categories are the ones in the diagram we want to prove., we obtain
I. Hasuo, T. Kataoka and K. ho 582 oalgebra morphisms are compatible with inductive predicates just as in Proposition 3.13. Therefore, the inductive predicates μϕ c form a fibrewise initial object = μϕ of the fibration p (op)(op). 6. Examples at large Here are several results that ensure a fibration to be finitely determined or well-founded, and hence enable us to apply Theorem 3.9. Some of them are well-known; others especially those which relate fibrations and locally (finitely) presentable categories, including Lemmas 6.3 and 6.7 seem to be new. The following results provide sufficient conditions for a fibration to be finitely determined (Definition 3.2). Recall that a full subcategory F of P is said to be dense if each object P P is a colimit of the canonical diagram F/P π F P. Lemma 6.1. Let P p be a fibration with fibrewise limits and colimits and coproducts between fibres. Assume further that is LFP with a set F of FP objects (as in Definition 3.1). If the total category P has a dense subcategory F P such that every R F P is above F (i.e. pr F ), then p is finitely determined. Proof. The only non-trivial part is the direction of ond. 3. For that, it suffices to show that arbitrary P P is a colimit of the diagram (κ I P ). Here, I and κ I are as in ond. 3. By Lemma.11, the colimit olim κ I P is described as κ I κ I P using a sup in κ I P X, since (X I X) is colimiting. We have κ I κ IP P as a counit of an adjunction; therefore, olim κ I P P. Thus, it suffices to show that P olim κ I P in P X.Let(P J ) J J be a diagram in P g J such that P J F P and there is a colimiting cocone (P J P )J J. Such a diagram exists since F P is dense. By the assumption, for each J, the object P J F P lies above an object in F. Therefore, the arrow pg J : pp J pp = X is an object of F /X; since I = F /X, wecanchoose g J I J I such that κ IJ = pg J. Now an arrow P J P in P induces P J (pg J ) P = κ I J P (19) by the universality of artesian arrows. We proceed as follows: P = olim P ( ) J = ( ) pg J J J P J κ IJ κ I J P κ I κ IP ( ) = olim κ IP. J J J J For ( ), we used Lemma.11; ( ) holds since I J is chosen so that κ IJ = pg J and Equation (19) hold. This concludes the proof. orollary 6.2. Let P p be a fibration with fibrewise limits and colimits and coproducts between fibres, where is LFP with a set F of FP objects (in Definition 3.1). If the total category P is also LFP, with a set F P of FP objects (as in Definition 3.1) chosen so that every R F P is above F, then p is finitely determined.
oinductive predicates and final sequences in a fibration 583 6.1. Subobject fibrations The following is one of the results that are non-trivial. Lemma 6.3. Let be an LFP category with F being a set of FP objects (as in Definition 3.1). Then the total category Sub() of the subobject fibration is LFP: the set F Sub() := {(P X) X F, and there exists a strong epi Z P such that Z F} consists of FP objects in Sub(); and every object (Q Y ) Sub() is a colimit of a filtered diagram in F Sub(). Proof. The proof is by steps. Step a. First, we show that Sub() is complete and cocomplete. We rely on Lemma.11. Sub() We start with fibrewise limits in ; the proof is like in Jacobs (1999, Example 1.8.3(iii)). By Lemma B.6, an LFP category is complete. This equips each fibre Sub(X) with arbitrary inf s computed as wide pullbacks. A reindexing functor (by pullbacks) preserves these inf s since limits commute. Therefore, by Lemma.11, the total category Sub() is complete. Each fibre (which is a poset) has arbitrary inf s; hence, it is a complete lattice and arbitrary sup s also exist. Sub() Next, we show that is a bifibration (Definition.3). An abstract proof can be given by Freyd s adjoint functor theorem (note that each fibre Sub(X) is a complete lattice, and that reindexing f preserves inf s). Instead we explicitly introduce exploiting a factorization structure of LFP (Lemma B.6.2). Namely, given (P m X) Sub(X) and f : X Y, the opreindexing f P is defined by the (StrongEpi, Mono)-factorization of f m, asbelow. P f P m (20) X Y f The fact that f P Q if and only if P f Q is easily proved using the diagonalization property of the factorization structure. This establishes f as a left adjoint to reindexing f. Using Lemma.11, we conclude that Sub() is cocomplete. Step b. Let Im: /Y Sub(Y ) be the image functor defined by the (StrongEpi, Mono)- factorization (i.e. Im f = f X for f : X Y ). In the notation in Lemma B.11.2, we have F Sub() = {Im f X F, f F/X} = {(P X) Sub() X F, P F Sub(X) }. The set F Sub() is small, since F is small and F Sub(X) is small for each X F. Step c. First, we prove that (P m X) F Sub() is FP in Sub(). Opreindexings f f do not have to satisfy the Beck hevalley condition.