Theory and Applications of Categories, Vol. 25, No. 12, 2011, pp. 295–341.

TOWARDS A HOMOTOPY THEORY OF HIGHER DIMENSIONAL TRANSITION SYSTEMS

PHILIPPE GAUCHER

Abstract. We proved in a previous work that Cattani-Sassone’s higher dimensional transition systems can be interpreted as a small-orthogonality class of a topological locally finitely presentable category of weak higher dimensional transition systems. In this paper, we turn our attention to the full subcategory of weak higher dimensional transition systems which are unions of cubes. It is proved that there exists a left proper combinatorial model structure such that two objects are weakly equivalent if and only if they have the same cubes after simplification of the labelling. This model structure is obtained by Bousfield localizing a model structure which is left determined with respect to a class of maps which is not the class of monomorphisms. We prove that the higher dimensional transition systems corresponding to two process algebras are weakly equivalent if and only if they are isomorphic. We also construct a second Bousfield localization in which two bisimilar cubical transition systems are weakly equivalent. The appendix contains a technical lemma about smallness of weak factorization systems in coreflective subcategories which can be of independent interest. This paper is a first step towards a homotopical interpretation of bisimulation for higher dimensional transition systems.

Contents

1 Introduction 296 2 Weak higher dimensional transition systems 299 3 Cubical transition systems 302 4 About combinatorial model categories 309 5 The left determined model category of weak HDTS 312 6 The left determined model category of cubical transition systems 317 7 First Cattani-Sassone axiom and weakly equivalent cubical transition systems 321 8 Bousfield localization with respect to the cubification functor 326 9 Weak equivalence and bisimulation 332 A Small weak factorization system and coreflectivity 334

Received by the editors 2010-11-22 and, in revised form, 2011-06-03. Transmitted by Walter Tholen. Published on 2011-07-12. 2000 Mathematics Subject Classification: 18C35,18G55,55U35,68Q85. Key words and phrases: higher dimensional transition system, locally presentable category, topo-

logical category, combinatorial model category, left determined model category, Bousfield localization, bisimulation.

\begin{matrix}c \\ ◯ \end{matrix} Philippe Gaucher, 2011. Permission to copy for private use granted.

1. Introduction

Presentation of the paper. Directed homotopy is a field of research aiming at studying the link between concurrency and algebraic topology. In such a setting, concurrency is modelled by higher-dimensional “structures” between execution paths. In topological models like the ones of d-space [Gra03], d-space generated by cubes [FR08], flow [Gau03], globular complex [GG03], local po-space [FGR98], locally preordered space [Kri08], multipointed d-space [Gau09], these homotopies are homotopies in the usual sense which preserve the direction of time. In combinatorial models coming from the notion of (pre)cubical sets [Gou02] [Wor04] [Dij68] [Pra91] [Gun94] [VG06] [Gau08] [Gau10a], the concurrent execution of n actions is modelled by an n-cube, in which each axis of coordinates corresponds to one action.

Concurrency is modelled in a somewhat different way in the formalism of higher dimensional transition systems introduced by Cattani and Sassone [CS96]. Indeed, the concurrent execution of n actions is modelled by a multiset of n actions. A multiset is a set with possible repetition of some elements (e.g. {0, 0, 2, 3, 3, 3}). This notion is a generalization of the 1-dimensional notion of transition system in which transitions between states are labelled by one action (e.g., [WN95, Section 2.1]). The latter 1-dimensional notion cannot of course model concurrency. It is proved in [Gau10b] that Cattani-Sassone’s higher dimensional transition systems are a small-orthogonality class of a larger category of weak higher dimensional transition systems (weak HDTS) enjoying very nice categorical properties: topological and locally finitely presentable. Cattani-Sassone’s higher dimensional transition systems are weak HDTS satisfying two axioms CSA1 (cf. Definition 7.1) and CSA2 (understood first and second Cattani-Sassone Axiom): cf. Definition 6.4 for a weaker form of CSA2. In plain English, the first one says that one action between two given states can be realized by at most one transition ^{1} The axiom CSA1 used by Cattani and Sassone is even stronger (see the remark after Definition 7.1) but we do not need it by now. The second one is an analogue of the face operators in the setting of precubical sets. These two axioms are satisfied by all examples coming from process algebras.

It is not really a surprise that most of the topological models of directed homotopy can be endowed with mathematical structures which are very close to the ones existing in algebraic topology. In particular, various model category structures can be related to directed homotopy. It is more surprising that this kind of structure exists in the setting of higher dimensional transition systems as well.

We introduce in this paper the full subcategory of cubical transition systems. A cubical transition system is a weak HDTS which is equal to the union of its subcubes. Cubical transition systems have a straightforward interpretation in concurrency. All examples coming from process algebras are cubical because all these examples are already colimits of cubes. However, a cubical transition system is not necessarily a colimit of cubes and the full subcategory of weak HDTS generated by the colimits of cubes does not enjoy the closure property we expect to find in such a setting. For example, the boundary of the 2-cube (cf. Definition 3.16) is never a colimit of cubes, but is always cubical.

1In CCS, the transition a.P →^{a} P is the unique transition from a.P to P.

The main result of this paper is that the category of cubical transition systems can be endowed with a structure of left determined left proper combinatorial model category structure with respect to a class of cofibrations which is not the class of monomorphisms. This model category structure is really minimal. Indeed, the corresponding homotopy category cannot even identify all pairs of cubical transition systems containing the same cubes ! We prove that there exists a Bousfield localization such that two cubical transition systems are weakly equivalent if and only if they have the same cubes after simplification of the labelling. We also prove the existence of a Bousfield localization with respect to the proper class of bisimulations so that in the latter localization, two bisimilar cubical transition systems are weakly equivalent.

Organization of the paper. This paper starts in Section 2 with a reminder about weak higher dimensional transition systems (weak HDTS). Some information about locally presentable and topological categories are also collected here. It is important to say that the topological structure plays an important role in the work, as well as the theory of locally presentable categories which is extensively used, in particular in Appendix A. Possible references for these subjects are [AR94] [AHS06] [Ros09] [Hov99].

In Section 3, we want to introduce the notion of cubical transition system. Two equivalent definitions of them are given: the weak HDTS equal to the union of their subcubes or coreflective small-injectivity class. The last characterization already implies that the category is locally presentable. It is actually proved that it is locally finitely presentable. It is not topological since the adjunction between cubical transition systems and weak HDTS is not concrete. Indeed, the coreflector removes every action which is not used in a transition (cf. Proposition 6.10). So what plays the role of the underlying set varies. It is important to understand that the full subcategory of cubes is not a dense or even a strong generator of the category of cubical transition systems. It is necessary to add a new family of weak HDTS, the double transition ↑x↑ labelled by x for x running over the set Σ of labels (cf. Definition 2.5).

Section 4 is a reminder about combinatorial model categories, that is cofibrantly generated model categories [Hir03] [Hov99] such that the underlying category is locally presentable. Olschok’s paper [Ols09], which generalizes to locally presentable categories Cisinski’s techniques for constructing homotopical structures on toposes [Cis02], plays a fundamental role in this work. The notions of Grothendieck localizer and of left determined model category are also recalled in this section.

Section 5 expounds the construction of the combinatorial model structure on weak HDTS. This model category carries a segment object (which has nothing to do with the 1-cube !) which is the key to verifying all hypotheses of Olschok’s theorems. This model category is left proper since all objects are cofibrant. It is also left determined with respect to its class of cofibrations, i.e. it is the one with the smallest class of weak equivalences with our class of cofibrations. This class of weak equivalences is actually really small, as we will see. A cofibration of weak HDTS is by definition a map which is one-to-one on actions, but not necessarily on states. So a map like R : {0, 1} → {0} (a set being identified with the weak HDTS with same set of states, no actions and no transitions) is a cofibration of weak HDTS, and also of cubical transition systems since every set is cubical as a disjoint sum of 0-cubes. A similar cofibration R : {0, 1} → {0} exists in the model category of flows [Gau03] but we do not know whether there is a deeper connexion between these two facts.

Section 6 restricts the previous structure to the full subcategory of cubical transition systems. By definition, a cofibration of cubical transition systems is a map between cubical transition systems which is a cofibration of weak HDTS. The main problem is to prove the smallness of the class of cofibrations between cubical transition systems. The set of generating cofibrations used for constructing the left determined model structure of WHDTS cannot be reused since they involve weak HDTS which are not cubical. It is certainly possible to use combinatorial methods to find a generating set of the class of cofibrations of cubical transition systems. We use in this paper techniques of the theory of locally presentable categories. This is the subject of Appendix A which is of independent interest (cf. Theorem A.5). The argument is a kind of generalization of Smith’s arguments to prove his well-known theorem (Theorem 4.8), and more specifically for proving the smallness of the class of trivial cofibrations. But let us repeat: here the purpose is the proof of the smallness of the class of cofibrations. The smallness of the class of trivial cofibrations is a consequence of Olschok’s theorems. This model category is also left proper since all objects are cofibrant. It is also left determined with respect to its class of cofibrations.

The next Section 7 characterizes the weak equivalences in the left determined model structure of cubical transition systems. It appears that CSA1 has a homotopical interpretation. Roughly speaking, two cubical transition systems are weakly equivalent in the left determined model structure if and only if they are isomorphic modulo the first Cattani-Sassone axiom. It follows that the canonical map C_{1}[x] ⊔ C_{1}[x] ⟶ ↑x↑ sending two copies of the 1-cube generated by x to the double transition labelled by x is not a weak equivalence (cf. Figure 2). It is also proved in this section as intermediate result that every cubical transition system which satisfies CSA1 is fibrant.

Section 8 overcomes this problem by proving that it is possible to Bousfield localize with respect to the cubification functor. The above map becomes a weak equivalence since C_{1}[x] ⊔ C_{1}[x] is precisely the cubification of ↑x↑. In this Bousfield localization, two cubical transition systems are weakly equivalent if and only if they have the same cubes after simplification of the labelling.

Finally Section 9 sketches the link with bisimulation. This will be the subject of future works.

Appendix A is the categorical lemma used in the core of the paper which is of independent interest.

There are some remarks scattered in the paper about process algebras with references to [Gau10b]. But no knowledge about them is required to read this paper and these remarks can be skipped without problem.

2. Weak higher dimensional transition systems

All categories are locally small. The set of maps in a category K from X to Y is denoted by K(X, Y). The locally small category those objects are the maps of K and those morphisms are the commutative squares is denoted by Mor(K). The initial (final resp.) object, if it exists, is always denoted by ∅ (1). The identity of an object X is denoted by Id_{X}. A subcategory will be by convention always isomorphism-closed.

2.1. Notation. A non empty set of labels Σ is fixed.

Let us recall in this section the definition of a weak HDTS and some fundamental examples. We start by collecting some well-known facts about locally presentable and topological categories.

Locally presentable categories. Let λ be a regular cardinal, i.e. such that the poset λ is λ-directed [HJ99, p 160]. An object X of a category K is λ-presentable if the functor K(X, −) preserves λ-directed colimits. A category K is λ-accessible if there exists a set of λ-presentable objects such that every object of K is a λ-directed colimit of objects of this set. A category K is locally λ-presentable if it is cocomplete and λaccessible. A subcategory A of a category K is accessibly-embedded if it is full and closed under λ-directed colimits for some regular cardinal λ. A functor F : C → D is accessible if there exists a regular cardinal λ such that C and D are λ-accessible and F preserves λ-directed colimits. Every accessible functor satisfies the solution-set condition by [AR94, Corollary 2.45]. When λ = ℵ_{0}, the prefix “λ-” is replaced by “finitely”. In the preceding definitions, λ-directed diagrams can be substituted by λ-filtered diagrams by [AR94, Remark 1.21] since for every (small) λ-filtered category D, there exists a (small) λ-directed poset D_{0} and a cofinal functor D_{0} → D.

Topological categories. The paradigm of topological category over the category of Set is the one of general topological spaces with the notions of initial topology and final topology [AHS06]. More precisely, a functor ω : C → D is topological (or C is topological over D) if each cone (f_{i} : X → ωA_{i})_{i∈I} where I is a class has a unique ω-initial lift (the initial structure) (\overline{f}_{i} : A → A_{i})_{i∈I}, i.e.: 1) ωA = X and ω\overline{f}_{i} = f_{i} for each i ∈ I; 2) given h : ωB → X with f_{i}h = ω\overline{h}_{i}, \overline{h}_{i} : B → A_{i} for each i ∈ I, then h = ω\overline{h} for a unique \overline{h} : B → A. Topological functors can be characterized as functors such that each cocone (f_{i} : ωA_{i} → X)_{i∈I} where I is a class has a unique ω-final lift (the final structure) \overline{f}_{i} : A_{i} → A, i.e.: 1) ωA = X and ω\overline{f}_{i} = f_{i} for each i ∈ I; 2) given h : X → ωB with hf_{i} = ω\overline{h}_{i}, \overline{h}_{i} : A_{i} → B for each i ∈ I, then h = ω\overline{h} for a unique \overline{h} : A → B. Let us suppose D complete and cocomplete. A limit (resp. colimit) in C is calculated by taking the limit (resp. colimit) in D, and by endowing it with the initial (resp. final) structure. In this work, a topological category is a topological category over the category Set^{{s}∪Σ} where {s} ∪ Σ is called the set of sorts.

Weak higher dimensional transition systems (weak HDTS).

2.2. Definition. A weak higher dimensional transition system (weak HDTS) consists of a triple

(S, μ : L → Σ, T = ⋃_{n⩾1} T_{n})

where S is a set of states, where L is a set of actions, where μ : L → Σ is a set map called the labelling map, and finally where T_{n} ⊂ S × L^{n} × S for n ⩾ 1 is a set of n-transitions or n-dimensional transitions such that one has:

• (Multiset axiom) For every permutation σ of {1, …, n} with n ⩾ 2, if (α, u_{1}, …, u_{n}, β) is a transition, then (α, u_{σ(1)}, …, u_{σ(n)}, β) is a transition as well.

• (Coherence axiom) For every (n + 2)-tuple (α, u_{1}, …, u_{n}, β) with n ⩾ 3, for every p, q ⩾ 1 with p + q < n, if the five tuples (α, u_{1}, …, u_{n}, β), (α, u_{1}, …, u_{p}, ν_{1}), (ν_{1}, u_{p+1}, …, u_{n}, β), (α, u_{1}, …, u_{p+q}, ν_{2}) and (ν_{2}, u_{p+q+1}, …, u_{n}, β) are transitions, then the (q + 2)-tuple (ν_{1}, u_{p+1}, …, u_{p+q}, ν_{2}) is a transition as well.

A map of weak higher dimensional transition systems

f : (S, μ : L → Σ, (T_{n})_{n⩾1}) → (S′, μ′ : L′ → Σ, (T′_{n})_{n⩾1})

consists of a set map f_{0} : S → S′, a commutative square

[figure: L; μ; f̃; Σ; L′; μ′; Σ]

such that if (α, u_{1}, …, u_{n}, β) is a transition, then (f_{0}(α), f̃(u_{1}), …, f̃(u_{n}), f_{0}(β)) is a transition. The corresponding category is denoted by WHDTS. The n-transition (α, u_{1}, …, u_{n}, β) is also called a transition from α to β.

2.3. Notation. The labelling map from the set of actions to the set of labels will be very often denoted by μ.

A transition (α, u_{1}, …, u_{n}, β) intuitively means that one goes from the state α to the state β by executing concurrently n actions u_{1}, …, u_{n}. Hence the Multiset axiom, which replaces the multiset formalism of [CS96]. The Coherence axiom is more complicated to understand. We just want to say here that it is the topological part (in the sense of topological categories) of an axiom introduced by Cattani and Sassone themselves and that it is necessary for the mathematical development of the theory: it is necessary to view Cattani-Sassone’s higher dimensional transition systems as a small-orthogonality class of WHDTS. All cubes satisfy this axiom and inside a given cube, the Coherence axiom ensures that all transitions glue together properly. Formally, this axiom looks like a 5-ary composition, even if it is topological. We refer to [Gau10b] for further explanations.

