Unique Factorisation Lifting Functors and Categories of Processes

Marta Bunge^{∗} Department of Mathematics and Statistics McGill University

Marcelo Fiore^{∗} School of Cognitive and Computing Sciences University of Sussex

October 1998

Introduction

This work is an investigation into the mathematical structure of processes. The processes to be considered embody a notion of state space varying according to a control. This we formalise as a category of states (and their inter-relations) 𝕏 equipped with a control functor

[figure: 𝕏; ℂ; f].

There are different ways in which the control category ℂ may be required to control the state category 𝕏; these depend, of course, on the properties required from the control functor f. For instance, one may require the control functor to be a discrete opfibration or, dually, a discrete fibration. The first requirement corresponds to imposing a determinacy property on the state category [Law86c], as for every state X in 𝕏 and every control path γ : f(X) [figure] C there should exist a unique evolution e : X [figure] Y in 𝕏 along γ (i.e., such that f(e) = γ). The second case corresponds essentially to Winskel’s et al. presheaf models [JNW96, CW97, WN97]. It allows non-determinism but, as we explain in Section 1, imposes a particular notion of state on the state category. The approach adopted here will be to consider a more general notion of control functor; viz., unique factorisation lifting (ufl) functors. Our motivation for doing so comes from computer science where ufl functors can be used to provide a conceptual understanding of certain models for concurrency that have been dealt with in an ad hoc manner (see Sections 1 and 3). For motivations relevant to continuum physics see [Law86b, Law86c].

Intuitively, in a ufl functor [figure: 𝕏; ℂ; f], every evolution e : X [figure] Y in 𝕏 is controlled by ℂ in that

whenever the control path f(e) in ℂ may be performed in two stages (γ_{0}, γ_{1}) (i.e., f(e) = γ_{0} · γ_{1}) then the evolution e uniquely decomposes as two evolutions (e_{0}, e_{1}) (i.e., e = e_{0} · e_{1}) respectively taking place along γ_{0} and γ_{1} (i.e., f(e_{0}) = γ_{0} and f(e_{1}) = γ_{1}).