The category WHDTS is locally finitely presentable by [Gau10b, Theorem 3.4]. The functor

ω : WHDTS ⟶ Set^{{s}∪Σ}

taking the weak higher dimensional transition system (S, μ : L → Σ, (T_{n})_{n⩾1}) to the ({s}∪Σ)-tuple of sets (S, (μ^{−1}(x))_{x∈Σ}) ∈ Set^{{s}∪Σ} is topological by [Gau10b, Theorem 3.4] too.

2.4. Notation. For n ⩾ 1, let 0_{n} = (0, …, 0) (n-times) and 1_{n} = (1, …, 1) (n-times). By convention, let 0_{0} = 1_{0} = ().

We give now some important examples of weak HDTS. In each of the following examples, the Multiset axiom and the Coherence axiom are satisfied for trivial reasons.

1. Let n ⩾ 0. Let x_{1}, …, x_{n} ∈ Σ. The pure n-transition C_{n}[x_{1}, …, x_{n}]^{ext} is the weak HDTS with the set of states {0_{n}, 1_{n}}, with the set of actions {(x_{1}, 1), …, (x_{n}, n)} and with the transitions all (n + 2)-tuples (0_{n}, (x_{σ(1)}, σ(1)), …, (x_{σ(n)}, σ(n)), 1_{n}) for σ running over the set of permutations of the set {1, …, n}.

2. Every set X may be identified with the weak HDTS having the set of states X, with no actions and no transitions.

3. For every x ∈ Σ, let us denote by \underline{x} the weak HDTS with no states, one action x, and no transitions. Warning: the weak HDTS {x} contains one state x and no actions whereas the weak HDTS \underline{x} contains no states and one action x.

4. For every x ∈ Σ, let us denote by ↑x↑ the weak HDTS with four states {1, 2, 3, 4}, one action x and two transitions (1, x, 2) and (3, x, 4).

2.5. Definition. The weak HDTS ↑x↑ is called the double transition (labelled by x) where x ∈ Σ.

Let us introduce now the weak HDTS corresponding to the n-cube.

2.6. Proposition. [Gau10b, Proposition 5.2] Let n ⩾ 0 and x_{1}, …, x_{n} ∈ Σ. Let T_{d} ⊂ {0, 1}^{n} × {(x_{1}, 1), …, (x_{n}, n)}^{d} × {0, 1}^{n} (with d ⩾ 1) be the subset of (d + 2)-tuples

((ϵ_{1}, …, ϵ_{n}), (x_{i_{1}}, i_{1}), …, (x_{i_{d}}, i_{d}), (ϵ′_{1}, …, ϵ′_{n}))

such that

• i_{m} = i_{n} implies m = n, i.e. there are no repetitions in the list (x_{i_{1}}, i_{1}), …, (x_{i_{d}}, i_{d})

• for all i, ϵ_{i} ⩽ ϵ′_{i}

• ϵ_{i} ≠ ϵ′_{i} if and only if i ∈ {i_{1}, …, i_{d}}.

Let μ : {(x_{1}, 1), …, (x_{n}, n)} → Σ be the set map defined by μ(x_{i}, i) = x_{i}. Then

C_{n}[x_{1}, …, x_{n}] = ({0, 1}^{n}, μ : {(x_{1}, 1), …, (x_{n}, n)} → Σ, (T_{d})_{d⩾1})

is a well-defined weak HDTS called the n-cube.

For n = 0, C_{0}[], also denoted by C_{0}, is nothing else but the weak HDTS ({()}, μ : ∅ → Σ, ∅). For every x ∈ Σ, one has C_{1}[x] = C_{1}[x]^{ext}. In [Gau10b], it is explained how the n-cube C_{n}[x_{1}, …, x_{n}] is freely generated by the pure n-transition C_{n}[x_{1}, …, x_{n}]^{ext}. It is not necessary to recall this point here.

3. Cubical transition systems

Definition of CTS. Before giving the definition of a cubical transition system, we need first to check out that unions of objects exist in WHDTS. So this section starts by studying the monomorphisms of WHDTS.

3.1. Proposition. A map f : X = (S, μ : L → Σ, T) → X′ = (S′, μ′ : L′ → Σ, T′) of WHDTS is a monomorphism if and only if the set maps f_{0} : S → S′ and f̃: L → L′ are one-to-one.

Proof. \underline{Only if part}. Suppose that f : X → X′ is a monomorphism. Let α and β be two states of X with f_{0}(α) = f_{0}(β). Consider the two maps of weak higher dimensional transition systems g, h : {0} → X defined by g(0) = α and h(0) = β. Since f is a monomorphism, one has g = h. Therefore α = β. Thus, the set map f_{0} : S → S′ is one-to-one. Now let u and v be two actions of X with f̃(u) = f̃(v). One necessarily has μ(u) = μ(v) = x ∈ Σ. Let g, h : \underline{x} → X be the two maps of higher dimensional transition systems defined respectively by g(x) = u and h(x) = v. Then g = h since f is a monomorphism. Therefore u = v and f̃ is one-to-one. \underline{If part}. Let f : X → Y be a weak higher dimensional transition system such that f_{0} and f̃ are both one-to-one. Let g, h : Z → X be two maps of higher dimensional transition systems such that fg = fh. Then f_{0}g_{0} = f_{0}h_{0} and f̃g̃ = f̃h̃. So g_{0} = h_{0} and g̃ = h̃. The forgetful functor WHDTS → Set^{{s}∪Σ} is topological, and therefore faithful by [AHS06, Theorem 21.3]. So g = h and f is a monomorphism.

3.2. Proposition. Every family of subobjects of a weak HDTS has an union, i.e. a least upper bound in the family of subobjects.

Proof. Let (f_{i} : X_{i} → X)_{i∈I} be a family of subobjects of a weak HDTS X. Let X_{i} = (S_{i}, μ : L_{i} → Σ, T_{i}). Consider the set of states S′ = ⋃_{i∈I}(f_{i})_{0}(S_{i}) and the set of actions L′ = ⋃_{i∈I} f̃_{i}(L_{i}) equipped with the final structure. We obtain a weak HDTS X′ and by Proposition 3.1, the canonical map X′ → X is a monomorphism. The weak HDTS X′ is the union of the (f_{i} : X_{i} → X)_{i∈I}.

We are now ready to give the definition of a cubical transition system.

3.3. Definition. Let X be a weak HDTS. A cube of X is a map C_{n}[x_{1}, …, x_{n}] ⟶ X. A subcube of X is the image of a cube of X. A weak HDTS is a cubical transition system if it is equal to the union of its subcubes. The full subcategory of cubical transition systems is denoted by CTS.

Let x_{1}, …, x_{n} ∈ Σ with n ⩾ 0. For n ⩾ 2, the weak HDTS C_{n}[x_{1}, …, x_{n}]^{ext} is not cubical since the union of its subcubes is equal to its set of states {0_{n}, 1_{n}}. The weak HDTS C_{n}[x_{1}, …, x_{n}] is always a cubical transition system since the image of the identity of C_{n}[x_{1}, …, x_{n}] is a subcube. The weak HDTS ↑x↑ is cubical for every x ∈ Σ. The weak HDTS \underline{x} is never cubical for any x ∈ Σ since the union of its subcube is equal to ∅. For every set A, the corresponding weak HDTS A is cubical as a disjoint sum of 0-cubes.

Lifting property and small-injectivity class.

3.4. Definition. Let i : A ⟶ B and p : X ⟶ Y be maps of K. Then i has the left lifting property (LLP) with respect to p (or p has the right lifting property (RLP) with respect to i) if for every commutative square of solid arrows

\xymatrix{A \ar[d]_{i} \ar[r]^{α} & X \ar[d]^{p} \\ B \ar@{-->}[ur]^{k} \ar[r]_{β} & Y,}

there exists a morphism k called a lift making both triangles commutative. This situation is denoted by f□g.

Let us introduce the notations inj_{K}(C) = {g ∈ K, ∀f ∈ C, f□g} and cof_{K}(C) = {f ∈ K, ∀g ∈ inj_{K}(C), f□g} where C is a class of maps of K. The class of morphisms of K that are transfinite compositions of pushouts of elements of C is denoted by cell_{K}(C). An element of cell_{K}(C) is called a relative C-cell complex. The cocompleteness of K implies cell_{K}(C) ⊂ cof_{K}(C). When the class C is a set I, every morphism of cof_{K}(I) is a retract of a morphism of cell_{K}(I) by [Hov99, Corollary 2.1.15] since in a locally presentable category, the domains of I are always small relative to cell_{K}(I).

Sometimes, the letter K in the notations cof_{K}, inj_{K} and cell_{K} may be omitted if the underlying category we are working with is obvious.

By convention, the letter K will be always omitted if K = WHDTS.

3.5. Definition. [AR94, Definition 4.1] Let S be a set of maps of a locally presentable category K. The full subcategory of S-injective objects (called a small-injectivity class) of K is generated by {X ∈ K | X → 1 ∈ inj(S)}.

Let us recall that an object X is orthogonal to S if not only it is injective, but also the factorization is unique. A small-injectivity class of a locally presentable category is always accessible. A small-orthogonality class (the subclass of objects orthogonal to a given set of objects) of a locally presentable category is always a reflective locally presentable subcategory. Read [AR94, Chapter 1.C] and [AR94, Chapter 4] for further details. For an epimorphism f, being f-orthogonal is equivalent to being f-injective.

The cubical transition systems as a small-injectivity class.

3.6. Theorem. The category of cubical transition systems is a small-injectivity class of WHDTS. More precisely, a weak HDTS X is a cubical transition system if and only if it is injective with respect to the set of inclusions C_{n}[x_{1}, …, x_{n}]^{ext} ⊂ C_{n}[x_{1}, …, x_{n}] and \underline{x_{1}} ⊂ C_{1}[x_{1}] for all n ⩾ 0 and all x_{1}, …, x_{n} ∈ Σ.

Proof. \underline{Only if part}. 1) Let X be a cubical transition system. Let C_{n}[x_{1}, …, x_{n}]^{ext} → X be a map of weak HDTS. Let (α, u_{1}, …, u_{n}, β) be the image by this map of the transition (0_{n}, (x_{1}, 1), …, (x_{n}, n), 1_{n}). By hypothesis, there exists a cube C_{m}[y_{1}, …, y_{m}] → X of X such that the image contains the transition (α, u_{1}, …, u_{n}, β). There is not yet any reason for m to be equal to n. This means that the image of C_{m}[y_{1}, …, y_{m}] → X contains the image of C_{n}[x_{1}, …, x_{n}]^{ext} → X. In other terms, the latter map factors as a composite

C_{n}[x_{1}, …, x_{n}]^{ext} ⟶ C_{m}[y_{1}, …, y_{m}] ⟶ X.

By [Gau10b, Theorem 5.6], the map C_{n}[x_{1}, …, x_{n}]^{ext} → C_{m}[y_{1}, …, y_{m}] factors as a composite C_{n}[x_{1}, …, x_{n}]^{ext} → C_{n}[x_{1}, …, x_{n}] → C_{m}[y_{1}, …, y_{m}] since the cube C_{m}[y_{1}, …, y_{m}] is injective, and even orthogonal to the inclusion C_{n}[x_{1}, …, x_{n}]^{ext} ⊂ C_{n}[x_{1}, …, x_{n}] ^{2}. Thus, X is injective with respect to the set of maps C_{n}[x_{1}, …, x_{n}]^{ext} ⊂ C_{n}[x_{1}, …, x_{n}] for all n ⩾ 0 and all x_{1}, …, x_{n} ∈ Σ. 2) Let \underline{x_{1}} → X be a map of weak HDTS. By hypothesis, there exists a cube C_{m}[y_{1}, …, y_{m}] → X of X such that the image contains the image of \underline{x_{1}} → X. In other terms, the latter map factors as a composite

\underline{x_{1}} ⟶ C_{m}[y_{1}, …, y_{m}] ⟶ X.

Since the maps of weak HDTS preserve labellings, there exists k such that x_{1} = y_{k}. Hence the factorization

\underline{x_{1}} ⟶ C_{1}[x_{1}] ⟶ C_{m}[y_{1}, …, y_{m}] ⟶ X.

So X is injective with respect to the set of maps \underline{x_{1}} ⊂ C_{1}[x_{1}] for x_{1} running over Σ. \underline{If part}. Every transition and every state of X belong to a subcube since X is injective with respect to the maps C_{n}[x_{1}, …, x_{n}]^{ext} ⊂ C_{n}[x_{1}, …, x_{n}] for all n ⩾ 0 and all x_{1}, …, x_{n} ∈ Σ. Every action of X belongs to a subcube because X is injective with respect to the maps \underline{x_{1}} ⊂ C_{1}[x_{1}] for x_{1} running over Σ.

2Orthogonality means that this factorization is unique but we do not need this fact here.

It follows that the category CTS of cubical transition systems is accessible by [AR94, Proposition 4.7]. It is even locally finitely presentable, as we will see.

Some elementary facts about (co)reflective subcategories. A coreflective (resp. reflective) subcategory of a category C is a full isomorphism-closed category such that the inclusion functor is a left (resp. right) adjoint. The right (resp. left) adjoint is called the coreflector (resp. the reflector). The two following propositions are elementary and well-known. We use them several times so we need to state them clearly.

3.7. Proposition. [ML98, page 89] Let D ⊂ C be a coreflective (isomorphism-closed) subcategory of a category C, i.e. a full subcategory such that the inclusion D ⊂ C has a right adjoint R : C → D. Then:

1. The counit R(X) → X is an isomorphism if and only if X belongs to D

2. If C is cocomplete, then so is D.

3.8. Proposition. [Rap09, Proposition 3.1(i)] Let C be a cocomplete category. Let S be a set of objects of C. The full subcategory of colimits of objects of S is a coreflective subcategory C_{S} of C. The right adjoint to the inclusion functor C_{S} ⊂ C is the “Kelleyfication” functor k_{S} defined by:

k_{S}(X) = \underrightarrow{lim} ; \begin{matrix}S → X \\ S ∈ S \end{matrix} S.

Coreflectivity of the category of cubical transition systems. First we recall how colimits are calculated in WHDTS.

3.9. Proposition. [Gau10b, Proposition 3.5] Let X = \underrightarrow{lim} X_{i} be a colimit of weak higher dimensional transition systems with X_{i} = (S_{i}, μ_{i} : L_{i} → Σ, T^{i} = ⋃_{n⩾1} T_{n}^{i}) and X = (S, μ : L → Σ, T = ⋃_{n⩾1} T_{n}). Then:

1. S = \underrightarrow{lim} S_{i}, L = \underrightarrow{lim} L_{i}, μ = \underrightarrow{lim} μ_{i}

2. the union ⋃_{i} T^{i} of the image of the T^{i} in ⋃_{n⩾1}(S × L^{n} × S) satisfies the Multiset axiom.

3. T is the closure of ⋃_{i} T^{i} under the Coherence axiom.

4. when the union ⋃_{i} T^{i} is already closed under the Coherence axiom, this union is the final structure.

3.10. Lemma. Consider a colimit \underrightarrow{lim} X_{i} in WHDTS such that every action u of X_{i} is used, i.e. there exists a transition (α_{i}, u_{i}, β_{i}) of X_{i}. Then every action of X is used.

Proof. By Proposition 3.9, the set of transitions of \underrightarrow{lim} X_{i} is obtained by taking the closure under the Coherence axiom of the union of the transitions of the X_{i}, hence the result since the set of actions of \underrightarrow{lim} X_{i} is the union of the actions of the X_{i}.

\xymatrix{C_{1}[μ(u)] \ar[dr] \ar[drr] \\  & ↑x↑ \ar[r] & X \\ C_{1}[μ(v)] \ar@{-->}[ur] \ar[urr]}

Figure 1: The crucial role of ↑x↑

3.11. Theorem. Let X ∈ WHDTS. The counit map

q_{X} : \underrightarrow{lim} ; \begin{matrix}f : C_{n}[x_{1}, …, x_{n}] → X \\ or f : ↑x↑ → X \end{matrix} dom(f) → X

where dom(f) is the domain of f is bijective on states and one-to-one on actions and transitions. Moreover, the weak HDTS X is cubical if and only if q_{X} is an isomorphism.

Proof. It is important to keep in mind that, since WHDTS is topological, the set of states (resp. of actions) of dom(q_{X}) is the colimit of the sets of states (resp. of actions) of the dom(f) for f running over the set of maps of the form C_{n}[x_{1}, …, x_{n}] → X or ↑x↑ → X for n ⩾ 0, x_{1}, …, x_{n}, x ∈ Σ.

\underline{q_{X} is one-to-one on states}. Let α and β be two states of dom(q_{X}) having the same image γ in X. Then the diagram {α} ← {γ} → {β} is a subdiagram in the colimit calculating dom(q_{X}). Hence α = γ = β in dom(q_{X}).

\underline{q_{X} is onto on states}. Let α be a state of X. Then the map C_{0}[] → X mapping the unique state of C_{0}[] to α is in the colimit calculating dom(q_{X}).

\underline{q_{X} is one-to-one on actions}. Let u and v be two actions of dom(q_{X}) having the same image w in X. By Lemma 3.10, the maps \underline{u} → dom(q_{X}) and \underline{v} → dom(q_{X}) factor as composites

\underline{u} ⟶ C_{1}[μ(u)] ⟶ dom(q_{X}) and \underline{v} ⟶ C_{1}[μ(v)] ⟶ dom(q_{X}).

One has μ(u) = μ(v) = μ(w) = x ∈ Σ by definition of a map of weak HDTS. Therefore, there exists a commutative diagram of weak HDTS like in Figure 1 Hence u = v in dom(q_{X}).

\underline{q_{X} is one-to-one on transitions}. Let (α, u_{1}, …, u_{n}, β) and (α′, u′_{1}, …, u′_{n′}, β′) be two transitions of dom(q_{X}) having the same image in X. Then one has n = n′. Since q_{X} is one-to-one on states, one gets α = α′ and β = β′. Since q_{X} is one-to-one on actions, one gets u_{i} = u′_{i} for 1 ⩽ i ⩽ n.

Let us prove now the last part of the theorem. Let X be a cubical transition system. Let u be an action of X. Then there exists a map \underline{μ(u)} → X mapping μ(u) to u. By Theorem 3.6, the latter map factors as a composite

\underline{μ(u)} ⟶ C_{1}[μ(u)] ⟶ X

since X is cubical. Hence q_{X} is onto on actions. Let (α, u_{1}, …, u_{n}, β) be a transition of X. Then there exists a map C_{n}[μ(u_{1}), …, μ(u_{n})]^{ext} → X mapping the transition

(0_{n}, (μ(u_{1}), 1), …, (μ(u_{n}), n), 1_{n})

to (α, u_{1}, …, u_{n}, β). By Theorem 3.6, the latter map factors as a composite

C_{n}[μ(u_{1}), …, μ(u_{n})]^{ext} ⟶ C_{n}[μ(u_{1}), …, μ(u_{n})] ⟶ X

since X is cubical. Hence q_{X} is onto on transitions. So q_{X} is an isomorphism. Conversely, let us suppose now that q_{X} is an isomorphism. Let f : \underline{x} → X be a map of weak HDTS. Then, by hypothesis, the action f̃(x) of X comes from an action u of dom(q_{X}). The corresponding map \underline{x} = \underline{μ(u)} → dom(q_{X}) factors as a composite

\underline{x} = \underline{μ(u)} ⟶ C_{1}[μ(u)] ⟶ dom(q_{X})

by construction of q_{X}. Hence X is injective with respect to the maps \underline{x} → C_{1}[x] for x ∈ Σ. Let g : C_{n}[x_{1}, …, x_{n}]^{ext} → X be a map of weak HDTS. Then, by hypothesis, the transition (g_{0}(0_{n}), g̃(x_{1}, 1), …, g̃(x_{n}, n), g_{0}(1_{n})) of X comes from a transition (α, u_{1}, …, u_{n}, β) of dom(q_{X}). The corresponding map C_{n}[μ(u_{1}), …, μ(u_{n})]^{ext} → dom(q_{X}) factors as a composite

C_{n}[μ(u_{1}), …, μ(u_{n})]^{ext} ⟶ C_{n}[μ(u_{1}), …, μ(u_{n})] ⟶ dom(q_{X})

by construction of q_{X}. Hence X is injective with respect to the maps

C_{n}[μ(u_{1}), …, μ(u_{n})]^{ext} ⟶ C_{n}[μ(u_{1}), …, μ(u_{n})].

So by Theorem 3.6, the weak HDTS X is cubical.

3.12. Corollary. The full subcategory of CTS generated by the cubes C_{n}[x_{1}, …, x_{n}] for n ⩾ 0 and x_{1}, …, x_{n} ∈ Σ and by the weak HDTS ↑x↑ for x ∈ Σ is dense in CTS.

3.13. Definition. Let X ∈ WHDTS. The cubification functor is the functor

\underline{Cub} : WHDTS ⟶ WHDTS

defined by

\underline{Cub} = \underrightarrow{lim}_{C_{n}[x_{1},...,x_{n}]→X} C_{n}[x_{1}, …, x_{n}].

Denote by p_{X} : \underline{Cub}(X) → X the canonical map.