Thus, a first rough notion of category of processes can be taken to be the category UFL/ℂ, where UFL is the subcategory of Cat of ufl functors. We show in Section 2 that UFL/ℂ may be embedded (as a full reflective subcategory) in a presheaf topos; viz., ℂ̂_{#} where ℂ_{#} is Mac Lane’s twisted arrow category [ML71, page 223]. On the one hand, this result establishes connections with presheaf models; thus opening the possibility of reusing the techniques developed in that setting [CW97]. On the other hand, it highlights important differences. First, the path category ℂ_{#} is obtained from the control category ℂ and this passage equips the former with extra structure; notably notions of cover. Second, presheaf models can be over generous. For instance, by considering all presheaves in ℂ̂_{#} as processes one is doomed to rule out important notions of state (e.g., as in transition systems; see Section 1). This may be overcome by restricting to presheaves in ℂ̂_{#} satisfying certain orthogonality (sheaf) conditions; for these are in bijective correspondence with ufl functors over ℂ (the bijection extracts a state category out of a presheaf). However, this mathematical equivalence should not undermine the fibrational viewpoint provided by ufl functors.

∗Research supported by grants from the Natural Sciences and Engineering Council of Canada and from the Ministere de l’Education du Quebec.

Finally, to establish the categories of processes that will be the subject study of this paper we need analyse the nature of control categories. Various interpretations for them are possible. For example, one may regard control categories as providing time duration for the evolutions of a process; this is the viewpoint adopted in [Law86b, Law86c]. Natural examples under this interpretation are the additive monoid of natural numbers (discrete time) and the additive monoid of non-negative real numbers (continuous time). Another view of control categories is as providing observations (e.g., time passing or actions being performed); this is the interpretation explored here. Our basic example is the free monoid on a set of actions. In particular, when the set of actions is a singleton (containing a “tic”) we obtain the monoid of discrete time. The relevant structure of these and similar examples of control categories is axiomatised as so-called triangulated categories, that we introduce and study in Section 4. Informally, triangulated control categories are those in which any two equal control paths can be linearised (or interleaved) in a canonical fashion; see (18). This property is better defined as the conjunction of a “cancellation” and a “fill-in” property (see Definition 4.1). The cancellation property has been considered by Lawvere in the context of processes in [Law89] and, as argued there, seems to be inherent in the notion of a given evolution of a process. The further imposition of the fill-in property has important mathematical and conceptual consequences. From the mathematical perspective, as shown in Section 4, the cancellation and fill-in properties on a category ℂ are equivalent to an “interval glueing” property used in [BN98] to show that UFL/ℂ is a topos; we will give another proof of this result in Section 5. (We remark that Johnstone showed that for ℂ the commutative square, the simplest example of failure of fill-in, the category UFL/ℂ is not a topos [Joh98].) Conceptually, the consideration of processes over a triangulated control category corresponds to restricting attention to processes that are linearly controlled; that is, to interleaving models, in the jargon of computer science.

Organisation of the paper. We start in Section 1 with background material motivated from the point of view of computer science. In Section 2, the category UFL is defined and its basic properties are studied. Section 3 explores applications of ufl functors to concurrency. In particular we show that they may be used in the study of interleaving models like transition systems. In Section 4, we introduce triangulated categories. Our main use for them is in Section 5 where, for ℂ a triangulated category, we exhibit the category UFL/ℂ as a sheaf topos. These toposes may be regarded as models of linearly-controlled processes. Some concluding remarks are provided in Section 6.

1 Background and motivation

Labelled transition systems are a model of computation widely used in concurrency [WN95]. We recall the basic definitions.

A transition system over a set of actions A consists of a set of states S and a transition relation [figure] ⊆ S × A × S. A tuple (s, a, s′) ∈ [figure] is usually denoted as s [figure: a] s′; its intended meaning is that at the state s the system may perform the action a and, in doing so, evolve to the state s′. The category of transition systems over a set of actions A, denoted TS_{A}, has transition systems over A as objects and morphisms σ : (S, [figure] ) [figure] (S′, [figure]′) where σ : S [figure] S′ is a function such that s [figure: a] s′ implies σ(s) [figure: a] σ(s′).

One is sometimes interested in transition systems with an initial state and morphisms preserving it. This category is obtained as the slice TS_{A}^{•} = ℓ0/TS_{A} where ℓ0 = • is the transition system with one state and no transitions (in this case, loops).

An important subclass of transition systems is that of synchronisation trees [WN95]. Roughly, these are transition systems with a distinguished initial state, with no cycles, and such that

s_{1} [figure: a_{1}] s and s_{2} [figure: a_{2}] s imply s_{1} = s_{2} and a_{1} = a_{2} .  (1)

A conceptual description of the category of synchronisation trees is as certain presheaf models [JNW96, CW97, WN97]. We present this viewpoint next.

For a set A, let P(A) be the poset (A^{∗}, ≤) of finite sequences over A ordered by prefix. The category of synchronisation trees over a set of actions A is ST_{A} = P̃A, where for a small category ℙ with an initial object we write ℙ̃ for the full subcategory of ℙ̂ = [ℙ^{op}, Set] of rooted presheaves. These are presheaves T : ℙ^{op} [figure] Set satisfying either of the following equivalent conditions: for ⊥ an initial object in ℙ,

(R–i) The set T (⊥) is terminal in Set.

(R–ii) There exists a unique map ⊥ [figure]T in ℙ̂ (that is, 0 [figure]⊥ is orthogonal [FK72] to T [figure] 1 in ℙ̂).

In the definition of the category of synchronisation trees, we have implicitly identified the rooted presheaf T : P(A)^{op} [figure] Set with the synchronisation tree with initial state given by the unique element of T (ε); set of states given by ∑_{α∈A^{∗}} T (α); and transition relation given by

(α, s) [figure: a] (α′, s′) iff α′ = α · a and s = T (α ≤ α′)(s′) .

This construction is the well-known Grothendieck construction [MLM94, Bor94] in disguise. The Grothendieck construction applies to presheaf categories over an arbitrary small category ℙ, and provides a fibrational view of ℙ̂ as a full subcategory of Cat/ℙ. It associates a presheaf

T : ℙ^{op} [figure] Set with the functor [figure: ∫ T; ℙ] given by an obvious projection, where the category of

elements ∫ T has set of objects given by ∑_{α∈ℙ} T (α); morphisms (α, s) [figure: a] (α′, s′) given by morphisms a : α [figure] α′ in ℙ such that s = T (a)(s′); and identities and composition given as in ℙ. This mapping extends to an embedding (in fact a coreflection)

ℙ̂ [figure] Cat/ℙ  (2)

whose image consists of so-called discrete fibrations. Moreover, in the presence of the axiom of choice, the embedding (2) cuts down to an equivalence

ℙ̂ ≃ DFib/ℙ  (3)

where DFib denotes the subcategory of Cat of discrete fibrations. Recall that a functor [figure: 𝕋; ℙ; t]

is called a discrete fibration if every commutative square

(DF) \xymatrix{1 \ar[r] \ar[d]_{(1)} & 𝕋 \ar[d]^{t} \\ 2 \ar[r] \ar@{.>}[ur]^{∃!} & ℙ}

has a unique fill-in as indicated (that is, if (1) : 1 [figure] 2 is orthogonal to t : 𝕋 [figure] ℙ in Cat). Dually, a functor is a discrete opfibration if (0) : 1 [figure] 2 is orthogonal to it.

In elementary terms, the condition (DF) says that in the situation

\xymatrix{ & s′ \ar@{|->}[d]^{t} \\ α \ar[r]_{a} & α′}  (4)

there exists a unique morphism s [figure] s′ in 𝕋 such that

[figure: s; t; s′; α; α′; .]  (5)

The equivalence (3) associates to a discrete fibration [figure: 𝕋; ℙ; t]the presheaf T : ℙ^{op} [figure] Set where

T (α) = { s ∈ 𝕋_{0} | t(s) = α } and, for a : α [figure] α′ in ℙ, the function T (a) : T (α′) [figure] T (α) maps an s′ as in (4) to the unique s as in (5).

Observe that from the fibrational perspective the rootness conditions (R) above can be expressed as a unique lifting property. Indeed, for a small category ℙ with an initial object ⊥, we have the equivalence

ℙ̃ ≃ DFib_{0}/ℙ

where DFib_{0} is the full subcategory of DFib consisting of discrete fibrations [figure: 𝕋; ℙ; t]such that

(⊥) : 1 [figure] ℙ has a unique lifting along t as follows

\xymatrix{ & 𝕋 \ar[d]^{t} \\ 1 \ar[r]_{(⊥)} \ar@{.>}[ur]^{∃!} & ℙ & .}  (6)

Since t is a discrete fibration, the object provided by the lifting 1 [figure] 𝕋 of (6) is initial in 𝕋; hence t creates initial objects.

Following the work on presheaf models, the category DFib/ℙ may be regarded as a cate-

gory of processes over the category of computation paths ℙ. Indeed, a (discrete) fibration [figure: 𝕋; ℙ; t]

embodies a category of states and transitions (the objects and morphisms of 𝕋) varying along observations (the morphisms of ℙ) as specified by the labelling functor t. More concretely, a morphism s [figure: e] s′ in 𝕋 witnesses the capability of the system to evolve from the state s to the state s′ producing the observable behaviour t(e) [WN97]. In this light, the condition (DF) has the following computational interpretation: a state s′ occurring after an observation a, as indicated in (4) above, comes from a unique state s and transition s [figure] s′ along which a is observed. Notice that for discrete fibrations (equivalently presheaves) the notion of state captured by this interpretation is that of the computation state associated to the behaviour of a system, as opposite to the states in which a system can be. Indeed, we have the following property

for s_{1} [figure: e_{1}] s and s_{2} [figure: e_{2}] s, if t(e_{1}) = t(e_{2}) then s_{1} = s_{2} and e_{1} = e_{2}

analogous to property (1) of synchronisation trees.

We will show below that, by broadening the notion of fibration, one can develop a theory for transition systems with a treatment of bisimulation via open-maps [JNW96] in the same spirit of Winskel’s et al. presheaf models. The required fibration condition amounts to a unique factorisation lifting property [Law86b, Str96, BN98]. We illustrate this concept in the context of transition systems.

Let (S, [figure] ) be an A-labelled transition system and let F(S, [figure] ) be the free category on its underlying graph (that is, its reflexive-transitive closure). Explicitly, the small category F(S, [figure] ) has set of objects given by S; morphisms s [figure]s′ given by finite paths (or runs, or histories) [s [figure: a_{1}] s_{1} [figure] ⋯ [figure: a_{n}] s′] of the system; identities given by the empty paths [s]; and composition given by concatenation of paths. Thus, writing M(A) for the free monoid on A,

we obtain a projection functor ^{F(S, [figure] )}_{M(A)} [figure] mapping a path [s [figure: a_{1}] s_{1} [figure] ⋯ [figure: a_{n}] s′] to the sequence

of actions a_{1} ⋯ a_{n} performed along it. The functors [figure: 𝕋; M(A)] so obtained satisfy the following

fibrational unique factorisation lifting (ufl) condition: every commutative square

(UFL) \xymatrix{2 \ar[r] \ar[d]_{(0,2)} & 𝕋 \ar[d] \\ 3 \ar[r] \ar@{.>}[ur]^{∃!} & M(A)}

has a unique fill-in as indicated (that is, (0, 2) : 2 [figure] 3 is orthogonal to 𝕋 [figure] M(A) in Cat). Notice that both discrete fibrations and discrete opfibrations have the (UFL) property.

In Section 3, the category

UFL/M(A) ,

where UFL [BN98] denotes the subcategory of Cat consisting of ufl functors (see Definition 2.1), will be studied as the category of models of computation given by transition graphs.

2 Unique factorisation lifting functors

We introduce unique factorisation lifting (ufl) functors [Law86b, Str96, BN98] and study their basic properties.

Definition 2.1 A ufl functor is a functor 𝕏 [figure] 𝔹 satisfying the following fibrational unique factorisation lifting condition: every commutative square

(UFL) \xymatrix{2 \ar[r] \ar[d]_{(0,2)} & 𝕏 \ar[d] \\ 3 \ar[r] \ar@{.>}[ur]^{∃!} & 𝔹}

has a unique fill-in as indicated.

In elementary terms, the condition (UFL) says that in the situation

[figure: A; C; a; c; b]

there exists unique A [figure] B and B [figure] C such that

[figure: A; C; B; a; c; b; .]

As can be easily shown, ufl functors reflect identities.

Lemma 2.2 For a ufl functor f, if f(x) = id then x = id.

Since ufl functors are closed under identities and composition, they form a subcategory of Cat, which we denote UFL. Moreover, since whenever 𝕏 [figure] 𝕐 [figure] 𝔹 and 𝕐 [figure] 𝔹 are ufl functors then so is 𝕏 [figure] 𝕐, we have that UFL/𝔹 is a full subcategory of Cat/𝔹.

We consider some examples.

Example 2.3 1. Discrete fibrations and discrete opfibrations are ufl functors.

2. The difference functor Δ_{A} : P(A) [figure] M(A) mapping (α ≤ α · α′) to α′ is a ufl functor.

In particular, for A = 1, we obtain the usual difference functor (m ≤ n) [figure] n − m from ω = P(1), the poset of natural numbers, to N = M(1), the additive monoid of natural numbers.

3. We let Graph [Law86a, Law89] be the presheaf category of graphs Ĝ where G^{op} = N [figure] E , and we write F for the left adjoint to the forgetful functor Cat [figure] Graph :

ℂ [figure] (ℂ_{0} [figure: dom; cod] ℂ_{1}) providing the free category on a graph.

Consider the following loop construction ℓ defined by the adjoint situation below

[figure: 1; (E); Set; (E)_{∗}=ℓ; ⊣; G; Graph; (E)^{∗}; .]

Explicitly, for a set A, the graph ℓA is given by (1 [figure] A).

We have that ℓ1 is the terminal graph and that F(ℓ1) ≅ N. Moreover, for a graph G, the unique graph homomorphism G [figure] ℓ1 induces a length functor FG [figure] N which is a ufl functor [Str96].

More generally, for a set A, we have that F(ℓA) ≅ M(A) and that a graph G together with a labelling homomorphism G [figure] ℓA induces a ufl functor FG [figure] M(A).

The rest of the section is devoted to the study of the slice categories UFL/𝔹. These we characterise as certain full subcategories of a presheaf category by means of orthogonality conditions (Lemma 2.7). Since the representables are ufl functors, we obtain a Yoneda embedding for UFL/𝔹.

The needed category of representables is MacLane’s “twisted arrow category” [ML71, page 223] of the base category. We recall the construction.

Definition 2.4 For a small category 𝔹 let 𝔹_{#} be the small category with objects given by the morphisms of 𝔹, arrows α [figure] β given by pairs of morphisms (φ, γ) in 𝔹 such that

\xymatrix{A \ar[d]_{α} & B \ar[l]_{φ} \ar[d]^{β} \\ A′ \ar[r]_{γ} & B′}

commutes, identities given by pairs of identities in 𝔹, and composition given pointwise.

Example 2.5 The twisted arrow category M(A)_{#} has objects given by finite sequences α ∈ A^{∗} and morphisms given by extensions (φ, γ) : α [figure] φ · α · γ (α, φ, γ ∈ A^{∗}). Notice that the poset P(A) appears as the subcategory of M(A)_{#} consisting of the post-extensions (ε, γ) : α [figure] α·γ (α, γ ∈ A^{∗}), whilst the dual poset P(A)^{op} appears as the subcategory of M(A)_{#} of the preextensions (φ, ε) : α [figure] φ · α (α, φ ∈ A^{∗}). Thus, we may regard M(A)_{#} as a path category extending P(A) with intertwined past and future (or back and forth) observations.

The mapping ( )_{#} : 𝔹 [figure] 𝔹_{#} extends to an endofunctor on Cat in an obvious way. It was show in [BN98] that,

f is a ufl functor iff f_{#} is a discrete fibration .

Thus we obtain functors UFL/𝔹 [figure] DFib/𝔹_{#} which we also denote ( )_{#}.

Proposition 2.6 For f, g ∈ |Cat/𝔹|, consider H : g_{#} [figure] f_{#} in Cat/𝔹_{#}. If f is a ufl functor then there exists a (necessarily unique) functor h such that h : g [figure]f in Cat/𝔹 and H = h_{#}.

Proof: The functor H has the following properties.

• For Y ∈ 𝕐_{0}, we have that H(id_{Y}) = id_{X} for some (necessarily unique) X ∈ 𝕏_{0}, which we set to be h(Y).

Follows from Lemma 2.2, because f(H(id_{Y})) = id_{gY} using that f_{#} ∘ H = g_{#} and the definition of ( )_{#}.

• For y : Y [figure] Y′ in 𝕐,

1. dom(Hy) = h(Y) and H(id_{Y} , y) = (id_{hY} , Hy).

2. cod(Hy) = h(Y′) and H(y, id_{Y′}) = (Hy, id_{hY′}).

We only show (1), as (2) is proved similarly. Consider (id_{Y} , y) : id_{Y} [figure] y in 𝕐_{#}, and let

H(id_{Y} , y) = \xymatrix{h(Y) \ar[d]_{H(id_{Y} )=id_{hY}} & X_{0} \ar[l]_{x_{0}} \ar[d]^{H(y)} \\ h(Y) \ar[r]_{x_{1}} & X_{1} & .}

Using that f_{#} ∘ H = g_{#} and the definition of ( )_{#} it follows that (f(x_{0}), f(x_{1})) = (id_{gY} , g(y)). Thus, by Lemma 2.2, we have that X_{0} = h(Y) and x_{0} = id_{hY}, and so also that x_{1} = H(y).

From the above we obtain the following two further properties.

• For Y [figure: y] Y′ [figure: y′] Y′′ in 𝕐,

H(y · y′) = H(y) · H(y′) .

• For (y_{0}, y_{1}) : y [figure] y′ in 𝕐_{#},

H(y_{0}, y_{1}) = (Hy_{0}, Hy_{1}) .

Finally, defining h : 𝕐 [figure] 𝕏 : y [figure] H(y) we are done. □

It follows from this proposition that the functor ( )_{#} : UFL/𝔹 [figure] DFib/𝔹_{#} is an embedding. We proceed to characterise its image.

Lemma 2.7 For p ∈ |DFib/𝔹_{#}| the following are equivalent.

1. For some f ∈ |UFL/𝔹|, the discrete fibration p and f_{#} are isomorphic.

2. The discrete fibration p creates the following pushouts

\xymatrix{ & β \ar[dr]^{(id_{B},γ)} \ar[dl]_{(α,id_{C})} \\ α · β \ar@{-->}[dr]_{(id_{A},γ)} &  & β · γ \ar[dl]^{(α,id_{D})} \\  & α · β · γ}  (A [figure: α] B [figure: β] C [figure: γ] D in 𝔹)  (7)

(that is, the pushouts (7) have a unique lifting along p).

3. For P the presheaf in 𝔹̂_{#} associated to the discrete fibration p in DFib/𝔹_{#}, the diagram

\xymatrix{ & P (β) \\ P (α · β) \ar@{-->}[ur]^{P (α,id_{C})} &  & P (β · γ) \ar@{-->}[ul]_{P (id_{B},γ)} \\  & P (α · β · γ) \ar@{-->}[ul]^{P (id_{A},γ)} \ar@{-->}[ur]_{P (α,id_{D})}}  (A [figure: α] B [figure: β] C [figure: γ] D in 𝔹)  (8)

is a pullback in Set.

Proof:

(1) [figure] (2) For f ∈ |UFL/𝔹| we show that f_{#} creates the pushouts (7). Indeed, assume

[figure: v; (u_{0},u_{1}); (w_{0},w_{1}); u; w; β; (α,id); (id,γ); α · β; (id,γ); β · γ; (α,id); α · β · γ; .]  (9)

Then, since f is a ufl functor it follows from Lemma 2.2 that u_{1} = id and w_{0} = id; and hence that u = u_{0} · v and w = v · w_{1}. Thus, (9) has as unique lifting the pushout

\xymatrix{ & v \ar[dr]^{(id,w_{1})} \ar[dl]_{(u_{0},id)} \\ u_{0} · v \ar[dr]_{(id,w_{1})} &  & v · w_{1} \ar[dl]^{(u_{0},id)} \\  & u_{0} · w · w_{1} &  & .}

(2) [figure] (3) Because (8) is a pullback iff in the situation

[figure: v; u; w; β; (α,id); (id,γ); α · β; β · γ]

there exists a unique [figure: x; α · β · γ] such that

[figure: u; w; x; α · β; (id,γ); β · γ; (α,id); α · β · γ; .]

for some (necessarily unique) cospan u [figure] x [figure] v.

(3) [figure] (1) Let [figure: 𝔼; 𝔹_{#}; p] be a discrete fibration with the property of the preceding implication.

We define a small category 𝕏 as follows:

• 𝕏_{0} = { E ∈ 𝔼_{0} | p(E) = id };

• 𝕏_{1} = 𝔼_{0};

• dom, cod : 𝕏_{1} [figure] 𝕏_{0} are the mappings sending e ∈ 𝕏_{1} to the unique dom(e), cod(e) ∈ 𝕏_{0}

such that

[figure: dom(e); cod(e); e; id; (id,p(e)); id; (p(e),id); p(e); ;]

• id : 𝕏_{0} [figure] 𝕏_{1} is the inclusion; and

• · : 𝕏_{1} ×_{𝕏_{0}} 𝕏_{1} [figure] 𝕏_{1} is the mapping sending a pair e, e′ ∈ 𝕏_{1} such that

[figure: cod(e) = dom(e′); e; e′; id; (p(e),id); (id,p(e′)); p(e); p(e′)]

to the unique [figure: e · e′; p(e) · p(e′)] such that

[figure: e; e′; e · e′; p(e); (id,p(e′)); p(e′); (p(e),id); p(e) · p(e′); .]

Notice that the above definition only requires pullbacks as in (8) with g = id. The more general pullbacks are needed to establish the associativity law for composition. (We leave the verification of the fact that 𝕏 is a category to the reader.)

The mapping 𝕏 [figure] 𝔹 : e [figure] p(e) is functorial (an easy verification which we also omit) and we denote it f. We claim that f is a ufl functor. Indeed, a morphism e ∈ 𝕏_{1} such that f(e) = β_{0} · β_{1} has a unique factorisation lifting (e_{0}, e_{1}) given by the following construction

\xymatrix{dom(e) = dom(e_{0}) \ar@{-->}[dr] &  & cod(e_{0}) = dom(e_{1}) \ar@{-->}[dr] \ar@{-->}[dl] &  & cod(e_{1}) = cod(e) \ar@{-->}[dl] \\  & e_{0} \ar@{-->}[dr] \ar@{.>}[ddd] &  & e_{1} \ar@{-->}[dl] \ar@{.>}[ddd] \\  &  & e \\ id \ar[dr]_{(id,β_{0})} &  & id \ar[dr]^{(id,β_{1})} \ar[dl]_{(β_{0},id)} &  & id \ar[dl]^{(β_{1},id)} \\  & β_{0} \ar[dr]_{(id,β_{1})} &  & β_{1} \ar[dl]^{(β_{0},id)} \\  &  & β_{0} · β_{1} &  &  & .}

Finally we show that p ≅ f_{#} in DFib/𝔹_{#}. The isomorphism is given by the functors defined below.

• 𝔼 [figure] 𝕏_{#} : [figure: e; e′; ϵ][figure][figure: e; e′; (e_{0}, e_{1})]where, for p(e [figure: ϵ] e′) = (β [figure: (φ,γ)] β′), we set

[figure: e_{0}; e_{1}; e′; φ; (id,γ·β); γ; (φ·β,id); β′; .]

• 𝕏_{#} [figure] 𝔼 : [figure: e; e′; (e_{0}, e_{1})][figure][figure: e; e′; ϵ]where we set

[figure: cod(e_{0}) = dom(e); cod(e) = dom(e_{1}); e_{0}; e; ϵ; e_{1}; e_{0} · e; e · e_{1}; \begin{matrix}e_{0} · e · e_{1} \\ ∣∣ \\ e′ \end{matrix}; .]

□

The property of Lemma 2.7 (3) is an orthogonality condition. Indeed, it states that a presheaf in 𝔹̂_{#} is orthogonal to the set of canonical maps { y(α · β) +_{y(β)} y(β · α) [figure] y(α · β · γ) }.

Moreover, as the diagrams (7) are pullbacks, this property amounts to the sheaf condition with respect to covers of the form

\xymatrix{α · β \ar[dr]_{(id,γ)} &  & β · γ \ar[dl]^{(α,id)} \\  & α · β · γ}  (A [figure: α] B [figure: β] C [figure: γ] D in 𝔹)  (10)

We denote this family of covers in 𝔹_{#} by K_{3} and write Ort(𝔹_{#}, K_{3}) for the full subcategory of 𝔹̂_{#} consisting of the presheaves orthogonal (in the above sense) to the covers in K_{3}. By Proposition 2.6, in the presence of the axiom of choice, it follows that

UFL/𝔹 ≃ Ort(𝔹_{#}, K_{3}) .  (11)

We thus obtain the following corollary (see [FK72, Kel82, AR94, Bor94]).

Corollary 2.8 UFL/𝔹 is (equivalent to) a full reflective subcategory of 𝔹̂_{#}.

One can check that the representables y(β) (β ∈ |𝔹_{#}|) satisfy the condition of Lemma 2.7 (3). Hence, the Yoneda embedding 𝔹_{#} [figure] 𝔹̂_{#} factors through the embedding UFL/𝔹 [figure] 𝔹̂_{#}. Explicitly, we obtain the following Yoneda embedding,

[figure: 𝔹_{#}; u_{𝔹}; UFL/𝔹; β; [[β]]; 𝔹; u(β)]  (12)

where, for β : B [figure] B′, the category [[β]] has objects given by factorisations (B [figure: φ] X [figure: γ] B′) of β in 𝔹, morphisms χ : (φ, X, γ) [figure] (φ′, X′, γ′) given by arrows χ : X [figure] X′ in 𝔹 such that

\xymatrix{ & B \ar[dr]^{φ′} \ar[dl]_{φ} \\ X \ar[dr]_{γ} \ar[rr]^{χ} &  & X′ \ar[dl]^{γ′} \\  & B′}  (13)

commutes, and identities and composition given as in 𝔹; the ufl functor u(β) maps a morphism

as in (13) to X [figure: χ] X′. Following [Law86c] we will refer to the categories [[B [figure: β] B′]] as interval categories; they range from the initial object (id_{B}, B, β) to the terminal object (β, B′, id_{B′}).

Associated to every functor f : 𝕏 [figure] 𝔹 there is a natural transformation

[figure: 𝕏_{#}; [[ ]]; f_{#}; \overline{f}; 𝔹_{#}; [[ ]]; Cat]

where \overline{f}_{x} : [[x]] [figure][[fx]] : (x_{0}, X, x_{1}) [figure](fx_{0}, fX, fx_{1}). This data permits an alternative characterisation of the (UFL) property [Law86c]:

f is a ufl functor iff \overline{f} is a natural isomorphism .

3 Transition graphs

Labelled transition graphs generalise labelled transition systems in that they allow different transitions between states to be labelled by the same action. Specifically, a transition graph consists of a set of states and a set of labelled transitions between states. For an example, we depict below a transition graph over a set of actions A which is not a transition system.

[figure: 0; a; a; a; 1; a; a]  (a ∈ A)  (14)

Morphisms between transition graphs are given by pairs of functions between the underlying sets of states and transitions that respect both the labelling, and the initial and final states of transitions. The category of transition systems is then the full subcategory of the category of transition graphs consisting of objects which are extensional in the sense that every transition is uniquely determined by its label, and by its initial and final states.

The category of transition graphs over a set of actions A will be denoted TG_{A}. The purpose of this section is to analyse static and dynamic aspects (with emphasis on the latter) of this category. As we will see below, a topos of labelled graphs (see [Law89]) provides a natural setting for treating static aspects; whilst, as hinted at in Section 1, ufl functors are appropriate structures for the study of the dynamics.

Static aspect. We give the definition of (the static view of) the category of transition graphs.

TG_{A} = Graph/ℓ(A) ≅ Ĝ_{A}

where

G_{A}^{op} = (∫ ℓ(A))^{op} ≅ N [figure: ^{dom^{a}}; _{cod_{a}}] E_{a} (a ∈ A)  .

Thus, TG_{A} is a presheaf topos; the subobject classifier is given by the transition graph (14) equipped with the subobject [figure: 1; a] (a ∈ A) (c.f. [Law89, BN98]). The category of transition systems TS_{A} appears as the full subcategory of TG_{A} of transition graphs that are extensional with respect to

U = • ≅ ℓ(0 [figure] A) in Graph/ℓ(A)
≅ y(N)  in Ĝ_{A}  ;

that is, those transition graphs S with the property that, for all f, g : G [figure] S in TG_{A},

if f ∘ u = g ∘ u, for all u : U [figure] G, then f = g .

It follows that TS_{A} is a full reflective exponential ideal of TG_{A}, and that it is not a topos. The reflector TG_{A} [figure] TS_{A} identifies transitions with both the same label, and initial and final states. (The reader may wish to calculate exponentials.)

Dynamic aspect. We observe that

TG_{A} ≃ UFL/M(A)  (15)

and argue that this representation embodies the dynamics of transition graphs. The equivalence (15) above for the case A = 1 was first noticed by Street and Schanuel.

To see (15) observe that the adjunction η, ε : F ⊣ U : Cat [figure]Graph induces the following adjoint situation

Graph/ℓ(A) [figure: Σ_{η}; ⊤; η^{∗}]Graph/UF(ℓA) [figure: ⊤]Cat/F(ℓA)  (16)

where the left adjoint lands in UFL/F(ℓA). Moreover, the unit of this adjunction is an

isomorphism; whilst, for [figure: 𝕏; F(ℓA); f] in Cat/F(ℓA), the component of the counit at f is an iso-

morphism iff the category 𝕏 is freely generated by the morphisms in it over an element of A, iff f is a ufl functor. Thus, the adjunction (16) cuts down to the equivalence (15).

The first dynamic aspect of transition graphs to be considered is the operation that associates a transition graph with its space of computation paths. For transition systems, this construction amounts to the well-known coreflection ST_{A} [figure: ⊤]TS_{A}^{•} unfolding a transition system with an initial state into a synchronisation tree with root the given initial state [WN97]. The corresponding construction for transition graphs is as follows

{ \atop P(A)} [figure: ⊤]UFL/P(A) [figure: Σ_{Δ}; ⊤; Δ^{∗}]UFL/M(A) ;  (17)

the right adjoint unfolds a transition graph into the synchronisation forest of all the possible finite runs of the system. A more conceptual description of this adjunction is basically given by the reflection of Corollary 2.8. To see this, for a small category 𝔹 let j : 𝔹_{#}^{+} [figure] 𝔹_{#} be the inclusion of the category 𝔹_{#}^{+} ≅ ∑_{B∈𝔹_{0}} B/𝔹 of post-extensions in the category 𝔹_{#} (see Example 2.5). We have the following adjoint situation

𝔹̂_{#}^{+} [figure: j_{!}; ⊤; j^{∗}] 𝔹̂_{#} [figure: ⊤; ( )_{#}] UFL/𝔹

which for 𝔹 = M(A) yields (17).

Finally we concentrate on process equivalence. A standard such notion is given by bisimilarity [Mil89]. We recall the definition. A (strong) bisimulation between transition graphs X and Y is a relation R between their respective state sets such that whenever x R y, then

if x [figure: a] x′ then y [figure: a] y′ and x′ R y′, for some y′;
if y [figure: a] y′ then x [figure: a] x′ and x′ R y′, for some x′.

(Here we have used the notation s [figure: a] s′ to refer to an anonymous transition from s to s′ labelled by a.) One says that two transition graphs with initial state are bisimilar if there is a bisimulation relating the respective initial states.

Following [JNW96], we provide a treatment of bisimulation for transition graphs via open maps. Very roughly, the idea of this approach is to consider a category of models M together with a path functor π : P [figure] M and define the notion of π-bisimilarity as given by a span of π-open maps. A map in M is said to be π-open if the image of every map in P under π is weakly orthogonal to it; that is, X [figure] Y in M is π-open if, for every p : P [figure] Q in P, all commutative squares

\xymatrix{πP \ar[r] \ar[d]_{πp} & X \ar[d] \\ πQ \ar[r] \ar@{.>}[ur]^{∃} & Y}

have a fill-in as indicated.

In the setting of so-called presheaf models [CW97], the category of models is given by a presheaf category and the path functor is taken to be the Yoneda embedding. In our context, the structure of the category of paths allows for various alternatives. The straightforward choice is to consider the Yoneda embedding u_{𝔹} : 𝔹_{#} [figure] UFL/𝔹 (see (12)); another possibility is its restriction

u_{𝔹}^{+} : 𝔹_{#}^{+} [figure] 𝔹_{#} [figure] UFL/𝔹 .

For the case under study, 𝔹 = M(A), the path functor u^{+} is the inclusion P(A) [figure] TG_{A}; yielding a situation analogous to the one considered in [JNW96] for transition systems. It follows that two transition graphs X and Y with initial states x : U [figure] X and y : U [figure] Y are bisimilar iff there exists a span X [figure: w_{1}] W [figure: w_{2}]Y of u^{+}-open maps such that (x, y) ∈ W (that is, (x, y) factors through (w_{1}, w_{2})). The notion of bisimulation provided by the path functor u : M(A)_{#} [figure] TG_{A} corresponds to back-and-forth bisimulation [DNMV90, WN97].

4 Triangulated categories

In the previous section we have regarded and analysed the category of transition graphs UFL/M(A) as an interleaving model of concurrent computation. In this section control categories like M(A) are axiomatised as triangulated categories. Roughly speaking triangulated categories are those in which every commutative square has an essentially unique triangular factorisation (see (CFI) in Definition 4.1 below). Intuitively, a triangulated control category is a control category in which two equal control paths can be linearised (or interleaved) in a canonical fashion, as exemplified in the following diagram

\xymatrix{ & α_{1} \ar[rr] &  & α_{2} \ar@{.>}[ddr] \ar@{.>}[ddrrr] \ar[rr] &  & α_{3} \ar[rr] &  & α_{4} \ar[dr] \\ * \ar[ur] \ar[drr] &  &  &  &  &  &  &  & • \\  &  & β_{1} \ar[rr] \ar@{.>}[uul] \ar@{.>}[uur] &  & β_{2} \ar[rr] &  & β_{3} \ar@{.>}[uur] \ar@{.>}[uul] \ar[urr]}  (18)

where the top and bottom control paths have been linearised (interleaved) as the control path

∗ [figure] β_{1}  [figure] α_{1}  [figure] α_{2}  [figure] β_{2}  [figure] β_{3}  [figure] α_{3}  [figure] α_{4}  [figure] • .

Our main use for triangulated categories is in the next section where we investigate the categories of processes UFL/ℂ for a triangulated control category ℂ. Thus, from the computational viewpoint, we will be focusing on so-called interleaving models of concurrent processes.

Definition 4.1 A triangulated category ℂ is a category satisfying either of the following equivalent conditions.

(CFI) Canonical fill-in.

(C) Cancellation: for every \xymatrix{a \ar[r]^{α} & b \ar[r]^{φ} \ar[r]_{γ} & c \ar[r]^{β} & d} in ℂ,

if α · φ = α · γ and φ · β = γ · β then φ = γ .

(FI) Fill-in: every commutative square in ℂ has a fill-in.

(IG) Interval glueing.

For every a [figure: α] b [figure: β] c in ℂ, the commutative square

\xymatrix{ & [[id_{b}]] \ar@{-->}[dl]_{[[α,id_{b}]]} \ar@{-->}[dr]^{[[id_{b},β]]} \\ [[α]] \ar@{-->}[dr]_{[[id_{a},β]]} &  & [[β]] \ar@{-->}[dl]^{[[α,id_{c}]]} \\  & [[α · β]]}  (19)

is a pushout in Cat.

The equivalence between (CFI) and (IG) will be proved below. Before doing so we mention some examples and comment on the definition.

In a triangulated category, fill-in’s of commutative squares are canonical in the sense that two parallel fill-in’s are equal, whilst two opposite fill-in’s are the inverse of each other. Thus the interval categories are linear preorders.

Examples of triangulated control categories are: free categories on graphs (in particular, the monoid M(A) for any set A); preorders in which every interval is linear (in particular, the poset P(A) for any set A); and the additive monoid of non-negative real numbers. These examples are special in that they satisfy the further property

(RI) Every retraction is an identity.

making the interval categories into linear orders. It follows that the categories satisfying (CFI) and (RI) are the factorisation linearly ordered categories of [BN98].

In the context of categories of processes, the properties (C), (IG), and (RI) have been respectively considered by Lawvere in [Law89], [Law86b], and [Law86c].

Examples of triangulated categories in which the property (RI) does not hold include: groupoids, and the category

[figure: 1; (1); (0); 2; (1,0)] .

The simplest non-example of a triangulated category is the (independence) square

\xymatrix{ & (a, ∗) \ar@{-->}[dr] \\ (∗, ∗) \ar@{-->}[ur] \ar@{-->}[dr] &  & (a, b) \\  & (∗, b) \ar@{-->}[ur]}

typical of non-interleaving (or independence) models of concurrent processes [WN95].

It was shown in [BN98], via model generated techniques, that, for a category ℂ satisfying (IG), the category UFL/ℂ is a topos. We will give another proof of this result in the next section by exhibiting it as a sheaf topos. We remark that for an arbitrary base category 𝔹 the category UFL/𝔹 need not be a topos. Indeed, this was established by Johnstone for 𝔹 the commutative square [Joh98].

We proceed to show the equivalence between (CFI) and (IG).

Theorem 4.2 The following statements are equivalent.

1. ℂ has the canonical fill-in property (CFI).

2. For every a [figure: α] b [figure: β] c in ℂ the commutative diagram

\xymatrix{ & [[id_{b}]]_{0} \ar[dl]_{[[α,id_{b}]]_{0}} \ar@{-->}[dr]^{[[id_{b},β]]_{0}} \\ [[α]]_{0} \ar@{-->}[dr]_{[[id_{a},β]]_{0}} &  & [[β]]_{0} \ar@{-->}[dl]^{[[α,id_{c}]]_{0}} \\  & [[α · β]]_{0}}  (20)

is a pushout in Set.

3. ℂ has the interval glueing property (IG).

The implication (3) [figure] (2) holds because the forgetful functor ( )_{0} : Cat [figure] Set has a right adjoint and hence preserves colimits.

We prove the implication (2) [figure] (1). Henceforth we will refer to the statement in Theorem 4.2 (2) as the “(IG)_{0} property”. We start with the following crucial lemma.

Lemma 4.3 If ℂ has the (IG)_{0} property then it satisfies the following property

Every idempotent is an identity.  (21)

and hence also the property

Every retraction is an isomorphism.

Proof: Let e be an idempotent. We write ≈ for the equivalence relation on [[e]]_{0} + [[e]]_{0} generated by ∼ defined as follows

⨿_{1}(e · x, y) ∼ ⨿_{2}(x, y · e) , for every (x, y) ∈ [[id]]_{0} .

Notice the important fact that

[⨿_{1}(e, id)]_{≈} = { ⨿_{1}(e, id), ⨿_{2}(id, e) } .  (22)

We have the following situation

[figure: [[id]]_{0}; [[e,id]]_{0}; [[id,e]]_{0}; [[e]]_{0}; [[e,id]]_{0}; [[e]]_{0}; [[id,e]]_{0}; _{[[e]]_{0} + [[e]]_{0}/≈}; ≅; ∃!; [[e]]_{0}]

and since [[id, e]]_{0}(e, id) = (e, e) = [[id, e]]_{0}(e, e) it follows that ⨿_{1}(e, id) ≈ ⨿_{1}(e, e); which, by (22) above, yields e = id. □

Property (21) is considered in [Law89].

It follows that the pushout (20) is simply a union.

Corollary 4.4 Assume that ℂ has the (IG)_{0} property. For every α : a [figure]b in ℂ, the

functions [[α, id]]_{0} : [[id]]_{0}  [figure] [[α]]_{0} and [[id, α]]_{0} : [[id]]_{0}  [figure] [[α]]_{0} are injective.

Proof: By Lemma 4.3, for every (x, y) ∈ [[id]]_{0}, we have that x and y are inverse of each other. Thus, for (x, y), (x′, y′) ∈ [[id]]_{0}, if [[α, id]]_{0}(x, y) = [[α, id]]_{0}(x′, y′) then y = y′ and so x = y^{−1} = y′^{−1} = x′. The injectivity of [[id, α]]_{0} is established analogously. □

As a consequence of the above we have that under the (IG)_{0} property, for every a [figure: α] b [figure: β] c, the functions [[id, β]]_{0} : [[α]]_{0} [figure] [[α · β]]_{0} and [[α, id]]_{0} : [[β]]_{0} [figure] [[α · β]]_{0} are injective. Hence, as we show below, the implication (2) [figure] (1) holds.

Proposition 4.5 If a category satisfies the (IG)_{0} property then it also satisfies the canonical fill-in property (CFI).

Proof:

(C) Let \xymatrix{a \ar[r]^{α} & b \ar[r]^{φ} \ar[r]_{γ} & c \ar[r]^{β} & d} in ℂ where α · φ = α · γ and φ · β = γ · β. Then we

have that φ equals γ because the objects (α, φ), (α, γ) ∈ [[α · φ]]_{0} are both mapped under the injection [[id, β]]_{0} : [[α · φ]]_{0} [figure] [[α · φ · β]]_{0} to (α, φ · β) = (α, γ · β).

(FI) Assume α · β = φ · γ. If (φ, γ) = [[id, β]]_{0}(α_{0}, α_{1}) ∈ [[α · β]]_{0} for some (α_{0}, α_{1}) ∈ [[α]]_{0} then α_{1} provides the required fill-in; otherwise, (φ, γ) = [[α, id]]_{0}(β_{0}, β_{1}) ∈ [[α · β]]_{0} for some (β_{0}, β_{1}) ∈ [[β]]_{0} and the required fill-in is provided by β_{0}. □

Finally we show the implication (1) [figure] (3). The version of Proposition 4.7 below for factorisation linearly ordered categories (categories satisfying (CFI) and (RI)) appears in [BN98].

Proposition 4.6 If a category satisfies the canonical fill-in property (CFI) then it also satisfies the (IG)_{0} property.

Proof: Let [[α]]_{0} [figure: f_{0}] X [figure: g_{0}] [[β]]_{0} be a cone for the span [[α]]_{0} [figure: [[α,id]]_{0}] [[id]]_{0} [figure: [[id,β]]_{0}] [[β]]_{0} in Set.

Since fill-in’s are canonical, it follows that the relation [figure: h_{0}] ⊆ [[α · β]]_{0} × X given by

(φ, γ) [figure: h_{0}] f_{0}(φ, μ) , for μ : (φ, γ) [figure] (α, β) in [[α · β]]
(φ, γ) [figure: h_{0}] g_{0}(ν, γ) , for ν : (α, β) [figure] (φ, γ) in [[α · β]]

defines a function [[α · β]]_{0} [figure]X, which can be readily checked to be the required unique mediating morphism. □

Proposition 4.7 If a category satisfies the canonical fill-in property (CFI) then it also satisfies the interval glueing property (IG).

Proof: We start with the following lemma: for every a [figure: φ]b [figure: γ]c, the functors [[id, γ]] : [[φ]] [figure][[φ · γ]] and [[φ, id]] : [[γ]] [figure][[φ · γ]] are embeddings. Indeed, the functor [[id, γ]] is faithful by construction. It is also full because, for objects (φ_{0}, φ_{1}), (φ′_{0}, φ′_{1}) ∈ [[φ]] and a morphism μ : (φ_{0}, φ_{1} · γ) [figure](φ′_{0}, φ′_{1} · γ) in [[φ · γ]] we have that φ_{0} · μ = φ′_{0}, and that φ_{1} · γ = (μ · φ′_{1}) · γ and φ_{0} · φ_{1} = φ = φ′_{0} · φ′_{1} = φ_{0} · (μ · φ′_{1}). Thus, by cancellation, the equality φ_{1} = μ · φ′_{1} holds and we are done. The case for the functor [[φ, id]] is analogous.

It follows that the diagrams (19) consist of injective-on-objects embeddings. We proceed

to show that they are pushouts. Let [[α]] [figure: f] 𝕏 [figure: g] [[β]] be a cone for the span [[α]] [figure: [[α,id]]]

[[id]] [figure: [[id,β]]] [[β]] in Cat, and let h_{0} : [[α · β]]_{0} [figure] 𝕏_{0} be the function given by Proposition 4.6

with respect to the cone [[α]]_{0} [figure: f_{0}] 𝕏_{0} [figure: g_{0}] [[β]]_{0} in Set.

Notice the following two properties that follow form cancellation.

• For every (α_{0}, α_{1}) ∈ [[α]], (β_{0}, β_{1}) ∈ [[β]] and γ : (α_{0}, α_{1} · β) [figure] (α · β_{0}, β_{1}) in [[α · β]], we have that γ = α_{1} · β_{0}.

• For every (α_{0}, α_{1}) ∈ [[α]], (β_{0}, β_{1}) ∈ [[β]], and γ : (α · β_{0}, β_{1}) [figure] (α_{0}, α_{1} · β) in [[α · β]], we have that β_{0} and α_{1} are isomorphisms and that γ = β_{0}^{−1} · α_{1}^{−1}.

Thus we may extend the function h_{0} to a functor h = (h_{0}, h_{1}) : [[α · β]] [figure] 𝕏 by cases as follows.

1. For γ : (α_{0}, α_{1}) [figure] (α′_{0}, α′_{1}) in [[α]], set

((α_{0}, α_{1} · β) [figure: γ] (α′_{0}, α′_{1} · β)) [figure: h_{1}]f_{1}(γ) .

2. For γ : (β_{0}, β_{1}) [figure] (β′_{0}, β′_{1}) in [[β]], set

(α · β_{0}, β_{1}) [figure: γ] (α · β′_{0}, β′_{1})) [figure: h_{1}]g_{1}(γ) .

3. For (α_{0}, α_{1}) ∈ [[α]], (β_{0}, β_{1}) ∈ [[β]], and γ : (α_{0}, α_{1} · β) [figure] (α · β_{0}, β_{1}) in [[α · β]], set

γ [figure: h_{1}]f_{1}((α_{0}, α_{1}) [figure: α_{1}] (α, id)) · g_{1}((id, β) [figure: β_{0}] (β_{0}, β_{1})) .

4. For (α_{0}, α_{1}) ∈ [[α]], (β_{0}, β_{1}) ∈ [[β]], and γ : (α · β_{0}, β_{1}) [figure] (α_{0}, α_{1} · β) in [[α · β]], set

γ [figure: h_{1}]g_{1}((α · β_{0}, β_{1}) [figure: ^{β_{0}^{−1}}] (α, β)) · f_{1}((α, β) [figure: ^{α_{1}^{−1}}] (α_{0}, α_{1} · β)) .

That h is well-defined and has the required universal property is easily checked. □

We conclude the section with a property of twisted arrow categories of triangulated categories that gives insight into these notions. Intuitively, the property says that a path appearing in two non-overlapping parts of another path is a deformation.

Proposition 4.8 For ℂ triangulated, every commutative diagram

\xymatrix{ & ρ \ar[dr]^{(τ_{0},τ_{1})} \ar[dl]_{(σ_{0},σ_{1})} \\ α · β \ar@{-->}[dr]_{(φ,γ_{0}·γ·γ_{1})} &  & γ \ar[dl]^{(φ·α·β·γ_{0},γ_{1})} \\  & φ · α · β · γ_{0} · γ · γ_{1}}

in ℂ_{#} is such that ρ and σ_{1} are isomorphisms. Hence, the map (σ_{0}, σ_{1}) : ρ [figure] α · β factors through (α, id) : β [figure] α · β.

Proof: We have that φ · α · β = φ · α · β · (γ_{0} · τ_{0} · ρ · σ_{1}) and that (γ_{0} · τ_{0} · ρ · σ_{1}) · γ_{0} · γ · γ_{1} = γ_{0} · γ · γ_{1} and so, by cancellation, γ_{0} · τ_{0} · ρ · σ_{1} = id. Since in a triangulated category retractions are isomorphisms, it follows that γ_{0}, τ_{0}, ρ, σ_{1} are isos. The map (σ_{0}, σ_{1}) factors as (β · σ_{1}^{−1} · ρ^{−1}, σ_{1}) · (α, id). □

5 Categories of processes

We study the categories UFL/ℂ for ℂ a triangulated category. That the control category be triangulated leads to considering processes with a category of states in which any two equal evolution paths can be linearised into one. Indeed, we have the following proposition.

Proposition 5.1 For a ufl functor [figure: 𝕏; ℂ; f]over a triangulated category ℂ, the category 𝕏 is

triangulated.

Proof: Follows from the commutativity of the following cube

[figure: [[id]]; [[id,y]]; _{\overline{f}_{id}}; ≅; [[x,id]]; [[y]]; ≅; _{\overline{f}_{y}}; [[x,id]]; [[x]]; [[id,y]]; ≅; _{\overline{f}_{x}}; [[x · y]]; ≅; _{\overline{f}_{x·y}}; [[id]]; [[id,fy]]; [[fx,id]]; [[fy]]; [[fx,id]]; [[fx]]; [[id,fy]]; [[fx · fy]]]

for every X [figure: x] Y [figure: y] Z in 𝕏. □

As a consequence, interval categories in a triangulated category are triangulated (see (12)).

We proceed to show that the categories UFL/ℂ for ℂ a triangulated category are sheaf toposes —they may be regarded as topos models of linearly-controlled processes. Our approach is to establish the equivalence between the orthogonality condition of Lemma 2.7 (3) and a sheaf condition. To this end we need consider binary versions of the covers K_{3} introduced in (10). For a small category ℂ, let K_{2} be the family of covers

\xymatrix{α \ar[dr]_{(id,γ)} &  & γ \ar[dl]^{(α,id)} \\  & α · γ}  (A [figure: α] Y [figure: γ] D in ℂ)

in ℂ_{#}. These covers need not be pretopologies; however the stability axiom can be easily guaranteed.

Proposition 5.2 For a small category ℂ, the family of covers K_{2} satisfies the stability axiom for a pretopology iff the category ℂ has the fill-in property (FI).

Proof:

( [figure] ) Let α · β = φ · γ. Consider the cover α [figure: (id,β)] φ · γ [figure: (α,id)] β and the map (φ, γ) :

id [figure] φ · γ. There exists a cover μ [figure: (id,ν)] id [figure: (μ,id)] ν such that, for instance, the composite

μ [figure: (id,ν)] id [figure: (φ,γ)] φ · γ factors through α [figure: (id,β)] φ · γ or through β [figure: (α,id)] φ · γ. In the first case, if (id, ν) · (φ, γ) = (ρ, σ) · (id, β) then μ · σ is a fill-in for the equal pair of arrows α · β and φ · γ. In the second case, if (id, ν) · (φ, γ) = (ρ, σ) · (α, id) then ρ provides the fill-in.

( [figure] ) Consider the cover α [figure: (id,β)] α · β [figure: (α,id)] β and let (μ, ν) : γ [figure] α · β. The proof proceeds by inspecting the triangulations of the equal pair of arrows α · β and μ · γ · ν. The only non-trivial situation is

\xymatrix{ &  & • \ar[drr]^{β} \ar@{.>}[ddr]^{γ_{1}} \\ • \ar[dr]_{μ} \ar[urr]^{α} &  &  &  & • \\  & • \ar[rr]_{γ} \ar@{.>}[uur]^{γ_{0}} &  & • \ar[ur]_{ν}}

in which case we have the factorisations below

\xymatrix{γ_{0} \ar[ddr]_{(id,γ_{1})} \ar@{.>}[rrrrr]^{(μ,id)} &  &  &  &  & α \ar[ddl]^{(id,β)} \\  &  & γ_{1} \ar[dl]_{(γ_{0},id)} \ar@{.>}[r]^{(id,ν)} & β \ar[dr]^{(α,id)} \\  & γ \ar[rrr]_{(μ,ν)} &  &  & α · β &  & .}

□

Let \overline{K_{2}} be the closure of K_{2} under transitivity. Explicitly, the covers of \overline{K_{2}} are given by the families

{ (γ_{1} · . . . · γ_{i−1}, γ_{i+1} · . . . · γ_{n}) : γ_{i}  [figure] γ_{1} · . . . · γ_{i} · . . . · γ_{n} | 1 ≤ i ≤ n } .

As K_{2} satisfies the identity axiom of pretopologies, for a category ℂ with the fill-in property, we obtain a site (ℂ_{#}, \overline{K_{2}}); its associated sheaf topos Sh(ℂ_{#}, \overline{K_{2}}) is denoted U_{ℂ}. Now, following Johnstone [Joh98], we restrict attention to categories satisfying the cancellation property. We thus consider triangulated categories. For them we show that the sheaf condition with respect to \overline{K_{2}} is equivalent to orthogonality with respect to K_{3}. This, by (11) above, establishes Theorem 5.4.

Proposition 5.3 Let ℂ be a triangulated category. For a presheaf in ℂ̂_{#} the following statements are equivalent.

1. The presheaf is orthogonal to every cover in K_{3}.

2. The presheaf is orthogonal to every cover in K_{2}.

3. The presheaf is a \overline{K_{2}}-sheaf.

Proof:

(1) [figure] (2) Vacuosly.

(2) [figure] (3) For a presheaf P in ℂ̂_{#} we show by induction on the size of the covers in \overline{K_{2}} that P satisfies the sheaf condition.

For n = 1, the sheaf condition is trivial and, for n = 2, it amounts to orthogonality with respect to covers in K_{2}. For the inductive step, assume that P satisfies the sheaf condition for all covers in \overline{K_{2}} of size n (n ≥ 2). Consider a cover \{ γ_{i} [figure] γ_{1} · . . . · γ_{n+1} | 1 ≤ i ≤ n + 1 \} and let { x_{i} : γ_{i} [figure] P | 1 ≤ i ≤ n + 1 } be a matching family for it. Define x_{1,2} : γ_{1} · γ_{2} [figure] P as the unique amalgamation, given by orthogonality with respect to K_{2}, of the matching

family { x_{1}, x_{2} } for the cover { γ_{1}  [figure] γ_{1} · γ_{2}, γ_{2}  [figure] γ_{1} · γ_{2} } in K_{2}. Observe that the family
{ x_{1,2} }∪{ x_{i} | 3 ≤ i ≤ n+1 } is a matching family for the cover { γ_{1}·γ_{2}  [figure] γ_{1}·. . .·γ_{n+1} }∪{ γ_{i}  [figure]

γ_{1} · . . . · γ_{n+1} | 3 ≤ i ≤ n + 1 \} in \overline{K_{2}} because, by Proposition 4.8, whenever we have a common restriction as below

\xymatrix{ & ρ \ar[dr] \ar[dl] \\ γ_{1} · γ_{2} \ar[dr]_{(id,γ_{3}·...·γ_{n+1})} &  & γ_{i} \ar[dl]^{(γ_{1}·...·γ_{i−1},γ_{i+1}·...·γ_{n+1})} \\  & γ_{1} · . . . · γ_{n+1}}  (3 ≤ i ≤ n + 1)

the map ρ [figure] γ_{1} · γ_{2} factors through (γ_{1}, id) : γ_{2} [figure] γ_{1} · γ_{2}. By inductive hypothesis, there exists a unique amalgamation x : γ_{1} · . . . · γ_{n+1} [figure]P such that (γ_{1} · γ_{2} [figure]γ_{1} · γ_{2} · γ_{3} · . . . · γ_{n+1}) · x = x_{1,2} and (γ_{i} [figure]γ_{1} · . . . · γ_{n+1}) · x = x_{i} (3 ≤ i ≤ n + 1). Clearly, x is an amalgamation for the matching family { x_{i} | 1 ≤ i ≤ n + 1 } with respect to the cover { γ_{i} [figure] γ_{1} · . . . · γ_{n+1} | 1 ≤ i ≤ n + 1 }. It is unique because any such amalgamation is also an amalgamation for the matching family { x_{1,2} } ∪ { x_{i} | 3 ≤ i ≤ n + 1 } with respect to the cover { γ_{1} · γ_{2} [figure] γ_{1} · . . . · γ_{n+1} } ∪ { γ_{i} [figure] γ_{1} · . . . · γ_{n+1} | 3 ≤ i ≤ n + 1 }.

(3) [figure] (1) Let P be a \overline{K_{2}}-sheaf.

For A [figure: α] B [figure: β] C [figure: γ] D in ℂ, let α · β [figure: x] P [figure: y] β · γ be a matching family for the cover α · β [figure] α · β · γ [figure] β · γ in K_{3}, and let { u : α [figure] P, v : β [figure] P, w : γ [figure] P } be a matching family for the cover \{ α [figure] α · β · γ, β [figure] α · β · γ, γ [figure] α · β · γ \} in \overline{K_{2}}. The result follows form the two observations below.

1. The identities u = (id, β) · x, v = (α, id) · x = (id, γ) · y, and w = (β, id) · y hold if and only if x is the unique amalgamation of the matching family { u, v } with respect to the cover α [figure] α · β [figure] β in \overline{K_{2}}, and y is the unique amalgamation of the matching family \{ v, w \} with respect to the cover β [figure] β · γ [figure] γ in \overline{K_{2}}.

2. The amalgamations of the matching family { x, y } with respect to the cover α · β [figure] α · β · γ [figure] β · γ in K_{3} are in bijective correspondence with the amalgamations of the matching family { (id, β) · x, (α, id) · x = (id, γ) · y, (β, id) · y } with respect to the cover \{ α [figure] α · β · γ, β [figure] α · β · γ, γ [figure] α · β · γ \} in \overline{K_{2}}.

□

Theorem 5.4 For ℂ a triangulated category, we have the following equivalence

UFL/ℂ ≃ U_{ℂ} .

6 Concluding remarks

Our treatment of categories of processes, we believe, provides the basis for a fruitful approach to a conceptual analysis of general processes with state. From this viewpoint this paper opens up new possibilities and we consider it as ground work for future developments and refinements of some of the topics dealt with in here. In particular, investigations related to real-time and/or hybrid systems will be pursued elsewhere.

The fact that UFL/ℂ is a topos (for ℂ triangulated) has not been exploited here. Nor has its feature of “single universe” (for discrete fibrations and discrete opfibrations) been analysed. This relates to considering processes with “past” and “future”, or with history. Whereas of certain interest in physics, it is not clear what impact this might have in computer science.

The general considerations of this paper make sense not just for categories and functors, but also in other contexts; for example, for multicategories and multifunctors (where an application to linguistics is envisaged) and for computads (see [Str96]). Last, but not least, there are ufl functors in topology, locales, and toposes [BN98] only partially explored so far.

References

[AR94] J. Adámek and J. Rosický. Locally Presentable and Accessible Categories. Number 189 in London Mathematical Society Lecture Note Series. Cambridge University Press, 1994.

[BN98] M. Bunge and S. Niefield. Exponentiability and single universes. To appear in J. Pure Appl. Algebra, 1998.

[Bor94] F. Borceux. Handbook of Categorical Algebra. Number 50–52 in Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994.

[CW97] G.L. Cattani and G. Winskel. Presheaf models for concurrency. In D. van Dalen and M. Bezem, editors, Proceedings of the CSL’96 Conf., volume 1258 of Lecture Notes in Computer Science, pages 58–75. Springer-Verlag, 1997.

[DNMV90] R. De Nicola, U. Montanari, and F. Vaandrager. Back and forth bisimulations. In Proceedings of the CONCUR’90 Conf., volume 458 of Lecture Notes in Computer Science, pages 152–165. Springer-Verlag, 1990.

[FK72] P. J. Freyd and G. M. Kelly. Categories of continuous functors. I. J. of Pure Appl. Algebra, 2:169–191, 1972. (Erratum: J. Pure Appl. Algebra 4: 121, 1974.).

[JNW96] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Inform. and Comput., 127(2):164–185, 1996.

[Joh98] P.T. Johnstone. A note on discrete Conduché fibrations. Unpublished, July 1998.

[Kel82] G.M. Kelly. Basic concepts of enriched category theory. Number 64 in London Mathematical Society Lecture Note Series. Cambridge University Press, 1982.

[Law86a] F.W. Lawvere. Categories of spaces may not be generalized spaces as exemplified by directed graphs. Rev. Colombiana Mat., 20:179–185, 1986.

[Law86b] F.W. Lawvere. Introduction. In F.W. Lawvere and S.H. Schanuel, editors, Categories in continuum physics, volume 1174 of Lecture Notes in Mathematics, pages 1–16. Springer-Verlag, 1986.

[Law86c] F.W. Lawvere. State categories and response functors. Unpublished, May 1986.

[Law89] F.W. Lawvere. Qualitative distinctions between some toposes of generalized graphs. Contemporary Mathematics, 92:261–299, 1989.

[Mil89] R. Milner. Communication and Concurrency. Prentice Hall, 1989.

[ML71] S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.

[MLM94] S. Mac Lane and I. Moerdijk. Sheaves in geometry and logic: A first introduction to topos theory. Universitext. Springer-Verlag, 1994.

[Str96] R. Street. Categorical structures. In Handbook of algebra, volume 1, pages 529– 577. North-Holland, 1996.

[WN95] G. Winskel and M. Nielsen. Models for concurrency. In Handbook of logic in computer science, volume 4 of Oxford Sci. Publ., pages 1–148. Oxford Univ. Press, 1995.

[WN97] G. Winskel and M. Nielsen. Presheaves as transition systems. In Partial order methods in verification, volume 29 of DIMACS Ser. Discrete Math. Theoret. Comput. Sci., pages 129–140, 1997.