\{ C_{1}[x] ⊔ C_{1}[x]) ; ⟶^{x_{1}} ; ⟶^{x_{2}} ⟶^{p_{x}} \{ \underrightarrow{lim}(C_{1}[x] ← \underline{x} → C_{1}[x]) ; ⟶^{x} ; ⟶^{x}

Figure 2: Monomorphism in CTS with μ(x_{1}) = μ(x_{2}) = x

The full subcategory generated by the cubes C_{n}[x_{1}, …, x_{n}] for n ⩾ 0 and x_{1}, …, x_{n} ∈ Σ is not a dense, and even not a strong generator of CTS. It is not a dense generator since the weak HDTS ↑x↑ is not a colimit of cubes. Indeed, the canonical map

C_{1}[x] ⊔ C_{1}[x] ≅ \underline{Cub}(↑x↑) ⟶ ↑x↑

is not an isomorphism. The left-hand weak HDTS contains two distinct actions x_{1} and x_{2} labelled by x, whereas the right-hand one contains only one action x. It is not a strong generator either since the canonical map (cf. Figure 2)

\underline{Cub}(↑x↑) ⟶ ↑x↑

is a monomorphism in CTS ^{3} and since every map C_{n}[x_{1}, …, x_{n}] → ↑x↑ factors as a composite C_{n}[x_{1}, …, x_{n}] → C_{1}[x] ⊔ C_{1}[x] → ↑x↑ (n is necessarily equal to 1).

3.14. Remark. The map of Figure 2 is also an epimorphism.

3.15. Corollary. The category CTS is a coreflective locally finitely presentable subcategory of WHDTS.

Proof. The right adjoint to the inclusion functor CTS ⊂ WHDTS is the functor X ↦ dom(q_{X}) by Proposition 3.8. The category is therefore cocomplete with set of dense (and therefore strong) finitely presentable generators the cubes C_{n}[x_{1}, …, x_{n}] for n ⩾ 0 and x_{1}, …, x_{n} ∈ Σ and the weak HDTS ↑x↑ for x ∈ Σ. The category CTS is therefore locally finitely presentable by [AR94, Theorem 1.20].

3.16. Definition. Let n ⩾ 1 and x_{1}, …, x_{n} ∈ Σ. Let ∂C_{n}[x_{1}, …, x_{n}] be the weak HDTS defined by removing from its set of transitions all n-transitions. It is called the boundary of C_{n}[x_{1}, …, x_{n}].

The weak HDTS ∂C_{2}[x_{1}, x_{2}] is not a colimit of cubes but is cubical: it is obtained by identifying states in the cubical transition system ↑x_{1}↑ ⊔ ↑x_{2}↑.

3It is not a monomorphism in WHDTS: the precompositions by \underline{x} → C_{1}[x] ⊔ C_{1}[x] mapping x to x_{1} and to x_{2} give the same result.

4. About combinatorial model categories

4.1. Definition. [AHRT02] Let K be a locally presentable category. A weak factorization system is a pair (L, R) of classes of morphisms of K such that inj_{K}(L) = R and such that every morphism of K factors as a composite r ∘ ℓ with ℓ ∈ L and r ∈ R. The weak factorization system is functorial if the factorization r ∘ ℓ can be made functorial.

For every set of maps I of a locally presentable category K, the pair of classes of maps (cof_{K}(I), inj_{K}(I)) is a weak factorization system by [Bek00, Proposition 1.3]. A weak factorization system of the form (cof_{K}(I), inj_{K}(I)) is said small, or generated by I. A small weak factorization system is necessarily functorial.

For every weak factorization system (L, R), the class of maps L is closed under retract, pushout and transfinite composition.

4.2. Definition. [Hov99] A combinatorial model category is a locally presentable category equipped with three classes of morphisms (C, F, W) (resp. called the classes of cofibrations, fibrations and weak equivalences) such that:

1. the class of morphisms W is closed under retracts and satisfies the two-out-of-three axiom i.e.: if f and g are morphisms of K such that g ∘ f is defined and two of f, g and g ∘ f are weak equivalences, then so is the third.

2. the pairs (C ∩ W, F) and (C, F ∩ W) are both small weak factorization systems. So there exist two sets of maps I and J such that (C, F ∩ W) = (cof_{K}(I), inj_{K}(I)) and (C ∩ W, F) = (cof_{K}(J), inj_{K}(J)).

The triple (C, F, W) is called a model category structure. An element of C ∩ W is called a trivial cofibration. An element of F ∩ W is called a trivial fibration. A map of I is called a generating cofibration and a map of J a generating trivial cofibration.

There exists at most one model category structure (C, F, W) for a given class of cofibrations C and a given class of weak equivalences W. Indeed, the class of cofibrations determines the class of trivial fibrations, and the intersection of the classes of cofibrations and of weak equivalences determines the class of fibrations.

An object X is cofibrant (fibrant resp.) if the canonical map ∅ → X (X → 1) is a cofibration (fibration resp.). A model category is left proper if the pushout along a cofibration of a weak equivalence is a weak equivalence. By a well-know theorem due to C. L. Reedy [Ree74], every model category such that every object is cofibrant is left proper (e.g., [Hir03, Corollary 13.1.3]).

For every object X of a model category, the canonical map ∅ → X (X → 1 resp.) factors as a composite 0 → X^{cof} → X (X → X^{fib} → 1 resp.) where X^{cof} is cofibrant and X^{cof} → X is a trivial fibration (X^{fib} is fibrant and X → X^{fib} is a trivial cofibration resp.). X^{cof} (X^{fib} resp.) is called the cofibrant (fibrant resp.) replacement functor.

4.3. Definition. [Cis02, Definition 3.4] Let A be a class of morphisms of a category K. A class of maps W satisfying the two-out-of-three axiom, such that inj_{K}(A) ⊂ W and such that A ∩ W is closed under pushout and transfinite composition is called a A-localizer, or a localizer with respect to A.

The class of all maps of K is clearly an A-localizer and the intersection of any family of A-localizers is a A-localizer. Therefore there exists a smallest A-localizer containing a given set of maps S denoted by W_{A}^{K}(S), or W_{A}(S) if there is no ambiguity (once again, K will be always omitted if K = WHDTS).

Let K be a locally presentable category. Let A be a class of morphisms of K. There exists at most one model structure on K such that A is the class of cofibrations and such that W_{A}(∅) is the class of weak equivalences since the class of trivial cofibrations is then completely known and by definition of a weak factorization system, the classes of fibrations and trivial fibrations are determined as well. When it exists, it is called the left determined model structure with respect to A [RT03]. Note that the existence of this model structure implies that W_{A}(∅) is closed under retract. However, this hypothesis is not in the definition of a localizer.

4.4. Definition. [KR05] A very good cylinder of a weak factorization system (L, R) in a locally presentable category K is a functorial factorization of the codiagonal X ⊔X → X as a composite

\xymatrix{X ⊔ X \ar[r]^{γ_{X}} & Cyl(X) \ar[r]^{σ_{X}} & X}

with γ_{X} ∈ L and σ_{X} ∈ R. Two maps f, g : X ⇉ Y are homotopy equivalent if the pair (f, g) belongs to the symmetric transitive closure of the binary relation f ∼ g whenever the map f ⊔ g : X ⊔ X → Y factors as a composite

\xymatrix{X ⊔ X \ar[r]^{γ_{X}} & Cyl(X) \ar[r]^{H} & Y.}

The homotopy relation does not depend on the choice of a very good cylinder by [KR05, Observation 3.3].

The adjective very good (meaning that σ_{X} ∈ R) is not used in [KR05]. The adjective final is used in [Ols09]. The terminology of [DS95, Definition 4.2] seems to be better to avoid any confusion with the notion of final structure in a topological category.

4.5. Notation. The two composites

\xymatrix{X ⊂ X ⊔ X \ar[r]^{γ_{X}} & Cyl(X)}

are denoted by γ_{X}^{0} and γ_{X}^{1}.

4.6. Notation. For every map f : X → Y and every natural transformation α : F ⇒ F′ between two endofunctors of K, the map f ⋆ α is the canonical map

f ⋆ α : F Y ⊔_{F X} F′X ⟶ F′Y

induced by the commutative diagram of solid arrows

\xymatrix{F X \ar[r]^{α_{X}} \ar[d]_{F f} & F′X \ar[d]_{F′f} \\ F Y \ar[r]^{α_{Y}} & F′Y}

and the universal property of the pushout.

4.7. Definition. [Ols09, Definition 3.8] A very good cylinder of a weak factorization system (L, R) in a locally presentable category K is cartesian if the cylinder functor Cyl : K → K is a left adjoint and if one has the inclusions L ⋆ γ ⊂ L and L ⋆ γ^{k} ⊂ L for k = 0, 1.

A cylinder of a model category is a very good cylinder for the weak factorization system formed by the cofibrations and the trivial fibrations.

Let us conclude the section by recalling well-known Smith’s theorem generating model structures on locally presentable categories.

4.8. Theorem. (Smith) Let I be a set of morphisms of a locally presentable category K. Let W be an accessible accessibly-embedded cof_{K}(I)-localizer closed under retracts. Then there exists a cofibrantly generated model structure on K with class of cofibrations cof_{K}(I), with class of fibrations inj_{K}(cof_{K}(I) ∩ W), and with class of weak equivalences W.

Sketch of Proof. The class W satisfies the solution set condition by [AR94, Corollary 2.45]. Hence the existence of the model structure by Smith’s theorem [Bek00, Theorem 1.7].

The Bousfield localization of a model category M by a class of maps A is a model category L_{A}M with the same underlying category, the same class of cofibrations, together with a map of model categories ^{4} M → L_{A}M such that every map of model categories M → N taking the cofibrant replacement of every map of A to a weak equivalence of N factors uniquely as a composite M → L_{A}M → N. The properties of this object used in this paper are listed now:

1. The Bousfield localization of a left proper combinatorial model category with respect to any set of maps always exists and is left proper combinatorial [Ros09] [Lur09] [Hir03, Theorem 3.3.19].

2. A weak equivalence between two cofibrant-fibrant objects in L_{A}M is a weak equivalence of M [Hir03, Theorem 3.2.13].

4i.e. a left adjoint preserving cofibrations and trivial cofibrations

By Bousfield localization of M with respect to a functor F : M → M preserving weak equivalences, it is meant the Bousfield localization with respect to the class of maps f such that F (f) is a weak equivalence.

5. The left determined model category of weak HDTS

The purpose of this section is the proof of the existence of the left determined model structure with respect to the cofibrations of weak HDTS defined as follows:

5.1. Definition. A cofibration of weak HDTS is a map of weak HDTS inducing an injection between the set of actions.

Note that the class of cofibrations is strictly bigger than the class of monomorphisms of WHDTS since R : {0, 1} → {0} is a cofibration of weak HDTS. We do not know if there is a link between this fact and the existence of an analogous cofibration on the model category of flows introduced in [Gau03].

5.2. Proposition. The class of cofibrations of weak HDTS is closed under pushout, transfinite composition and retract.

Proof. Since the functor ω : WHDTS ⟶ Set^{{s}∪Σ} is topological, it is colimit preserving. So it suffices to observe that the class of injections in the category of sets is closed under retract, pushout and transfinite composition, for example by considering the weak factorization system of the category of sets (cof_{Set}(C), inj_{Set}(C)) where C : ∅ ⊂ {0} denotes the inclusion.

5.3. Notation. Let I be the set of maps C : ∅ → \{0\}, R : \{0, 1\} → \{0\}, ∅ ⊂ \underline{x} for x ∈ Σ and \{0_{n}, 1_{n}\} ⊔ \underline{x_{1}} ⊔ ⋯ ⊔ \underline{x_{n}} ⊂ C_{n}[x_{1}, …, x_{n}]^{ext} for n ⩾ 1 and x_{1}, …, x_{n} ∈ Σ.

5.4. Proposition. One has cell(I) = cof(I) and this class of maps is the class of cofibrations of weak HDTS.

Proof. Every map of I is a cofibration of weak HDTS. Since I is a set, the class of maps cof(I) is the closure under retract of transfinite composition of pushouts of elements of I. So cell(I) ⊂ cof(I) and by Proposition 5.2, every map of cof(I) is a cofibration of weak HDTS. It then suffices to prove that every cofibration of weak HDTS belongs to cell(I).

Let f : X = (S, μ : L → Σ, T) → X′ = (S′, μ′ : L′ → Σ, T′) be a cofibration of weak HDTS. The set map f_{0} : S → S′ factors as a composite S → f_{0}(S) ⊂ S′. The left-hand map is a transfinite composition of pushouts of R : {0, 1} → {0}. The inclusion f_{0}(S) ⊂ S′ is a transfinite composition of pushouts of C : ∅ → {0}. By hypothesis, the set map f̃: L → L′ is one-to-one. Consider the pushout diagram of weak HDTS

[figure: S ⊔ (⨆_{u∈L} \underline{μ(u)}); ⊂; f⊔f̃; X; S′ ⊔ (⨆_{u∈L′} \underline{μ′(u)}); Y.]

The universal property of the pushout yields a map of weak HDTS g : Y → X′ such that g_{0} and g̃ are bijections. Consider the pushout diagram of weak HDTS

[figure: ⨆_{(α,u_{1},...,u_{n},β)∈T′\T}(\{0_{n}, 1_{n}\} ⊔ \underline{μ′(u_{1})} ⊔ ⋯ ⊔ \underline{μ′(u_{n})}); \begin{matrix}0_{n} ↦ α \\ 1_{n} ↦ β \\ μ′(u_{i}) ↦ μ′(u_{i}) \end{matrix}; Y; ⨆_{(α,u_{1},...,u_{n},β)∈T′\T} C_{n}[μ′(u_{1}), …, μ′(u_{n})]^{ext}; Z.]

The universal property of the pushout yields a map h : Z → X′ such that h_{0} and h̃ are bijections. So the set of transitions of Z can be identified with a subset of the set of transitions of X′. By construction, the map h induces an onto map between the set of transitions. So h is an isomorphism of weak HDTS and cell(I) = cof(I).

The terminal object 1 of WHDTS is described as follows: the set of states is {0}, the set of actions is Σ, the labelling map is the identity of Σ and the set of transitions is ⋃_{n⩾1} Σ^{n}. In other terms, one has 1 ≅ ({0}, Id_{Σ}, ⋃_{n⩾1} Σ^{n}). Let V be the weak HDTS

V := ({0}, pr_{1} : Σ × {0, 1} → Σ, {0} × (⋃_{n⩾1}(Σ × {0, 1})^{n}) × {0})

V is called the segment object of WHDTS.

5.5. Proposition. Let X = (S, μ : L → Σ, T) and X′ = (S′, μ′ : L′ → Σ, T′) be two weak HDTS. The binary product X × X′ has the set of states S × S′, the set of actions L ×_{Σ} L′ = {(x, x′) ∈ L × L′, μ(x) = μ′(x′)} and the labelling map μ ×_{Σ} μ′ : L ×_{Σ} L′ → Σ. A tuple ((α, α′), (u_{1}, u′_{1}), …, (u_{n}, u′_{n}), (β, β′)) is a transition of X × X′ if and only if μ(u_{i}) = μ′(u′_{i}) for 1 ⩽ i ⩽ n with n ⩾ 1, the tuple (α, u_{1}, …, u_{n}, β) is a transition of X and (α′, u′_{1}, …, u′_{n}, β′) a transition of X′.

Proof. The forgetful functor ω : WHDTS ⟶ Set^{{s}∪Σ} is limit-preserving by [AHS06, Proposition 21.12] since it is topological. So the set of states is S × S′, the set of actions L ×_{Σ} L′ and the labelling map μ ×_{Σ} μ′ : L ×_{Σ} L′ → Σ. Consider the set T′′′ of tuples ((α, α′), (u_{1}, u′_{1}), …, (u_{n}, u′_{n}), (β, β′)) such that μ(u_{i}) = μ′(u′_{i}) for 1 ⩽ i ⩽ n with n ⩾ 1, the tuple (α, u_{1}, …, u_{n}, β) is a transition of X and (α′, u′_{1}, …, u′_{n}, β′) a transition of X′. The existence of the projections X × X′ → X and X × X′ → X′ implies that the set of transitions T′′ of X × X′ satisfies T′′ ⊂ T′′′. Let t = (α, u_{1}, …, u_{n}, β) ∈ T and t′ = (α′, u′_{1}, …, u′_{n}, β′) ∈ T′ such that μ(u_{i}) = μ′(u′_{i}) for 1 ⩽ i ⩽ n with n ⩾ 1. Let t × t′ be the weak HDTS with set of states S × S′, with set of actions L ×_{Σ} L′, with labelling map μ ×_{Σ} μ′, and with set of transitions

{((α, α′), (u_{σ(1)}, u′_{σ(1)}), …, (u_{σ(n)}, u′_{σ(n)}), (β, β′)), σ permutation of {1, …, n}}.

Since the set of transitions T′′ is given by an initial structure, the cone of weak HDTS (t × t′ → X, t × t′ → X′) induced by the projections factors uniquely by a map t × t′ → X × X′ which is the identity on the set of states and the set of actions. So T′′′ ⊂ T′′.

5.6. Proposition. Let X = (S, μ : L → Σ, T) and X′ = (S′, μ′ : L′ → Σ, T′) be two weak higher dimensional transition systems. The binary coproduct X ⊔ X′ has the set of states S ⊔ S′, the set of actions L ⊔ L′ and the labelling map μ ⊔ μ′ : L ⊔ L′ → Σ. A tuple (α, u_{1}, …, u_{n}, β) is a transition of X ⊔ X′ if and only if it is a transition of X or a transition of X′.

Proof. The forgetful functor ω : WHDTS ⟶ Set^{{s}∪Σ} is colimit-preserving by [AHS06, Proposition 21.12] since it is topological. So the set of states is S ⊔ S′, the set of actions L ⊔ L′ and the labelling map μ ⊔ μ′ : L ⊔ L′ → Σ. The disjoint union of the transitions of X and X′ is closed under the Coherence axiom. So it is equal to the set of transitions of X ⊔ X′ by Proposition 3.9.

5.7. Proposition. The canonical map 1⊔1 → 1 factors as a composite 1⊔1 ⟶ V ⟶ 1 such that the left-hand map is a cofibration and such that the right-hand map satisfies the right lifting property with respect to every cofibration.

Proof. Proposition 5.6 tells us that the set of states (resp. of actions) of 1 ⊔ 1 is the disjoint union of the set of states (resp. of actions) of 1. Let 1 ⊔ 1 → V be the map of weak HDTS defined on states by the constant set map (V has only one state) and on actions by the bijection Σ ⊔ Σ → Σ × {0, 1} taking the left-hand copy Σ to Σ × {0} and the right-hand copy of Σ to Σ × {1}. The composite 1 ⊔ 1 → V → 1 is the unique map of weak HDTS from 1 ⊔ 1 to 1. The map 1 ⊔ 1 → V is a cofibration.

Consider the commutative square of solid arrows

\xymatrix{X \ar[r]^{g} \ar[d]_{f} & V \ar[d] \\ X′ \ar[r] \ar@{-->}[ur]^{k} & 1}

where f : X → X′ is a cofibration of weak HDTS. Let X = (S, μ : L → Σ, T) and X′ = (S′, μ′ : L′ → Σ, T′). Since V has only one state, the definition of k_{0} is clear: k_{0} = 0. Since f is a cofibration, L can be identified with a subset of L′. Let k̃ : L′ → Σ × {0, 1} be the set map defined as follows:

• k̃(u) = g̃(u) if u ∈ L (we have no choice here)

• k̃(u) = (μ′(u), 0) if u ∈ L′\L.

Let (α, u_{1}, …, u_{n}, β) be a transition of X′. One always has k̃(u_{i}) ∈ {μ′(u_{i})} × {0, 1}, and necessarily k̃(u_{i}) = (μ′(u_{i}), 0) if u_{i} ∈ L′\L for every i ∈ {1, …, n}. So the set maps k_{0} and k̃ takes the transition (α, u_{1}, …, u_{n}, β) to the tuple (0, (μ′(u_{1}), ϵ_{1}), …, (μ′(u_{n}), ϵ_{n}), 0) with ϵ_{1}, …, ϵ_{n} ∈ {0, 1}. The tuple (0, (μ′(u_{1}), ϵ_{1}), …, (μ′(u_{n}), ϵ_{n}), 0) is a transition of V by definition of V. So k is a map of weak HDTS and the map V → 1 satisfies the RLP with respect to every cofibration.

5.8. Proposition. The weak HDTS V is exponentiable, i.e. the functor V × − : WHDTS → WHDTS has a right adjoint denoted by (−)^{V} : WHDTS → WHDTS.

Proof. Let Y = (S_{Y} , μ : L_{Y} → Σ, T_{Y}) be a weak HDTS. Recall that

V := ({0}, pr_{1} : Σ × {0, 1} → Σ, {0} × (⋃_{n⩾1}(Σ × {0, 1})^{n}) × {0}).

Let us describe at first the right adjoint

Y^{V} = (S^{V} , μ^{V} : L^{V} → Σ, T^{V}).

One must have the bijection of sets

WHDTS(V × {0}, Y) ≅ WHDTS({0}, Y^{V}) ≅ S^{V} .

By Proposition 5.5, one has V × {0} ≅ {0}. So necessarily there is the equality S^{V} = S_{Y}. Let x ∈ Σ. One must have the bijection of sets

WHDTS(V × \underline{x}, Y) ≅ WHDTS(\underline{x}, Y^{V}) = (μ^{V})^{−1}(x).

By Proposition 5.5 again, one has V × \underline{x} ≅ \underline{x} ⊔ \underline{x}. Therefore one has

(μ^{V})^{−1}(x) ≅ WHDTS(\underline{x} ⊔ \underline{x}, X) ≅ μ^{−1}(x) × μ^{−1}(x).

Thus, one must necessarily have L^{V} = L_{Y} ×_{Σ} L_{Y} (the fibered product of L_{Y} by itself over Σ). Finally, one must have the bijection of sets

WHDTS(V × C_{n}[x_{1}, …, x_{n}]^{ext}, Y) ≅ WHDTS(C_{n}[x_{1}, …, x_{n}]^{ext}, Y^{V})

for every x_{1}, …, x_{n} ∈ Σ. By Proposition 5.5 again, the n-transitions of Y^{V} are of the form (α, (u_{1}^{−}, u_{1}^{+}), …, (u_{n}^{−}, u_{n}^{+}), β) such that the 2^{n} tuples (α, u_{1}^{±}, …, u_{n}^{±}, β) are transitions of Y.

Let X = (S_{X}, μ : L_{X} → Σ, T_{X}) be another weak HDTS. Using Proposition 5.5 again, let us describe now the binary product X × V. The set of states of X × V is S_{X}, the set of actions is L_{X} ×_{Σ} (Σ × {0, 1}) = L_{X} × {0, 1} and a tuple (α, (u_{1}, ϵ_{1}), …, (u_{n}, ϵ_{n}), β) is a transition if and only if (α, u_{1}, …, u_{n}, β) is a transition of X.

The bijection WHDTS(X × V, Y) ≅ WHDTS(X, Y^{V}) is then easy to check.

5.9. Notation. Let Cyl(X) := X × V.

5.10. Proposition. One has cof(I)⋆γ^{0} ⊂ cof(I), cof(I)⋆γ^{1} ⊂ cof(I) and cof(I)⋆γ ⊂ cof(I).

Proof. Let f : X → X′ be a cofibration of weak HDTS. Let X = (S, μ : L → Σ, T) and X′ = (S′, μ′ : L′ → Σ, T′). The map of weak HDTS f ⋆ γ : (X′ ⊔ X′) ⊔_{X⊔X} Cyl(X) → Cyl(X′) is a cofibration since the set map { \atop f ⋆ γ} is the identity of L′ ⊔L′. The map of weak HDTS f ⋆γ^{k} : X′⊔_{X} Cyl(X) → Cyl(X′), where γ_{X}^{k} : X → Cyl(X) and γ_{X′}^{k} : X′ → Cyl(X′) are the canonical maps is a cofibration of weak HDTS since the set map { \atop f ⋆ γ^{k}} is the inclusion L ⊔ L′ → L′ ⊔ L′.

5.11. Theorem. Let S be an arbitrary set of maps of WHDTS. The triple

(cof(I), inj(cof(I) ∩ W_{cof(I)}(S)), W_{cof(I)}(S))

is a left proper combinatorial model structure of WHDTS. The segment object V is fibrant and contractible (i.e. weakly equivalent to the terminal object) for this model structure. All objects are cofibrant.

Proof. By Proposition 5.8, Proposition 5.10 and Proposition 5.7, the functor Cyl(X) = V ×X is a cartesian very good cylinder for the weak factorization system (cof(I), inj(I)). The latter weak factorization system is cofibrant, i.e. all maps ∅ → X belongs to cof(I) by Proposition 5.4. The theorem is therefore a consequence of [Ols09, Corollary 4.6].

When S = ∅, the above model structure is left determined in the sense of [RT03], i.e. the class of weak equivalences is the smallest localizer closed under retract. Indeed, W_{cof(I)}(S) is included in this smallest localizer closed under retract and it is closed under retract itself since it is the class of weak equivalences of a model category structure.

Note that the category WHDTS is distributive in the following sense:

5.12. Proposition. The category WHDTS is distributive, i.e. for every weak higher dimensional transition system X, Y and Z, there is the isomorphism (X ×Y)⊔(X ×Z) ≅ X × (Y ⊔ Z).

Proof. Since the forgetful functor WHDTS → Set^{{s}∪Σ} is topological, it preserves limits and colimits by [AHS06, Proposition 21.12]. So the canonical map (X × Y) ⊔ (X × Z) → X×(Y ⊔Z) induces a bijection between the sets of states and the sets of actions. So the set of transitions T of (X×Y)⊔(X×Z) can be identified with a subset of the set of transitions T′ of X × (Y ⊔ Z). So T ⊂ T′. By Proposition 5.5, a transition of X × (Y ⊔ Z) is of the form ((α, γ), (u_{1}, v_{1}), …, (u_{n}, v_{n}), (β, δ)) where the tuple (α, u_{1}, …, u_{n}, β) is a transition of X and where the tuple (γ, v_{1}, …, v_{n}, δ) is a transition of Y ⊔ Z. By Proposition 5.6, the transition (γ, v_{1}, …, v_{n}, δ) is then either a transition of Y or a transition of Z. So by Proposition 5.5 again, the tuple ((α, γ), (u_{1}, v_{1}), …, (u_{n}, v_{n}), (β, δ)) is either a transition of X × Y or a transition of X × Z. Thus, T′ ⊂ T.

The class of cofibrations is also stable under pullback along any map (not necessarily product projection). Therefore, [Ols09, Remark 4.7] applies here: any factorization of the codiagonal 1 + 1 → 1 as a composite 1 + 1 → W′ → 1 with the left-hand map a cofibration and the right-hand map an element of inj(I) will provide a very good cylinder.

6. The left determined model category of cubical transition systems

In this section, A is a coreflective full subcategory of WHDTS.

6.1. Theorem. Let A be a coreflective accessible subcategory of WHDTS such that:

• The class of cofibrations of WHDTS between objects of A is generated by a set, i.e. there exists a set I_{A} of maps of A such that cof_{A}(I_{A}) is this class of maps.

• The segment object V belongs to A.

• The inclusion functor A ⊂ WHDTS preserves binary products by V.

Let S be an arbitrary set of maps of A. The triple

(cof_{A}(I_{A}), inj_{A}(cof_{A}(I) ∩ W_{cof(I_{A})}^{A}(S)), W_{cof(I_{A})}^{A}(S))

is a left proper combinatorial model structure of A.

Proof. The category A is cocomplete by Proposition 3.7. Therefore it is locally presentable. So the cylinder functor X ↦ V × X is a left adjoint. The proof then goes as for that of Theorem 5.11. The latter theorem is in fact the particular case A = WHDTS.

When S = ∅, the above model structure is left determined in the sense of [RT03], i.e. the class of weak equivalences is the smallest localizer closed under retract.

6.2. Notation. Let Λ_{A}(Cyl, S, I_{A}) be the set of maps:

• Λ_{A}^{0}(Cyl, S, I_{A}) = S ∪ (I_{A} ⋆ γ^{0}) ∪ (I_{A} ⋆ γ^{1})

• Λ_{A}^{n+1}(Cyl, S, I_{A}) = Λ_{A}^{n}(Cyl, S, I_{A}) ⋆ γ • Λ_{A}(Cyl, S, I_{A}) = ⋃_{n⩾0} Λ_{A}^{n}(Cyl, S, I_{A}).

By [Ols09, Theorem 3.16, Theorem 4.5 and corollary 4.6], the class of weak equivalences W_{cof(I_{A})}^{A}(S) coincides with the class of maps denoted by W(Λ_{A}(Cyl, S, I_{A})) defined as follows. A map f : X → Y of A belongs to W(Λ_{A}(Cyl, S, I_{A})) if and only if for every object T of A such that the canonical map T → 1 ∈ inj_{A}(Λ_{A}(Cyl, S, I_{A})), the induced set map

WHDTS(Y, T)/ ≃⟶ WHDTS(X, T)/ ≃

is a bijection where ≃ means the homotopy relation associated with the cylinder Cyl. Moreover, the fibrant objects of the model category of Theorem 6.1 are exactly the objects T such that T → 1 ∈ inj_{A}(Λ_{A}(Cyl, S, I_{A})).

6.3. Theorem. Let A and B be two coreflective accessible subcategories of WHDTS with A ⊂ B satisfying the hypotheses of Theorem 6.1. Let us suppose that the class of cofibrations of WHDTS between objects of A (resp. B) is generated by a set I_{A} (resp. I_{B}). Let S be an arbitrary set of maps of A. Let us equip A with the model structure

(cof_{A}(I_{A}), inj_{A}(cof_{A}(I) ∩ W_{cof(I_{A})}^{A}(S)), W_{cof(I_{A})}^{A}(S))

and B with the model structure

(cof_{B}(I_{B}), inj_{B}(cof_{B}(I) ∩ W_{cof(I_{B})}^{B}(S)), W_{cof(I_{B})}^{B}(S)).

Then the inclusion functor A ⊂ B is a left Quillen adjoint.

Proof. The two categories A and B are cocomplete by Proposition 3.7 and therefore locally presentable. Since the inclusion functor A ⊂ B preserves colimits (which are the same as the colimits of WHDTS), it is a left adjoint. it is clear that the inclusion functor takes cofibrations to cofibrations. We must prove that it takes trivial cofibrations to trivial cofibrations. It actually takes every weak equivalence to a weak equivalence. Let X → Y be a weak equivalence of A. Let T be a fibrant object of B. Then the map T → 1 satisfies the RLP with respect to any map of Λ_{A}(Cyl, S, I_{A}) ⊂ Λ_{B}(Cyl, S, I_{B}). So by adjunction, R(T) → 1 satisfies the RLP with respect to the maps of Λ_{A}(Cyl, S, I_{A}), where R(−) is the right adjoint to the inclusion functor. So R(T) is fibrant in A. Therefore the induced set map

WHDTS(Y, R(T))/ ≃⟶ WHDTS(X, R(T))/ ≃

is a bijection. So by adjunction again, X → Y is a weak equivalence of B.

We want to apply Theorem 6.1 to the case A = CTS and B = WHDTS.

6.4. Definition. A weak HDTS X satisfies the Intermediate state axiom if for every n ⩾ 2, every p with 1 ⩽ p < n and every transition (α, u_{1}, …, u_{n}, β) of X, there exists a (not necessarily unique) state ν such that both (α, u_{1}, …, u_{p}, ν) and (ν, u_{p+1}, …, u_{n}, β) are transitions.

Note that the Unique intermediate state axiom CSA2 introduced in [Gau10b] is slightly stronger than the axiom above. Indeed, it states that the intermediate states in a higher dimensional transition are unique.

6.5. Proposition. [Gau10b, Proposition 5.5] Let n ⩾ 0 and a_{1}, …, a_{n} ∈ Σ. Let X = (S, μ : L → Σ, T = ⋃_{n⩾1} T_{n}) be a weak higher dimensional transition system. Let f_{0} : {0, 1}^{n} → S and f̃ : {(a_{1}, 1), …, (a_{n}, n)} → L be two set maps. Then the following conditions are equivalent:

1. The pair (f_{0}, f̃) induces a map of weak higher dimensional transition systems from C_{n}[a_{1}, …, a_{n}] to X.

2. For every transition ((ϵ_{1}, …, ϵ_{n}), (a_{i_{1}}, i_{1}), …, (a_{i_{r}}, i_{r}), (ϵ′_{1}, …, ϵ′_{n})) of C_{n}[a_{1}, …, a_{n}] with (ϵ_{1}, …, ϵ_{n}) = 0_{n} or (ϵ′_{1}, …, ϵ′_{n}) = 1_{n}, the tuple

(f_{0}(ϵ_{1}, …, ϵ_{n}), f̃(a_{i_{1}}, i_{1}), …, f̃(a_{i_{r}}, i_{r}), f_{0}(ϵ′_{1}, …, ϵ′_{n}))

is a transition of X.

6.6. Proposition. A weak HDTS satisfies the Intermediate state axiom if and only if it is injective with respect to the maps C_{n}[x_{1}, …, x_{n}]^{ext} ⊂ C_{n}[x_{1}, …, x_{n}] for all n ⩾ 0 and all x_{1}, …, x_{n} ∈ Σ.

Recall that if a weak HDTS satisfies the Unique intermediate state axiom CSA2, not only it is injective with respect to the maps C_{n}[x_{1}, …, x_{n}]^{ext} ⊂ C_{n}[x_{1}, …, x_{n}] for all n ⩾ 0 and all x_{1}, …, x_{n} ∈ Σ, but also the factorization is unique: i.e. the weak HDTS is orthogonal to this set of maps [Gau10b, Theorem 5.6].

Proof. The proof is essentially an adaptation of the one of [Gau10b, Theorem 5.6].

\underline{Only if part}. Let X = (S, μ : L → Σ, T = ⋃_{n⩾1} T_{n}) be a weak HDTS satisfying the Intermediate state axiom. Let n ⩾ 0 and x_{1}, …, x_{n} ∈ Σ. We have to prove that the inclusion of weak HDTS C_{n}[x_{1}, …, x_{n}]^{ext} ⊂ C_{n}[x_{1}, …, x_{n}] induces an onto set map

WHDTS(C_{n}[x_{1}, …, x_{n}], X) ⟶ WHDTS(C_{n}[x_{1}, …, x_{n}]^{ext}, X).

This fact is trivial for n = 0 and n = 1 since the inclusion C_{n}[x_{1}, …, x_{n}]^{ext} ⊂ C_{n}[x_{1}, …, x_{n}] is an equality. Let f : C_{n}[x_{1}, …, x_{n}]^{ext} → X be a map of weak HDTS. The map f induces a set map f_{0} : {0_{n}, 1_{n}} → S and a set map f̃ : {(x_{1}, 1), …, (x_{n}, n)} → L. Let (ϵ_{1}, …, ϵ_{n}) ∈ [n] be a state of C_{n}[x_{1}, …, x_{n}] different from 0_{n} and 1_{n}. Then there exist (at least) two transitions

(0_{n}, (x_{i_{1}}, i_{1}), …, (x_{i_{r}}, i_{r}), (ϵ_{1}, …, ϵ_{n}))

and

((ϵ_{1}, …, ϵ_{n}), (x_{i_{r+1}}, i_{r+1}), …, (x_{i_{r+s}}, i_{r+s}), 1_{n})

of C_{n}[x_{1}, …, x_{n}] with r, s ⩾ 1. Let f_{0}(ϵ_{1}, …, ϵ_{n}) be a state of X such that

(f_{0}(0_{n}), f̃(x_{i_{1}}, i_{1}), …, f̃(x_{i_{r}}, i_{r}), f_{0}(ϵ_{1}, …, ϵ_{n}))

and

(f_{0}(ϵ_{1}, …, ϵ_{n}), f̃(x_{i_{r+1}}, i_{r+1}), …, f̃(x_{i_{r+s}}, i_{r+s}), f_{0}(1_{n}))

are two transitions of X. Since every transition from 0_{n} to (ϵ_{1}, …, ϵ_{n}) is of the form

(0_{n}, (x_{i_{σ(1)}}, i_{σ(1)}), …, (x_{i_{σ(r)}}, i_{σ(r)}), (ϵ_{1}, …, ϵ_{n}))

where σ is a permutation of {1, …, r} and since every transition from (ϵ_{1}, …, ϵ_{n}) to 1_{n} is of the form

((ϵ_{1}, …, ϵ_{n}), (x_{i_{σ′(r+1)}}, i_{σ′(r+1)}), …, (x_{i_{σ′(r+s)}}, i_{σ′(r+s)}), 1_{n})

where σ′ is a permutation of {r + 1, …, r + s}, one obtains a well-defined set map f_{0} :

[n] → S. The pair of set maps (f_{0}, f̃) induces a well-defined map of weak HDTS by Proposition 6.5. Therefore the set map

WHDTS(C_{n}[x_{1}, …, x_{n}], X) ⟶ WHDTS(C_{n}[x_{1}, …, x_{n}]^{ext}, X)

is onto.

\underline{If part}. Conversely, let X = (S, μ : L → Σ, T = ⋃_{n⩾1} T_{n}) be a weak HDTS injective to the set of inclusions {C_{n}[x_{1}, …, x_{n}]^{ext} ⊂ C_{n}[x_{1}, …, x_{n}], n ⩾ 0 and x_{1}, …, x_{n} ∈ Σ}. Let (α, u_{1}, …, u_{n}, β) be a transition of X with n ⩾ 2. Then there exists a (unique) map C_{n}[μ(u_{1}), …, μ(u_{n})]^{ext} ⟶ X taking the transition (0_{n}, (μ(u_{1}), 1), …, (μ(u_{n}), n), 1_{n}) to the transition (α, u_{1}, …, u_{n}, β). By hypothesis, this map factors as a composite

C_{n}[μ(u_{1}), …, μ(u_{n})]^{ext} ⊂ C_{n}[μ(u_{1}), …, μ(u_{n})] ⟶^{g} X.

Let 1 ⩽ p < n. There exists a (unique) state ν of C_{n}[μ(u_{1}), …, μ(u_{n})] such that the tuples (0_{n}, (μ(u_{1}), 1), …, (μ(u_{p}), p), ν) and (ν, (μ(u_{p+1}), p + 1), …, (μ(u_{n}), n), 1_{n}) are two transitions of the HDTS C_{n}[μ(u_{1}), …, μ(u_{n})] by Proposition 2.6. Hence the existence of a state g_{0}(ν) of X such that the tuples (α, u_{1}, …, u_{p}, g_{0}(ν)) and (g_{0}(ν), u_{p+1}, …, u_{n}, β) are two transitions of X. Thus, the weak HDTS X satisfies the Intermediate state axiom.

6.7. Proposition. A weak HDTS is a cubical transition system if and only if it satisfies the Intermediate state axiom and every action u is used in at least one 1-transition (α, u, β).

Proof. The statement is a corollary of Proposition 6.6 and Theorem 3.6.

6.8. Corollary. There exists a left determined model structure with respect to the class of cofibrations between cubical transition systems. The adjunction CTS ⇆ WHDTS is a Quillen adjunction. All objects of CTS are cofibrant.

Proof. The class of cofibrations between cubical transition systems is generated by a set I^{CTS} by Theorem A.5. The segment V is cubical by Proposition 6.7. The other hypotheses of Theorem 6.1 are easy to check. Hence the proof is complete.

Proposition 6.6 has a consequence which will not be used in the paper but which is worth mentioning anyway. This is about an explicit description of the coreflector from WHDTS to CTS.

6.9. Definition. Let X be a weak HDTS. A (n + 1)-transition (α, u_{1}, …, u_{n+1}, β) of X is divisible if either n = 0 or there exists a state γ such that the tuples (α, u_{1}, …, u_{p}, γ) and (γ, u_{p+1}, …, u_{n+1}, β) are two divisible transitions of X for some p ⩾ 1.

6.10. Proposition. Let X be a weak HDTS. The image \overline{X} of X by the coreflector is the weak HDTS having the same states as X, having as set of actions the actions of X which are used in a 1-transition (in the sense of Lemma 3.10) and having as set of transitions the divisible transitions.

Proof. It is clear by Proposition 6.6 that all transitions of \overline{X} are divisible. Conversely, let (α, u_{1}, …, u_{n}, β) be a divisible transition of X. Then the corresponding map

C_{n}[μ(u_{1}), …, μ(u_{n})]^{ext} ⟶ X

factors as a composite

C_{n}[μ(u_{1}), …, μ(u_{n})]^{ext} ⟶ C_{n}[μ(u_{1}), …, μ(u_{n})] ⟶ X.

Therefore every divisible transition belongs to a subcube.

7. First Cattani-Sassone axiom and weakly equivalent cubical transition systems

From now on, we work in the category of cubical transition systems CTS. So cof = cof_{CTS}, inj = inj_{CTS}, cell = cell_{CTS}. The localizer (with respect to the class of cofibrations of cubical transition systems) generated by a set S is denoted by W(S).

We want to characterize the weak equivalences of the left determined model structure of cubical transition systems. The following axiom, introduced in [Gau10b], will be useful.

7.1. Definition. A cubical transition system satisfies the First Cattani-Sassone axiom (CSA1) if for every transition (α, u, β) and (α, u′, β) such that the actions u and u′ have the same label in Σ, one has u = u′.

The axiom CSA1 used by Cattani and Sassone in their paper [CS96] is even stronger, but we do not need this stronger form. In our language, their stronger form states that if (α, u_{1}, …, u_{n}, β) and (α, u′_{1}, …, u′_{n}, β) are two n-dimensional transitions with μ(u_{i}) = μ(u′_{i}) for 1 ⩽ i ⩽ n, then one has (α, u_{1}, …, u_{n}, β) = (α, u′_{1}, …, u′_{n}, β).

7.2. Proposition. The full subcategory of cubical transition systems satisfying CSA1 is a full reflective subcategory of CTS.

Proof. The full subcategory of cubical transition systems satisfying CSA1 is a smallorthogonality class of CTS. Indeed a cubical transition system satisfies CSA1 if and only if it is orthogonal to the set of maps C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x] ⟶ C_{1}[x] for x running over Σ. The proof goes exactly as in [Gau10b, Corollary 5.7].

7.3. Notation. Let us denote by CSA_{1} the reflector.

7.4. Proposition. Let Y be a cubical transition system satisfying CSA1. Let X be a cubical transition system. Then two homotopy equivalent maps f, g : X → Y are equal. In other terms, each of the two canonical maps X → X × V induces a bijection CTS(X × V, Y) ≅ CTS(X, Y).

Proof. The cubical transition system X ×V is calculated in the proof of Proposition 5.8. Let us recall the results. The cubical transition system X ×V and X have the same states. If L is the set of actions of X, then L×{0, 1} is the set of actions of X ×V and the labelling map is the composite L × {0, 1} → L → Σ. Finally, a tuple (α, (u_{1}, ϵ_{1}), …, (u_{n}, ϵ_{n}), β) for ϵ_{1}, …, ϵ_{n} ∈ {0, 1} is a transition of X × V if and only if the tuple (α, u_{1}, …, u_{n}, β) is a transition of X.

Let us consider a homotopy H : X × V → Y between two maps f and g from X to Y. Since X × V and X have the same states, f_{0} = g_{0} = H_{0}, i.e. f and g coincide on states. Let u be an action of X. Since X is injective with respect to the map \underline{μ(u)} ⟶ C_{1}[μ(u)] by Theorem 3.6, there exists a transition (α, u, β) of X. So the tuples (α, (u, 0), β) and (α, (u, 1), β) are two transitions of X × V. Therefore (H_{0}(α), H̃(u, 0), H_{0}(β)) and (H_{0}(α), H̃(u, 1), H_{0}(β)) are two transitions of Y. By CSA1, one has f̃(u) = H̃(u, 0) = H̃(u, 1) = g̃(u). Hence f = g.

7.5. Corollary. Let T be a cubical transition system satisfying CSA1. Then there is the canonical isomorphism T^{V} ≅ T in CTS ^{5}

7.6. Proposition. Let T be a cubical transition system such that T^{V} ≅ T (in CTS). Then one has:

1. T is orthogonal to every map of the form f ⋆ γ^{ϵ} with ϵ = 0, 1 and with f any map of cubical transition systems.

2. T is injective with respect to a map of the form f ⋆ γ with f a map of cubical transition systems if and only if for every diagram of the form

\xymatrix{X \ar[r]^{g} \ar[d]^{f} & T \\ Y \ar@{-->}[ur]_{k}}

there exists at most one lift k.

3. T is injective with respect to every map of the form f ⋆ γ with f a map of cubical transition systems such that f_{0} and f̃ are onto ^{6}.

5The weak HDTS (T^{V})^{WHDTS} (the right adjoint being calculated in WHDTS) is not isomorphic to T; the calculations in the proof of Proposition 5.8 show that the two weak HDTS have a different set of actions, L ×_{Σ} L for (T^{V})^{WHDTS} if L is the set of actions of T.

6In fact, this assertion holds whenever f is an epimorphism.

4. T is injective with respect to every map of the form (f ⋆ γ) ⋆ γ where f is a map of cubical transition systems.

Proof. By adjunction, T is injective with respect to a map of the form f ⋆ γ^{ϵ} if and only if f satisfies the LLP with respect to the map π_{ϵ} : T^{V} → T which is an isomorphism. Hence the first assertion.

By adjunction again, T is injective with respect to a map of the form f ⋆ γ if and only if f satisfies the LLP with respect to the canonical map π : T^{V} → T × T which turns out to be the diagonal. Two lifts k_{1} and k_{2} in the diagram

\xymatrix{X \ar[r]^{g} \ar[d]^{f} & T \\ Y \ar@{-->}[ur]_{k_{1},k_{2}}}

give rise to the commutative diagram of solid arrows

\xymatrix{X \ar[r]^{g} \ar[d]_{f} & T^{V} \ar[d] \\ Y \ar[r]^{(k_{1},k_{2})} \ar@{-->}[ur]^{k} & T × T.}

One deduces k_{1} = k = k_{2}. Conversely, let us suppose that there is always at most one lift k in the diagram

\xymatrix{X \ar[r]^{g} \ar[d]^{f} & T \\ Y \ar@{-->}[ur]_{k}}

Consider a commutative diagram of solid arrows of the form

\xymatrix{X \ar[r]^{g} \ar[d]_{f} & T^{V} ≅ T \ar[d] \\ Y \ar[r]^{(k_{1},k_{2})} & T × T.}

Then k_{1} = k_{2} and therefore T is (f ⋆ γ)-injective. Hence the second assertion.

Let us suppose now that f is a map of cubical transition systems such that f_{0} and f̃ are onto. Let k_{1} and k_{2} be two lifts. Then ω(k_{1})ω(f) = ω(g) = ω(k_{2})ω(f). So ω(k_{1}) = ω(k_{2}). Since the forgetful functor ω is faithful, one deduces that k_{1} = k_{2}. Hence the third assertion.

Let f : X → X′ be a map of cubical transition systems with X = (S, μ : L → Σ, T) and X′ = (S′, μ′ : L′ → Σ, T′). The map f ⋆γ is obtained by considering the commutative diagram of solid arrows

\xymatrix{X ⊔ X \ar[d] \ar[r] & Cyl(X) \ar[d] \\ X′ ⊔ X′ \ar[r] & Cyl(X′)}

and by using the universal property of the pushout, giving the map

f ⋆ γ : (X′ ⊔ X′) ⊔_{X⊔X} Cyl(X) ⟶ Cyl(X′)

The latter map induces on the set of states the map (S′ ⊔ S′) ⊔_{S⊔S} S ≅ S′ ⊔_{S} S′ → S′ which is onto, and on the set of actions the map (L′ ⊔ L′) ⊔_{L⊔L} (L ⊔ L) ≅ L′ ⊔ L′ → L′ ⊔ L′ which is onto as well. So the fourth assertion is a consequence of the third one.

7.7. Proposition. Let S be a set of maps of cubical transition systems. Let T be a cubical transition system satisfying CSA1. Then T is Λ(Cyl, S, I^{CTS})-injective if and only if T is S-orthogonal.

Proof. If T is Λ(Cyl, S, I^{CTS})-injective, then it is Λ^{0}(Cyl, S, I^{CTS})-injective, and therefore S-injective. Such a T is also Λ^{1}(Cyl, S, I^{CTS})-injective with

Λ^{1}(Cyl, S, I^{CTS}) = Λ^{0}(Cyl, S, I^{CTS}) ⋆ γ.

Therefore T is S-orthogonal by Proposition 7.6 (2). Conversely, let us suppose that T is S-orthogonal. Then T is Λ^{0}(Cyl, S, I^{CTS})-injective by Proposition 7.6 (1). By Proposition 7.6 (2) and (1), T is Λ^{1}(Cyl, S, I^{CTS})-injective as well. The injectivity with respect to Λ^{n}(Cyl, S, I^{CTS}) for n ⩾ 2 is a consequence of Proposition 7.6 (4).

Hence the theorems:

7.8. Proposition. Every cubical transition system satisfying CSA1 is fibrant in the left determined model structure of CTS.

Proof. The statement is a corollary of Proposition 7.7 with S = ∅.

7.9. Proposition. Two cubical transition systems satisfying CSA1 are weakly equivalent if and only if they are isomorphic.

Proof. Let f : X → Y be a weak equivalence between two cubical transition systems satisfying CSA1. Since X and Y are both cofibrant and fibrant by Proposition 7.8, there exists a map g : Y → X such that f ∘ g is homotopy equivalent to Id_{Y} and such that g ∘ f is homotopy equivalent to Id_{X}. So by Proposition 7.4, f ∘ g = Id_{Y} and g ∘ f = Id_{X}. Hence X and Y are isomorphic.

7.10. Theorem. The reflector CSA_{1} detects the weak equivalences of the left determined model structure of CTS. In other terms, a map f of cubical transition systems is a weak equivalence in the left determined model structure of CTS if and only if CSA_{1}(f) is an isomorphism.

In particular, this theorem means that two cubical transition systems interpreting two process names in a process algebra are weakly equivalent in this model structure if and only if they are isomorphic. See [Gau10b] for further details.

Proof. By Proposition 7.9, it suffices to prove that for every cubical transition system X, the unit X → CSA_{1}(X) is a weak equivalence in the left determined model structure of CTS. An object X is orthogonal to a map of the form C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x] ⟶ C_{1}[x] for x ∈ Σ if and only if it is injective with respect to it since this map is an epimorphism. So the map X → CSA_{1}(X) is obtained by factoring the canonical map X → 1 (from X to the terminal object) as a composite X → CSA_{1}(X) → 1 where the left-hand map belongs to cell_{CTS}(U) and the right-hand map belongs to inj_{CTS}(U) where

U = {C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x] ⟶ C_{1}[x] | x ∈ Σ}.

So it suffices to prove that every pushout of a map of the form C_{1}[x]⊔_{{0_{1},1_{1}}} C_{1}[x] → C_{1}[x] for x ∈ Σ is a weak equivalence of the left determined model structure of CTS. The identity of C_{1}[x] factors as a composite

C_{1} ⟶ C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x] ⟶ C_{1}[x].

By the calculation made in the proof of Proposition 5.8, there is the isomorphism C_{1}[x] × V ≅ C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x]. Hence the left-hand map is a weak equivalence, and also the right-hand map by the two-out-of-three axiom. Consider a pushout diagram of the form

[figure: C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x]; ϕ; X; f; C_{1}[x]; Y]

The cubical transition system C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x] contains two actions x_{1} and x_{2} labelled by x. There are two mutually exclusive cases. Either ϕ̃(x_{1}) = ϕ̃(x_{2}) or ϕ̃(x_{1}) ≠ ϕ̃(x_{2}). In the first case, the commutative square above factors as a composite of commutative squares

[figure: C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x]; ϕ; C_{1}[x]; X; f; C_{1}[x]; C_{1}[x]; Y]

Hence X ≅ Y. In the second case, ϕ is one-to-one on actions, i.e. a cofibration of cubical transition systems. In that case, f is a weak equivalence since the left determined model structure of CTS is left proper. So the map X → CSA_{1}(X) is a transfinite composition of weak equivalences. The class of weak equivalences of a combinatorial model category is always accessible accessibly-embedded by e.g. [Lur09, Corollary A.2.6.6]. Hence a transfinite composition of weak equivalences is always a weak equivalence. The proof is complete.

7.11. Corollary. The counit map p_{x} : \underline{Cub}(↑x↑) ⟶ ↑x↑ is not a weak equivalence in the left determined model structure of CTS.

Corollary 7.11 shows that this model structure is really minimal. Even cubical transition systems having the same cubes may be not weakly equivalent. The next section explains how it is possible to add weak equivalences so that two cubical transition systems containing the same cubes after simplification of the labelling are always weakly equivalent.

8. Bousfield localization with respect to the cubification functor

Let us denote by W\underline{Cub} the smallest localizer generated by the class of maps of cubical transition systems f : X → Y such that \underline{Cub}(f) is a weak equivalence in the left determined model structure of CTS. We want to prove that it is small, more precisely that it is generated by the set of maps S = {p_{x} : C_{1}[x] ⊔ C_{1}[x] → ↑x↑ | x ∈ Σ}.

Let us prove first that the two functors \underline{Cub}(−) and CSA_{1}(−) commute with one another.

8.1. Proposition. Let X be a cubical transition system. Then there exists a natural isomorphism CSA_{1}(\underline{Cub}(X)) ≅ \underline{Cub}(CSA_{1}(X)).

Proof. That CSA_{1}(X) satisfies CSA1 means that for every x ∈ Σ, the map C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x] → C_{1}[x] induces a bijection

CTS(C_{1}[x], CSA_{1}(X)) ≅ CTS(C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x], CSA_{1}(X)).

By Proposition 3.8, the functor \underline{Cub} is right adjoint to the inclusion functor of the full subcategory of CTS generated by the cubes C_{n}[x_{1}, …, x_{n}] for n ⩾ 0 and x_{1}, …, x_{n} ∈ Σ into CTS. Both C_{1}[x] and C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x] are colimits of cubes. Therefore one has the bijections

CTS(C_{1}[x] ⊔_{\{0_{1},1_{1}\}} C_{1}[x], \underline{Cub}(CSA_{1}(X)))
≅ CTS(C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x], CSA_{1}(X))  by adjunction
≅ CTS(C_{1}[x], CSA_{1}(X))  since CSA_{1}(X) satisfies CSA1
≅ CTS(C_{1}[x], \underline{Cub}(CSA_{1}(X)))  by adjunction again.

Hence \underline{Cub}(CSA_{1}(X)) satisfies CSA1. Therefore the canonical map

\xymatrix{\underline{Cub}(X) \ar[r]^{\underline{Cub}(ϕ_{X})} & \underline{Cub}(CSA_{1}(X))}

factors uniquely as a composite

\xymatrix{\underline{Cub}(X) \ar[r]^{ϕ_{\underline{Cub}(X)}} & CSA_{1}(\underline{Cub}(X)) \ar[r]^{ψ_{X}} & \underline{Cub}(CSA_{1}(X)).}

The functors \underline{Cub} and CSA_{1} preserve states. So the map ψ_{X} is a bijection on states. The map ψ_{X} is also surjective on actions and on transitions since any of them comes respectively from an action or a transition of \underline{Cub}(X).

It remains to understand why the map ψ_{X} is one-to-one on actions for the proof to be complete. Consider the commutative diagram of cubical transition systems of Figure 3. Since the cubical transition systems of the bottom line of Figure 3 satisfy CSA1, this square factors uniquely as a composite of commutative squares as in Figure 4. Let u_{1} and u_{2} be two actions of CSA_{1}(\underline{Cub}(X)) such that ψ_{X}(u_{1}) = ψ_{X}(u_{2}) = u. Let u′_{1} and u′_{2} be two actions of \underline{Cub}(X) such that ϕ_{\underline{Cub}(X)}(u′_{1}) = u_{1} and ϕ_{\underline{Cub}(X)}(u′_{2}) = u_{2}. Let v′_{1} = p_{X}(u′_{1}), v′_{2} = p_{X}(u′_{2}), v_{1} = CSA_{1}(p_{X})(u_{1}), v_{2} = CSA_{1}(p_{X})(u_{2}) and finally v = p_{CSA_{1}(X)}(u)^{7} By commutativity of the diagram, we obtain v_{1} = v_{2} = v. By construction of the functor CSA_{1}(−), there exist two states α and β such that the triple (α, v′_{1}, β) and (α, v′_{2}, β) are two transitions of X. Therefore by definition of \underline{Cub}, the two triples (α, u′_{1}, β) and (α, u′_{2}, β) are two transitions of \underline{Cub}(X). So u_{1} = u_{2} since CSA_{1}(\underline{Cub}(X)) satisfies CSA1.

8.2. Proposition. The functor \underline{Cub} : CTS → CTS preserves weak equivalences.

Proof. Let f be a weak equivalence of CTS. Then CSA_{1}(f) is an isomorphism by Theorem 7.10. So CSA_{1}(\underline{Cub}(f)) is an isomorphism by Proposition 8.1. Therefore by Theorem 7.10 again, \underline{Cub}(f) is a weak equivalence of CTS.

7We denote in the same way a map of cubical transition systems f and the set map f̃ between actions in order to not overload the notations.

\xymatrix{\underline{Cub}(X) \ar[r]^{p_{X}} \ar[d]_{\underline{Cub}(ϕ_{X})} & X \ar[d]_{ϕ_{X}} \\ \underline{Cub}(CSA_{1}(X)) \ar[r]^{p_{CSA_{1}(X)}} & CSA_{1}(X)}

Figure 3: Composition of \underline{Cub} and CSA_{1} (I)

[figure: \underline{Cub}(X); p_{X}; ϕ_{\underline{Cub}(X)}; X; ϕ_{X}; CSA_{1}(\underline{Cub}(X)); CSA_{1}(p_{X}); ψ_{X}; CSA_{1}(X); \underline{Cub}(CSA_{1}(X)); p_{CSA_{1}(X)}; CSA_{1}(X)]

Figure 4: Composition of \underline{Cub} and CSA_{1} (II)

8.3. Corollary. Every weak equivalence of CTS belongs to W\underline{Cub}.

8.4. Proposition. Let X be a cubical transition system. The counit p_{X} : \underline{Cub}(X) → X is a transfinite composition of pushouts of the maps p_{x} : C_{1}[x]⊔C_{1}[x] → ↑x↑ for x running over Σ.

Proof. We already know that the map p_{X} : \underline{Cub}(X) → X is bijective on states. let u be an action of X. Since X is cubical, there exists a 1-transition (α, u, β) of X, which corresponds to a map C_{1}[μ(u)] → X. Hence the map p_{X} : \underline{Cub}(X) → X is onto on actions. Let (α, u_{1}, …, u_{n}, β) be a transition of X, which corresponds to a map C_{n}[μ(u_{1}), …, μ(u_{n})]^{ext} → X. Since X is cubical, the latter map factors as a composite C_{n}[μ(u_{1}), …, μ(u_{n})]^{ext} → C_{n}[μ(u_{1}), …, μ(u_{n})] → X by Theorem 3.6. Hence the map p_{X} : \underline{Cub}(X) → X is onto on transitions. Let us factor the map p_{X} as a composite \underline{Cub}(X) → Z → X where the left-hand map belongs to cell(S) and the right-hand map belongs to inj(S). The right-hand map g : Z → X is still bijective on states, and onto on actions and transitions. Let u_{1} and u_{2} be two actions of Z mapped to the same action u of X. Then μ(u_{1}) = μ(u_{2}) = μ(u) = x. Let us suppose that the action u_{1} is used in a transition (α_{1}, u_{1}, β_{1}), and the action u_{2} in a transition (α_{2}, u_{2}, β_{2}) of Z. Then consider the commutative diagram of cubical transition systems

\xymatrix{C_{1}[x] ⊔ C_{1}[x] \ar[r] \ar[d] & Z \ar[d] \\ ↑x↑ \ar@{-->}[ur]^{ℓ} \ar[r] & X,}

where each copy of C_{1}[x] corresponds to one of the two transitions (α_{i}, u_{i}, β_{i}). The existence of the lift ℓ implies that u_{1} = u_{2}. So the map g : Z → X is one-to-one on actions. Finally, let (α, u_{1}, …, u_{n}, β) and (α′, u′_{1}, …, u′_{n}, β′) be two transitions of Z mapped to the same transition of X. Then α = α′, β = β′ and u_{i} = u′_{i} for 1 ⩽ i ⩽ n since g : Z → X is bijective on states and actions. So g is one-to-one on transitions. Therefore g is an isomorphism.

8.5. Proposition. Every map of cell(S) belongs to the localizer generated by S, i.e. cell(S) ⊂ W(S).

Proof. Note that p_{x} : C_{1}[x] ⊔ C_{1}[x] → ↑x↑ is not a cofibration so we cannot use the fact that the class of trivial cofibrations is closed under pushout and transfinite compositions. By Theorem 6.1, the class of maps W(S) is the class of weak equivalences of a model structure on CTS. It is actually the class of weak equivalences of the Bousfield localization of the left determined model structure of CTS by S. Since all objects are cofibrant, it is left proper. Consider a pushout diagram of the form

[figure: C_{1}[x] ⊔ C_{1}[x]; ϕ; p_{x}; X; ↑x↑; Y.]

There are two mutually exclusive cases. The map ϕ takes the two actions of C_{1}[x] ⊔ C_{1}[x] to two different actions. Then ϕ is a cofibration and X → Y belongs to W(S) by left properness. Or ϕ takes the two actions of C_{1}[x] ⊔ C_{1}[x] to the same action. Then X ≅ Y (the argument is similar to the one used in the proof of Theorem 7.10). So in the two cases, the right-hand vertical map belongs to W(S). The proof is complete by [Lur09, Corollary A.2.6.6] since W(S) is closed under transfinite composition.

Hence the theorem:

8.6. Theorem. One has the equality of localizers W\underline{Cub} = W(S).

Proof. The map \underline{Cub}(p_{x}) is an isomorphism by Proposition 3.7 and Proposition 3.8. So S ⊂ W\underline{Cub}. Hence the first inclusion W(S) ⊂ W\underline{Cub}. Let f : X → Y be a map of cubical transition systems such that \underline{Cub}(f) is a weak equivalence of the left determined model structure of CTS. Consider the commutative diagram

\xymatrix{\underline{Cub}(X) \ar[r]^{\underline{Cub}(f)} \ar[d] & \underline{Cub}(Y) \ar[d] \\ X \ar[r]^{f} & Y.}

The vertical maps belong to W(S) by Proposition 8.4 and Proposition 8.5. By hypothesis, the top horizontal map is a weak equivalence of CTS, and therefore belongs to W(S) as well. Hence by the two-out-of-three property, f : X → Y belongs to W(S). We obtain the second inclusion W\underline{Cub} ⊂ W(S).

8.7. Corollary. The Bousfield localization of the left determined model structure of CTS with respect to the functor \underline{Cub} exists.

The weak factorization system (cof(S), inj(S)) gives rise to a functor \underline{L}_{S} : CTS → CTS. It is defined by functorially factoring the map X → 1 as a composite X → \underline{L}_{S}(X) → 1 where the left-hand map belongs to cell(S) and the right-hand map belongs to inj(S).

8.8. Remark. The labelling map is one-to-one for every cubical transition system of the form \underline{L}_{S}(X).

A remarkable consequence of this fact is that for every map f : X → Y of cubical transition systems, the map \underline{L}_{S}(f) : \underline{L}_{S}(X) → \underline{L}_{S}(Y) is a cofibration. So \underline{L}_{S}(f) is a cofibrant replacement of f in \underline{L}_{S}(CTS) by Proposition 8.5 and Theorem 8.6.

8.9. Proposition. Every cubical transition system of inj(S) satisfies CSA1.

Proof. Let (α_{1}, u_{1}, β_{1}) and (α_{2}, u_{2}, β_{1}) be two 1-transitions of a cubical transition system injective with respect to S with μ(u_{1}) = μ(u_{2}). Then u_{1} = u_{2}, and this is still true if α_{1} = α_{2} and β_{1} = β_{2}. Hence CSA1 is satisfied.

The weak equivalences of this Bousfield localization have a nice characterization.

8.10. Theorem. A map of cubical transition systems f : X → Y belongs to W(S) if and only if \underline{L}_{S}(f) : \underline{L}_{S}(X) ≅ \underline{L}_{S}(Y) is an isomorphism. In other terms, the functor \underline{L}_{S} detects the weak equivalences of this Bousfield localization.

Proof. If \underline{L}_{S}(f) is an isomorphism, f belongs to W(S) by Proposition 8.5 and by the two-out-of-three property. Conversely, suppose that f ∈ W(S). By Proposition 8.9 and Corollary 7.5, one has \underline{L}_{S}(X)^{V} = \underline{L}_{S}(X) and \underline{L}_{S}(Y)^{V} = \underline{L}_{S}(Y). The maps of S are onto on states and actions. So by Proposition 7.7, \underline{L}_{S}(X) and \underline{L}_{S}(Y) are fibrant in the Bousfield localization since if they are orthogonal to the maps of S. By the two-out-of-three property, \underline{L}_{S}(f) is therefore a weak equivalence between two cofibrant-fibrant objects in the Bousfield localization \underline{L}_{S}(CTS) of the left determined model structure of CTS by the maps of S. By [Hir03, Theorem 3.2.13], the map \underline{L}_{S}(f) is then a weak equivalence of the left determined model structure of CTS. Since \underline{L}_{S}(X) and \underline{L}_{S}(Y) satisfy CSA1 by Proposition 8.9, the map \underline{L}_{S}(f) is an isomorphism by Theorem 7.10.

So in the Bousfield localization \underline{L}_{S}(CTS), two cubical transition systems are weakly equivalent if they have the same cubes after simplification of the labelling. It is actually possible to prove better:

8.11. Theorem. We have:

1. The functor \underline{L}_{S} : CTS → CTS induces a functor from CTS to the full reflective subcategory S^{⊥} of cubical transition systems consisting of S-orthogonal objects.

2. For every S-orthogonal cubical transition system Y, there is a natural isomorphism Y ≅ \underline{L}_{S}(Y).

3. The functor \underline{L}_{S} is left adjoint to the inclusion functor S^{⊥} ⊂ CTS.

4. Every map between S-orthogonal cubical transition systems is a cofibration of cubical transition systems. Every S-orthogonal cubical transition system is cofibrant and fibrant in \underline{L}_{S}(CTS).

5. The homotopy category of \underline{L}_{S}(CTS) is equivalent to S^{⊥}.

Proof. (1) comes from the definition of \underline{L}_{S} and from the fact that S-injective is equivalent to S-orthogonal since every map of S is an epimorphism. One has a natural isomorphism \underline{L}_{S}(Y) ≅ Y for every S^{⊥}-orthogonal cubical transition system Y since every pushout Y → Z of a map of the form p_{x} : C_{1}[x] ⊔ C_{1}[x] → ↑x↑ for x ∈ Σ is an isomorphism, hence (2). For every S^{⊥}-orthogonal cubical transition system Y, the canonical map Y → 1 satisfies the RLP with respect to every map of cell(S), in particular with respect to every map X → \underline{L}_{S}(X) for every cubical transition system X. Moreover, every map of cell(S) is bijective on states and onto on actions; so every map of cell(S) is an epimorphism. So cell(S)-injective is equivalent to cell(S)-orthogonal. This means that every map X → Y from a cubical transition system X to an S-orthogonal cubical transition system Y factors uniquely as a composite X → \underline{L}_{S}(X) → Y, hence (3). (4) is explained in the proof of Theorem 8.10. The functor \underline{L}_{S} : CTS → CTS factors uniquely as a composite CTS → \underline{L}_{S}(CTS) → S^{⊥} by Theorem 8.10 and by the universal property of the categorical localization. There is a natural isomorphism X → \underline{L}_{S}(X) in \underline{L}_{S}(CTS) by Proposition 8.5 for every object of CTS. And there is a natural isomorphism Y ≅ \underline{L}_{S}(Y) for every Sorthogonal object since S-injective is equivalent to S-orthogonal. Hence (5).

9. Weak equivalence and bisimulation

This last section sketches the link between these homotopical constructions and bisimulation. Let us introduce bisimulations with open maps as in [JNW96]. The link between bisimulation and homotopy will be the subject of future works. Indeed, the definition of open maps taken here is very restrictive since a good definition requires a more general notion of paths (cf. [Fah05] for further explanations). The purpose of this section is only to have an idea of what it is possible to do with these homotopical constructions.

Let P be a subset of the set of cubes {C_{n}[x_{1}, …, x_{n}] | n ⩾ 0, x_{1}, …, x_{n} ∈ Σ}. The elements of P are called calculation paths.

9.1. Definition. A map f : X → Y is P-open if every commutative square of solid arrows

\xymatrix{\{0_{n}\} \ar[r] \ar[d] & X \ar[d] \\ P \ar[r] \ar@{-->}[ur]^{k} & Y}

as a lift k for every P ∈ P, i.e. f satisfies the RLP with respect to the inclusion {0_{n}} ⊂ P.

9.2. Definition. Two cubical transition systems X and Y are P-bisimilar if there exists a cubical transition system A and a zig-zag of maps X ⟵^{f} A ⟶^{g} Y such that f and g are P-open.

That X and Y are P-bisimilar means that every calculation path P of P of X is simulated by a calculation path of Y and vice versa.

\xymatrix{ &  & C \ar[dl] \ar[dr] \\  & A \ar[dl] \ar[dr] &  & B \ar[dl] \ar[dr] \\ X &  & Y &  & Z}

Figure 5: Bisimulation as an equivalence relation

Bisimilarity is an equivalence relation: it is clearly symmetric, it is reflexible with X = A = Y and it is transitive since a pullback of a map satisfying the RLP with respect to a given map still satisfies the RLP and because of the diagram cartesian in C of Figure 5.

The following theorem explains the connexion with more usual (1-dimensional) notions of bisimulations [WN95].

9.3. Proposition. Take P = {C_{1}[x] | x ∈ Σ}. Let X = (S_{X}, μ : L_{X} → Σ, T_{X}) and Y = (S_{Y} , μ : L_{Y} → Σ, T_{Y}) be two cubical transition systems. Then X and Y are Pbisimilar if and only if there exists a binary relation R ⊂ S_{X} × S_{Y} satisfying the following property:

1. for every pair (α, β) ∈ R and every map c : C_{1}[x] → X with c(0_{1}) = α, there exists a map d : C_{1}[x] → Y with d(0_{1}) = β and (c(1_{1}), d(1_{1})) ∈ R

2. for every pair (α, β) ∈ R and every map d : C_{1}[x] → Y with d(0_{1}) = β, there exists a map c : C_{1}[x] → X with c(0_{1}) = α and (c(1_{1}), d(1_{1})) ∈ R.

Proof. If X ⟵^{f} A ⟶^{g} Y is a map as above, then R = {(f(α), g(α)) | α state of A} satisfies the two properties of the statement of the theorem. Conversely, suppose that such a binary relation R exists. Let X ×_{R} Y be the weak HDTS with set of states R, with set of actions the one of X × Y and such that a transition (α, u_{1}, …, u_{n}, β) of X × Y is a transition of X ×_{R} Y if and only if α and β belong to R. Then consider the image A of X ×_{R} Y by the right adjoint to the inclusion functor CTS ⊂ WHDTS:

A = \underrightarrow{lim} ; \begin{matrix}f = C_{n}[x_{1}, …, x_{n}] → X ×_{R} Y \\ or f = ↑x↑ → X ×_{R} Y \end{matrix} dom(f)

Then the composite maps A → X ×_{R} Y → X ×Y → X and A → X ×_{R} Y → X ×Y → Y satisfy the RLP with respect to any map of the form {0_{1}} ⊂ C_{1}[x] for x ∈ Σ.

9.4. Theorem. The class of P-open maps is accessible and finitely accessibly embedded in the category of maps of cubical transition systems.

Note that the following proof does not use the fact that a path is a cube. It only needs the fact that we consider a set of paths. So our very restrictive choice for the definition of a path does not matter.

Proof. That it is finitely accessibly embedded (i.e. the inclusion functor in the category of maps preserves finitely filtered colimits) comes from the finiteness of the set of states and of the set of actions of a cube. This class of maps is accessible by [Ros09, Proposition 3.3].

Note that the arity of all relation symbols of the theory axiomatizing the class of Popen maps is finite. This provides another proof of the fact that the category of P-open maps is finitely accessibly-embedded (e.g, cf. the proof of [AR94, Theorem 5.9]).

9.5. Theorem. The Bousfield localization of \underline{L}_{S}(CTS) with respect to the proper class of P-open maps exists and is a combinatorial left proper model category.

Proof. The argument is standard. By [Dug01, Proposition 7.3], there exists a regular cardinal λ_{1} such that λ_{1}-filtered colimits of weak equivalences of \underline{L}_{S}(CTS) are again weak equivalences. Let λ_{2} be a regular cardinal such that the category of P-open maps is λ_{2}-accessible. Let λ be a regular cardinal sharply bigger than λ_{1} and λ_{2}. Consider the Bousfield localization \underline{L}_{λ} \underline{L}_{S}(CTS) of \underline{L}_{S}(CTS) by a set A_{λ} of representatives of the class of λ-presentable P-open maps. Then the localization functor \underline{L}_{λ}(−) is λ-accessible. Any P-open map f is a λ-filtered colimits of maps of A_{λ}, f = \underrightarrow{lim}_{i} f_{i} by Theorem 9.4. So \underline{L}_{λ}(f) = \underrightarrow{lim}_{i} \underline{L}_{λ}(f_{i}). But for every i, the map \underline{L}_{λ}(f_{i}) is a weak equivalence of \underline{L}_{S}(CTS). Therefore \underline{L}_{λ}(f) is a weak equivalence of \underline{L}_{S}(CTS) as well. Hence every P-open map is a weak equivalence of \underline{L}_{λ} \underline{L}_{S}(CTS), and therefore the latter model category is the Bousfield localization.

Note that all maps of S are actually P-open. In this new Bousfield localization, two bisimilar cubical transition systems are weakly equivalent. This new model category will be the subject of future works.

Let us conclude this section by mentioning [BCMR11]. The class of P-open maps is axiomatized by a set of formulas such that all quantifiers are bounded. So the latter paper provides another argument for the existence of the Bousfield localization.

A. Small weak factorization system and coreflectivity

We want to prove in this section that the restriction of a small weak factorization system to a coreflective locally presentable subcategory is still small (Theorem A.5) with some additional hypotheses on the subcategory.

A.1. Lemma. Let A be a coreflective subcategory of a cocomplete category K. Let I be a set of maps of K. One has the equality inj_{K}(I) ∩ Mor(A) = inj_{A}(I) and the inclusions

cell_{A}(I) ⊂ cell_{K}(I) ∩ Mor(A) ⊂ cof_{K}(I) ∩ Mor(A) ⊂ cof_{A}(I).

Moreover if I is a set of maps of A ⊂ K, then cell_{A}(I) = cell_{K}(I) ∩ Mor(A).

Proof. obvious.

A.2. Lemma. (Compare with [Bek00, Lemma 1.8]) Let A be a coreflective subcategory of a locally presentable category K. Let I be a set of maps of K. Let J be a solution set for I, i.e. a set of maps of A such that every map i → w of Mor(K) from i ∈ I to w ∈ Mor(A) factors as a composite i → j → w with j ∈ J. Then every map f : X → Y of A can be factored as a composite X ⟶^{g} P ⟶^{h} Y with g ∈ cell_{A}(J) and h ∈ inj_{A}(I).

Proof. We want to build by transfinite induction on the ordinal λ ⩾ 0 a diagram

X =: P_{0} ⟶ P_{1} ⟶ … ⟶ P_{α} ⟶ P_{α+1} ⟶ … ⟶ P_{λ} ⟶^{h_{λ}} Y

such that the diagram P_{0} → ⋯ → P_{λ} is a transfinite composition of maps belonging to cell_{A}(J). Since P_{λ} belongs to A and since the category A is a full coreflective subcategory of K, the map h_{λ} : P_{λ} → Y is a map of A as well.

Let P_{0} = X and h_{0} = f. For a limit ordinal λ, let P_{λ} = \underrightarrow{lim}_{α<λ} P_{α}. Since the inclusion functor A ⊂ K is colimit-preserving, P_{λ} is an object of A. Let λ ⩾ 0 be an ordinal and let us suppose P_{α} constructed for α ⩽ λ. We want now to build P_{λ+1}. Let us consider the set S_{λ} of all commutative squares

\xymatrix{A \ar[r] \ar[d]_{i} & P_{λ} \ar[d]_{h_{λ}} \\ B \ar[r] & Y}

with i ∈ I. The “density hypothesis” on J means the existence of a commutative diagram

\xymatrix{A \ar[r] \ar[d]_{i} & A_{s} \ar[r]^{t_{s}} \ar[d]_{j_{s}} & P_{λ} \ar[d]_{h_{λ}} \\ B \ar[r] & B_{s} \ar[r] & Y}

with j_{s} ∈ J (so A_{s} and B_{s} both belong to A), for each square s ∈ S_{λ}. Let P_{λ+1} be the pushout diagram (in A or in K)

[figure: ⨆ A_{s}; ⨆ j_{s}; ⨆_{{ts|s∈S_{λ}}} t_{s}; P_{λ}; h_{λ+1}; ⨆ B_{s}; P_{λ+1}]

The universal property of the pushout yields a map h_{λ+1} : P_{λ+1} → Y.

Let now κ be a regular cardinal exceeding the rank of presentability of all the objects that occur as domains of maps in I. The required factorization is X → P_{κ} → Y. Indeed, consider a commutative square of solid arrows of the form

\xymatrix{A \ar[r]^{a} \ar[d]_{i} & P_{κ} \ar[d] \\ B \ar[r] \ar@{-->}[ur]^{k} & Y}

with i ∈ I. Since κ is regular, the diagram X = P_{0} → ⋯ → P_{κ} is κ-filtered and since K(A, −) commutes with κ-filtered colimits by hypothesis, the map a factors as a composite A → P_{λ} → P_{κ} for some λ < κ. Let s ∈ S_{λ} be the commutative square

\xymatrix{A \ar[r] \ar[dd]_{i} & P_{λ} \ar[d] \\  & P_{κ} \ar[d]_{h_{κ}} \\ B \ar[r] & Y.}

Then the lift k is the bottom composite

[figure: A; i; A_{s}; j_{s}; ⨆ A_{s}; ⨆ j_{s}; P_{λ}; h_{λ}; B; B_{s}; ⨆ B_{s}; P_{λ+1}; P_{κ}.]

A.3. Lemma. Let A be a coreflective subcategory of a locally presentable category K. Let I be a set of maps of K. Let J be a solution set for I which satisfies J ⊂ cof_{K}(I). Then there is the equality cof_{A}(J) = cof_{K}(I) ∩ Mor(A).

Proof. One has cell_{A}(J) ⊂ cof_{K}(I) since J ⊂ cof_{K}(I) and since A is coreflective. Since J is a set, every map of cof_{A}(J) is a retract of a map of cell_{A}(J), therefore cof_{A}(J) ⊂ cof_{K}(I) ∩ Mor(A). Conversely, let f ∈ cof_{K}(I) ∩ Mor(A). By Lemma A.2, f factors as a composite

[figure: •; f; g; •; h; •; k; •]

with g ∈ cell_{A}(J) and h ∈ inj_{A}(I). The lift k exists since f ∈ cof_{K}(I). The commutative diagram

[figure: •; f; •; g; •; f; •; k; •; h; •]

proves that f is a retract of g ∈ cell_{A}(J). Therefore f ∈ cof_{A}(J). Hence the inclusion cof_{K}(I) ∩ Mor(A) ⊂ cof_{A}(J).

We want now conclude the section by giving a sufficient condition for a small weak factorization system to restrict to a small one on a full coreflective subcategory. First we recall a definition:

A.4. Definition. [AR94, Definition 4.14] Let K be a locally presentable category. An object K is injective with respect to a cone of maps (A → A_{i})_{i∈I} if the map K → 1 belongs to ⋃_{i∈I} inj(A → A_{i}). A small cone-injectivity class is the full subcategory of K of objects injective with respect to a given set of cones.

Hence the conclusion of the section:

A.5. Theorem. Let I be a set of maps of a locally presentable category K. Let A be a coreflective small cone-injectivity class of K such that each map of each cone is an element of cof_{K}(I). Then there exists a set of maps J of A such that cof_{K}(I)∩Mor(A) = cof_{A}(J).

Proof. By Lemma A.3, it suffices to prove that there exists a set of maps J of A which is a solution set for I with J ⊂ cof_{K}(I). We mimic the proof of [Bek00, Lemma 1.9]. Since A is a small cone-injectivity class, it is accessible (and accessibly embedded) by [AR94, Proposition 4.16]. Therefore A is locally presentable by Proposition 3.7. The inclusion functor Mor(A) ⊂ Mor(K) is colimit-preserving between two locally presentable categories (by [AR94, Theorem 2.43]). Therefore it is accessible. So it satisfies the solution set condition by [AR94, Corollary 2.45]. This means that there exists for each i ∈ I a solution set W_{i} ⊂ Mor(A), i.e. every map i → w of Mor(K) from i ∈ I to w ∈ Mor(A) factors as a composite i → w_{i} → w for some w_{i} ∈ W_{i}. Consider the set of commutative squares i → w_{i} for i running over the set I and w_{i} running over the set W_{i}:

\xymatrix{• \ar[d]_{i} \ar[r] & X \ar[d]_{w_{i}} \\ • \ar[r] & Y,}

Form the pushout diagram

[figure: •; i; X; i′; w_{i}; •; P; c; Y]

and factor c as P →^{p} Q →^{q} Y with p ∈ cell_{K}(I) and q ∈ inj_{K}(I). As in [Bek00, Lemma 1.9], let J be the set of maps j = pi′. By hypothesis, X and Y are cone-injective. Consider a map A ⟶ Q where A is the top of a cone characterizing A as a small cone-injectivity class. Let us consider the composition

A ⟶ Q ⟶^{q} Y.

Since Y is cone-injective, there exists a map A → B of the cone with top A and a commutative square of solid arrows of the form

\xymatrix{A \ar[r] \ar[d]_{g} & Q \ar[d]_{q} \\ B \ar[r]^{k} \ar@{-->}[ur]^{ℓ} & Y}

Since g ∈ cof_{K}(I) by hypothesis, and since q ∈ inj_{K}(I), the lift ℓ exists. This means that Q is cone-injective as well, i.e. Q ∈ A. Since A is a full subcategory of K, we deduce that j is a map of A. Therefore, J ⊂ cell_{K}(I) ∩ Mor(A). Finally, every map i → w of Mor(K) from i ∈ I to w ∈ Mor(A) factors as a composite i → j → w with j ∈ J by:

[figure: •; i; X; j(=pi′); X; w_{i}; •; w; •; Q; q; Y; •]

References

[AHRT02] J. Adámek, H. Herrlich, J. Rosický, and W. Tholen. On a generalized smallobject argument for the injective subcategory problem. Cah. Topol. Géom. Différ. Catég., 43(2):83–106, 2002.

[AHS06] J. Adámek, H. Herrlich, and G. E. Strecker. Abstract and concrete categories: the joy of cats. Repr. Theory Appl. Categ., (17):1–507 (electronic), 2006. Reprint of the 1990 original [Wiley, New York; MR1051419].

[AR94] J. Adámek and J. Rosický. Locally presentable and accessible categories. Cambridge University Press, Cambridge, 1994.

[BCMR11] J. Bagaria, C. Casacuberta, A. R. D. Mathias, and J. Rosicky. Definable orthogonality classes in accessible categories are small. arXiv:1101.2792, 2011.

[Bek00] T. Beke. Sheafifiable homotopy model categories. Math. Proc. Cambridge Philos. Soc., 129(3):447–475, 2000.

[Cis02] D-C. Cisinski. Théories homotopiques dans les topos. J. Pure Appl. Algebra, 174(1):43–82, 2002.

[CS96] G. L. Cattani and V. Sassone. Higher-dimensional transition systems. In 11th Annual IEEE Symposium on Logic in Computer Science (New Brunswick, NJ, 1996), pages 55–62. IEEE Comput. Soc. Press, Los Alamitos, CA, 1996.

[Dij68] E.W. Dijkstra. Cooperating Sequential Processes. Academic Press, 1968.

[DS95] W. G. Dwyer and J. Spaliński. Homotopy theories and model categories. In Handbook of algebraic topology, pages 73–126. North-Holland, Amsterdam, 1995.

[Dug01] D. Dugger. Combinatorial model categories have presentations. Adv. Math., 164(1):177–201, 2001.

[Fah05] U. Fahrenberg. A category of higher-dimensional automata. In Proc. FOS-SACS’05, volume 3441 of Lecture Notes in Computer Science, pages 187–201. Springer-Verlag, 2005.

[FGR98] L. Fajstrup, E. Goubault, and M. Raußen. Detecting deadlocks in concurrent systems. In CONCUR’98: concurrency theory (Nice), volume 1466 of Lecture Notes in Comput. Sci., pages 332–347. Springer, Berlin, 1998.

[FR08] L. Fajstrup and J. Rosický. A convenient category for directed homotopy. Theory and Applications of Categories, 21(1):pp 7–20, 2008.

[Gau03] P. Gaucher. A model category for the homotopy theory of concurrency. Homology, Homotopy and Applications, 5(1):p.549–599, 2003.

[Gau08] P. Gaucher. Towards a homotopy theory of process algebra. Homology Homotopy Appl., 10(1):353–388 (electronic), 2008.

[Gau09] P. Gaucher. Homotopical interpretation of globular complex by multipointed d-space. Theory Appl. Categ., 22:No. 22, 588–621 (electronic), 2009.

[Gau10a] P. Gaucher. Combinatorics of labelling in higher dimensional automata. Theoretical Computer Science, 411(11-13):1452–1483, 2010. doi:10.1016/j.tcs.2009.11.013.

[Gau10b] P. Gaucher. Directed algebraic topology and higher dimensional transition system. To appear in the New-York Journal of Mathematics, 2010.

[GG03] P. Gaucher and E. Goubault. Topological deformation of higher dimensional automata. Homology, Homotopy and Applications, 5(2):p.39–82, 2003.

[Gou02] E. Goubault. Labelled cubical sets and asynchronous transistion systems: an adjunction. Presented at CMCIM’02, 2002.

[Gra03] M. Grandis. Directed homotopy theory. I. Cah. Topol. Géom. Différ. Catég., 44(4):281–316, 2003.

[Gun94] J. Gunawardena. Homotopy and concurrency. Bull. EATCS, 54:184–193, 1994.

[Hir03] P. S. Hirschhorn. Model categories and their localizations, volume 99 of Mathematical Surveys and Monographs. American Mathematical Society, Providence, RI, 2003.

[HJ99] K. Hrbacek and T. Jech. Introduction to set theory, volume 220 of Monographs and Textbooks in Pure and Applied Mathematics. Marcel Dekker Inc., New York, third edition, 1999.

[Hov99] M. Hovey. Model categories. American Mathematical Society, Providence, RI, 1999.

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

[KR05] A. Kurz and J. Rosický. Weak factorizations, fractions and homotopies. Applied Categorical Structures, 13(2):pp.141–160, 2005.

[Kri08] S. Krishnan. A convenient category of locally preordered spaces. Applied Categorical Structures, pages 1–22, 2008. doi:10.1007/s10485-008-9140-9.

[Lur09] J. Lurie. Higher topos theory, volume 170 of Annals of Mathematics Studies. Princeton University Press, Princeton, NJ, 2009.

[ML98] S. Mac Lane. Categories for the working mathematician. Springer-Verlag, New York, second edition, 1998.

[Ols09] M. Olschok. Left determined model structures for locally presentable categories. Applied Categorical Structures, 2009. 10.1007/s10485-009-9207-2.

[Pra91] V. Pratt. Modeling concurrency with geometry. In ACM Press, editor, Proc. of the 18th ACM Symposium on Principles of Programming Languages, 1991.

[Rap09] G. Raptis. On the cofibrant generation of model categories. J. Homotopy Relat. Struct., 4(1):245–253, 2009.

[Ree74] C. L. Reedy. Homotopy theory of model categories. Unpublished manuscript, 1974.

[Ros09] J. Rosický. On combinatorial model categories. Appl. Categ. Structures, 17(3):303–316, 2009.

[RT03] J. Rosický and W. Tholen. Left-determined model categories and universal homotopy theories. Trans. Amer. Math. Soc., 355(9):3611–3623 (electronic), 2003.

[VG06] R.J. Van Glabbeek. On the expressiveness of higher dimensional automata. Theor. Comput. Sci., 368(1-2):168–194, 2006.

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

[Wor04] K. Worytkiewicz. Synchronization from a categorical perspective. ArXiv cs.PL/0411001, 2004.

Univ Paris Diderot Sorbonne Paris Cité Laboratoire PPS CNRS UMR 7126 75205 Paris Cedex 13 France http://www.pps.jussieu.fr/˜ gaucher/

Email: gaucher@pps.jussieu.fr

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/25/12/25-12.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors

Clemens Berger, Université de Nice-Sophia Antipolis, cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it

Valeria de Paiva: valeria.depaiva@gmail.com

Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Glasgow, Tom.Leinster@glasgow.ac.uk Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.upenn.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca