Theory and Applications of Categories, Vol. 32, No. 33, 2017, pp. 1107–1164.

COMBINATORICS OF PAST-SIMILARITY IN HIGHER DIMENSIONAL TRANSITION SYSTEMS

PHILIPPE GAUCHER

Abstract. The key notion to understand the left determined Olschok model category of star-shaped Cattani-Sassone transition systems is past-similarity. Two states are past-similar if they have homotopic pasts. An object is fibrant if and only if the set of transitions is closed under past-similarity. A map is a weak equivalence if and only if it induces an isomorphism after the identification of all past-similar states. The last part of this paper is a discussion about the link between causality and homotopy.

Contents

1 Introduction  1107
2 Higher dimensional transition systems  1112
3 Colimit of regular transition systems  1116
4 Cattani-Sassone transition system  1118
5 Homotopy theory of non star-shaped objects  1120
6 Computation of the path functor  1126
7 Characterization in the non star-shaped case  1128
8 Homotopy theory of star-shaped objects  1132
9 Past-similarity of states  1138
10 Fibrant star-shaped transition systems  1144
11 Characterization in the star-shaped case  1153
12 Causality and homotopy  1157
A Erratum  1161

1. Introduction

1.1. Presentation. This work belongs to our series of papers devoted to higher dimensional transition systems [Gaucher, 2010a] [Gaucher, 2011] [Gaucher, 2014a] [Gaucher, 2014b] [Gaucher, 2015a] [Gaucher, 2015b]. One of the goal of this series of papers is to explore the link between causality and homotopy in this setting.

Received by the editors 2016-08-02 and, in final form, 2017-08-26. Transmitted by Jiri Rosicky. Published on 2017-08-29. This revision 2017-09-08. 2010 Mathematics Subject Classification: 18C35,55U35,18G55,68Q85. Key words and phrases: left determined model category, combinatorial model category, discrete

model structure, higher dimensional transition system, causal structure, bisimulation.

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

\xymatrix{ & β \ar[dr]^{\{v\}} \\ α \ar[ur]^{\{u\}} \ar[dr]_{\{v\}} & \{u, v\} & δ \\  & γ \ar[ur]_{\{u\}}}

Figure 1: u||v: Concurrent execution of u and v

The notion of higher dimensional transition system is a higher dimensional analogue of the computer-scientific notion of labelled transition system. The purpose is to model the concurrent execution of n actions by a multiset of actions, i.e. a set with a possible repetition of some elements (e.g. {u, u, v, w, w, w}). In the language of Cattani and Sassone [Cattani and Sassone, 1996], the higher dimensional transition system u||v modeling the concurrent execution of the two actions u and v, depicted by Figure 1, consists of the transitions (α, {u}, β), (β, {v}, δ), (α, {v}, γ), (γ, {u}, δ) and (α, {u, v}, δ), where the middle term is a multiset, not a set. The labelling map is in this case the identity map.

This notion is reformulated in [Gaucher, 2010a] to make easier a categorical and homotopical treatment. A higher dimensional system consists of a set of states S, a set of actions L together with a labelling map μ : L → Σ where Σ is a set of labels, and a set of tuples of ⋃_{n⩾1} S × L^{n} × S satisfying at least the following two axioms, to obtain the “minimal” notion of weak transition system:

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

• Patching 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.

The multiset axiom avoids the use of multisets. The patching axiom enables us to see, amongst other things, the n-cube as a free object generated by a n-transition. The patching axiom looks like a 5-ary composition because it generates a new transition (the patch) from five transitions satisfying a particular condition. These two axioms are mathematically designed so that the forgetful functor forgetting the set of transitions is topological [Gaucher, 2010a, Theorem 3.4]. This topological structure turns out to be a very powerful tool to deal with these objects. Figure 1 has in this new formulation the transitions (α, u, β), (β, v, δ), (α, v, γ), (γ, u, δ), (α, u, v, δ) and (α, v, u, δ).

This paper is the direct continuation of [Gaucher, 2015a]. However, its reading is not required to read this one. In [Gaucher, 2015a], we prove the existence of a left determined Olschok model structure of weak transition systems which restricts to left determined Olschok model structures on various full subcategories without using the map R : {0, 1} → {0} in the set of generating cofibrations (unlike what is done in [Gaucher, 2011] and [Gaucher, 2015b]). Then we prove that the behavior of these homotopy theories break the causal structure and that the solution to overcome this problem is to work with star-shaped transition systems. A star-shaped transition system is by definition a pointed transition system (X, ∗), that means a transition system X together with a distinguished state ∗ called the base state, such that all other states of X are reachable from ∗ by a path, i.e. a finite sequence of 1-transitions. This path may also be called a past of the state.

In this paper, we want to make precise the above observations which are only sketched in [Gaucher, 2015a]. We work in a reflective subcategory of all subcategories of higher dimensional transition systems introduced in [Gaucher, 2015a]. It is called the subcategory CSTS of Cattani-Sassone transition systems. The axiom we add is CSA1: if α →^{u} β and α →^{v} β are two 1-transitions with μ(u) = μ(v), then u = v. This axiom is introduced in [Cattani and Sassone, 1996] in a more general formulation: we only use its 1-dimensional version. It appears also in [Winskel and Nielsen, 1995, Proposition 72] (it is called the condition-extension condition) and in the notion of extensional asynchronous transition system [Winskel and Nielsen, 1995, page 140]. It is used in [Gaucher, 2011] for a different purpose. The main feature of this axiom is to simplify the calculations of the cylinder and path functors (cf. Table 2, Table 3 and Table 4) while keeping all examples coming from process algebras [Gaucher, 2008] [Gaucher, 2010b] [Gaucher, 2010a]. The structure of the left determined model category CSTS obtained by restricting the construction of [Gaucher, 2015a] is unravelled in the following theorem:

1.2. Theorem. (Theorem 7.5) The left determined Olschok model category CSTS is Quillen equivalent to the full subcategory of Cattani-Sassone transition systems having at most one state equipped with the discrete model structure.

This theorem means that the homotopy category of Cattani-Sassone transition systems destroys the causal structure in a very spectacular way. Thus, localizing or colocalizing this model category will never give anything interesting from a computer-scientific point of view because it already contains too many weak equivalences.

The formalism of Cattani-Sassone transition systems is interesting because, unlike any formalism of labelled precubical sets [Gaucher, 2008] [Gaucher, 2010b] [Gaucher, 2014b], it only contains objects satisfying the higher dimensional automata paradigm [Gaucher, 2010a, Definition 7.1]: mathematically, this paradigm states that the boundary of a labelled n-cube, with n ⩾ 2, can be filled by at most one n-cube; from a computer scientific point of view, this paradigm means that the concurrent execution of n actions is modelled by exactly one n-cube, and not two or more having the same (n − 1)-dimensional boundary. The drawback of the formalism of higher dimensional transition system is that colimits are difficult to compute because of the patching axiom which freely adds new transitions in the colimits (cf. [Gaucher, 2015b, Proposition A.1]). Thanks to the axiom CSA2 (recalled in Section 2 and which plays the role of face operators in this setting), the category of Cattani-Sassone transition systems is better behaved with respect to colimits and the following fact can be considered as an important result of the paper:

1.3. Theorem. (Theorem 4.5) The set of transitions of a colimit of Cattani-Sassone transition systems is the union of the sets of transitions of the components.

The calculations made to prove Theorem 7.5 enable us to study the model category CSTS_{•} of star-shaped (Cattani-Sassone) transition systems. The notion of past-similarity plays a key role in this study. Two states α and β of a star-shaped (Cattani-Sassone) transition system (X, ∗) are past-similar if there exist two paths from the base state ∗ to α and β respectively which are homotopic. A star-shaped transition system is reduced if two states are past-similar if and only if they are equal: Figure 3 page 1139 gives an example of a non-reduced transition system. Using these two new notions (past-similarity and reduced transition system), the structure of the model category of star-shaped transition systems is unravelled:

1.4. Theorem. (Theorem 10.12) The fibrant objects of CSTS_{•} are the Cattani-Sassone transition systems such that the set of transitions is closed under past-similarity. In particular, all reduced transition systems are fibrant.

1.5. Theorem. (Theorem 11.9) The left determined Olschok model category CSTS_{•} is Quillen equivalent to the full subcategory of reduced objects equipped with the discrete model structure. In particular, a map of star-shaped Cattani-Sassone transition system is a weak equivalence if and only if it is an isomorphism after the identification of all past-similar states.

The interpretation of Theorem 11.9 is postponed to the discussion of Section 12 which speculates about the link between causality and homotopy in this setting.

1.6. Outline of the paper. The paper is structured as follows. Section 2 is a reminder about weak, cubical, regular and Cattani-Sassone transition systems. It avoids the reader to have to read the previous papers of this series. All these notions are necessary because calculations of limits and colimits often require to start from the topological structure of weak transition systems, and then to restrict to the coreflective subcategory of cubical transition systems, and then to restrict twice to the reflective subcategories of regular and Cattani-Sassone transition systems. It also happens that some proofs can be written only by working with cubical transition systems (e.g. the proof of Proposition 11.7). Section 3 is a technical section about the calculation of colimits in the category of regular transition systems. Theorem 3.3 must be considered as a vast generalization of [Gaucher, 2010a, Theorem 4.7] and [Gaucher, 2015b, Proposition A.3]. Roughly speaking, it says that the set of transitions of a colimit of regular transition systems is the union of the set of transitions. Section 4 expounds some basic properties of Cattani-Sassone transition systems. It also extends Theorem 3.3 to this new setting: in the category of Cattani-Sassone transition systems as well, the set of transitions of a colimit is also the union of the set of transitions. Section 5 uses the toolbox [Gaucher, 2015c] and the results of [Gaucher, 2015a] to construct the left determined Olschok model structure of Cattani-Sassone transition systems. The cylinder functor is calculated in detail. Section 6 gives a very explicit formulation of the path functor of the model category constructed in Section 5. Section 7 proves the first main result of the paper (Theorem 7.5). The formulation is chosen to highlight the destruction of the causal structure. The notions of pointed and star-shaped transition systems are recalled in Section 8. Then the toolbox [Gaucher, 2015c] is used to prove the existence of the left determined model structures on pointed and star-shaped Cattani-Sassone transition systems. Meanwhile, we give precise formulations of the cylinder and path functors of a star-shaped transition system. The notion of pastsimilar states is introduced and succinctly studied in Section 9. Section 10 characterizes the fibrant object of the left determined model structure of star-shaped transition systems (Theorem 10.12). Section 11 introduces a particular case of fibrant objects: the reduced star-shaped transition systems. By definition, a star-shaped transition system is reduced if past-similarity and equality coincide. Then the last part of the second main result of the paper (Theorem 11.9) is established. Section 12 is a discussion about an interpretation of Theorem 11.9 and about possible future works. In particular, Theorem 12.4 rules out a lot of candidates of model categories. The appendix is an erratum of the paper [Gaucher, 2015a].

1.7. Prerequisites and notations. All categories are locally small. The set of maps in a category K from X to Y is denoted by K(X, Y). The cardinal of a set S is denoted by #S. The class of morphisms of a category K is denoted by Mor(K). The composite of two maps is denoted by fg instead of f ∘g. The initial (final resp.) object, if it exists, is always denoted by ∅ (1 resp.). The identity of an object X is denoted by Id_{X}. A subcategory is always isomorphism-closed (i.e. replete). A reflective or coreflective subcategory is always full. By convention, A × B ⊔ C × D means (A × B) ⊔ (C × D) where × denotes the binary product and ⊔ the binary coproduct. Let f and g be two maps of a locally presentable category K. Denote by f□g when f satisfies the left lifting property (LLP) with respect to g, or equivalently when g satisfies the right lifting property (RLP) with respect to f. Let us introduce the notations inj_{K}(C) = {g ∈ K, ∀f ∈ C, f□g} called the class of Cinjective maps 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). There is the inclusion cell_{K}(C) ⊂ cof_{K}(C). Moreover, every morphism of cof_{K}(C) is a retract of a morphism of cell_{K}(C) as soon as the domains of K are small relative to cell_{K}(C) [Hovey, 1999, Corollary 2.1.15], e.g. when K is locally presentable. For every map f : X → Y and every natural transformation α : F → F′ between two endofunctors of K, the map f ⋆ α is defined by the diagram:

[figure: F X; α_{X}; F f; F Y; α_{Y}; F′X; F′f; •; f⋆α; F′Y.]

For a set of morphisms A, let A ⋆ α = {f ⋆ α, f ∈ A}. A cylinder functor C : K → K is equipped with two natural transformations γ = γ^{0} ⊔ γ^{1} : Id ⊔ Id ⇒ C and σ : C ⇒ Id such that σγ : Id ⊔ Id ⇒ Id is the codiagonal. A path functor P : K → K is equipped with two natural transformations τ : Id ⇒ P and π = (π^{0}, π^{1}) : P ⇒ Id × Id such that πτ : Id ⇒ Id × Id is the diagonal. Sometimes, a Greek letter denotes a state: the context always enables the reader to avoid any confusion. In a model category M, the homotopy class (left homotopy class, right homotopy class) of maps from X to Y is denoted by π_{M}(X, Y) (π_{M}^{l}(X, Y), π_{M}^{r}(X, Y) resp.). A cofibrant replacement functor will be denoted by (−)^{cof} and a fibrant replacement functor by (−)^{fib}. The discrete model structure is the model structure such that all maps are cofibrations and fibrations and such that the weak equivalences are the isomorphisms [Salch, 2017]. A map of model categories, i.e. a left Quillen functor L : M → N is homotopically surjective [Dugger, 2001, Definition 3.1] if for every fibrant object Y of N and every cofibrant replacement (RY)^{cof} →^{∼} RY, where R is a right adjoint of L, the induced map L((RY)^{cof}) → Y is a weak equivalence of N. A homotopically surjective map of model categories L : M → N is a Quillen equivalence if and only if for every cofibrant object X of M and every fibrant replacement LX →^{∼} (LX)^{fib}, the map X → R((LX)^{fib}) is a weak equivalence of M.

We refer to [Adámek and Rosický, 1994] for locally presentable categories, to [Rosický, 2009] for combinatorial model categories, and to [Adámek, Herrlich, and Strecker, 2006] for topological categories, i.e. categories equipped with a topological functor towards a power of the category of sets. We refer to [Hovey, 1999] and to [Hirschhorn, 2003] for model categories. For general facts about weak factorization systems, see also [Kurz and Rosický, 2005]. The reading of the first part of [Olschok, 2009b], published in [Olschok, 2009a], is recommended for any reference about good, cartesian, and very good cylinders. We use the paper [Gaucher, 2015c] as a toolbox for constructing the model structures. To keep this paper short, we refer to [Gaucher, 2015c] for all notions related to Olschok model categories.

2. Higher dimensional transition systems

This section is a reminder about weak, cubical, regular and Cattani-Sassone transition systems.

An infinite set of labels Σ is fixed. A transition presystem consists of a triple X = (\underline{S}(X), μ : \underline{L}(X) → Σ, \underline{T}(X) = ⋃_{n⩾1} \underline{T}_{n}(X)) where \underline{S}(X) is a set of states, where \underline{L}(X) is a set of actions, where μ : \underline{L}(X) → Σ is a set map called the labelling map, and finally where \underline{T}_{n}(X) ⊂ \underline{S}(X) × \underline{L}(X)^{n} × \underline{S}(X) for n ⩾ 1 is a set of n-transitions or n-dimensional transitions. A n-transition (α, u_{1}, …, u_{n}, β) is also called a transition from α to β: α is the initial state and β the final state of the transition. It can be denoted by \xymatrix{α \ar[r]^{u_{1},...,u_{n}} & β}. This set of data satisfies one or several of the following axioms (note that the Intermediate state axiom is a consequence of CSA2):

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

• Patching 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.

• All actions are used. For every u ∈ L, there is a 1-transition (α, u, β).

• Intermediate state axiom. For every n ⩾ 2, every p with 1 ⩽ p < n and every transition (α, u_{1}, …, u_{n}, β) of X, there exists a state ν (not necessarily unique) such that both (α, u_{1}, …, u_{p}, ν) and (ν, u_{p+1}, …, u_{n}, β) are transitions.

• CSA2 or Unique intermediate state axiom. For every n ⩾ 2, every p with 1 ⩽ p < n and every transition (α, u_{1}, …, u_{n}, β) of X, there exists a unique state ν such that both (α, u_{1}, …, u_{p}, ν) and (ν, u_{p+1}, …, u_{n}, β) are transitions.

• CSA1. If (α, u, β) and (α, v, β) are two transitions such that μ(u) = μ(v), then u = v.

A map of transition presystems consists of two set maps, one between the sets of states, the other one between the set of actions preserving the labelling map, such that any transition of the domain is mapped to a transition of the codomain. For a map f : X → Y of transition presystems, the image by f of a transition (α, u_{1}, …, u_{n}, β) should be noted f((α, u_{1}, …, u_{n}, β)). The notation f(α, u_{1}, …, u_{n}, β) will be used instead to not overload the calculations. This convention is already implicitly used in our previous papers. The mapping X → \underline{S}(X) ( X → \underline{L}(X) resp.) induces a functor from the category of transition presystems to the category of sets Set.

Table 1 lists the definitions of the categories WTS of weak transition systems [Gaucher, 2010a, Definition 3.2], CTS of cubical transition systems [Gaucher, 2011, Proposition 6.7], RTS of regular transition systems [Gaucher, 2015b, Definition 2.2] and CSTS of Cattani-Sassone transition systems [Gaucher, 2015b, Table 1]. All examples coming from process algebras belong to CSTS [Gaucher, 2008] [Gaucher, 2010b] [Gaucher, 2010a].

The category CSTS is a reflective subcategory of CTS by [Gaucher, 2011, Proposition 7.2], but also of RTS by Proposition 4.4. We will come back on the category CSTS in

Cattani-Sassone Regular Cubical Weak
Multiset axiom  yes  yes  yes  yes
Patching axiom  yes  yes  yes  yes
All actions used  yes  yes  yes  no
Intermediate state axiom  yes  yes  yes  no
Unique intermediate state axiom  yes  yes  no  no
CSA1  yes  no  no  no

Table 1: Cattani-Sassone, regular, cubical and weak transition systems.

Section 4. The category RTS is locally finitely presentable by [Gaucher, 2015b, Proposition 4.5]. It is a reflective subcategory of CTS by [Gaucher, 2015b, Proposition 4.4]. The reflection is the functor CSA_{2} : CTS → CTS which forces CSA2 to hold. This functor is extensively studied in [Gaucher, 2015b, Section 4]. The category CTS is locally finitely presentable by [Gaucher, 2011, Corollary 3.15]. By [Gaucher, 2011, Corollary 3.15], the category CTS is a coreflective subcategory of WTS. The latter is locally finitely presentable by [Gaucher, 2010a, Theorem 3.4]. The forgetful functor ω : WTS → Set^{{s}∪Σ} taking the weak higher dimensional transition system X to the ({s} ∪ Σ)-tuple of sets (\underline{S}(X), (μ^{−1}(x))_{x∈Σ}) ∈ Set^{\{s\}∪Σ} is topological by [Gaucher, 2010a, Theorem 3.4]. There is the chain of functors

CSTS ⊂_{reflective} RTS ⊂_{reflective} CTS ⊂_{coreflective} WTS ⟶^{ω}_{topological} Set^{{s}∪Σ}.

We give now some important examples of regular transition systems.

1. Every set X may be identified with the cubical transition system having the set of states X, with no actions and no transitions.

2. For every x ∈ Σ, let us denote by ↑x↑ the cubical transition system with four states {1, 2, 3, 4}, one action x and two transitions (1, x, 2) and (3, x, 4). The cubical transition system ↑x↑ is called the double transition (labelled by x) where x ∈ Σ.

2.1. 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} = ().

Let us introduce the weak transition system corresponding to the labelled n-cube.

2.2. Proposition. [Gaucher, 2010a, 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 transition system called the n-cube.

The n-cubes C_{n}[x_{1}, …, x_{n}] for all n ⩾ 0 and all x_{1}, …, x_{n} ∈ Σ are regular by [Gaucher, 2010a, Proposition 4.6] and [Gaucher, 2010a, Proposition 5.2]. For n = 0, C_{0}[], also denoted by C_{0}, is nothing else but the set {()}.

Here are two important families of weak transition systems which are not cubical, and therefore not regular:

1. The weak transition system \underline{x} = (∅, \{x\} ⊂ Σ, ∅) for x ∈ Σ is not cubical because the action x is not used.

2. Let n ⩾ 0. Let x_{1}, …, x_{n} ∈ Σ. The pure n-transition C_{n}^{ext}[x_{1}, …, x_{n}] is the weak transition system 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}. It is not cubical for n > 1 because it does not contain any 1-transition. Intuitively, the pure transition is a cube without faces of lower dimension.

The main use of the family of pure transitions is summarized in the following two facts:

1. For all weak transition systems X, the set WTS(C_{n}^{ext}[x_{1}, …, x_{n}], X) is the set of transitions (α, u_{1}, …, u_{n}, β) of X such that for all 1 ⩽ i ⩽ n, μ(u_{i}) = x_{i} and

⨆_{x_{1},...,x_{n}∈Σ} WTS(C_{n}^{ext}[x_{1}, …, x_{n}], X)

is the set of transitions of X.

2. Every map of weak transition systems f : C_{n}^{ext}[x_{1}, …, x_{n}] → X where X satisfies CSA2 factors uniquely as a composite f : C_{n}^{ext}[x_{1}, …, x_{n}] → C_{n}[x_{1}, …, x_{n}] → X by [Gaucher, 2010a, Theorem 5.6].

We conclude this section by recalling some important facts:

2.3. Proposition. Let f : A → B be a map of weak transition systems which is one-to-one on states and on actions. Then it is one-to-one on transitions.

Proof. It is mutatis mutandis the proof of [Gaucher, 2014b, Proposition .4.4].

2.4. Theorem. [Gaucher, 2015b, Theorem 3.3] Let (f_{i} : ω(A_{i}) → W)_{i∈I} be a cocone of Set^{{s}∪Σ} such that the weak transition systems A_{i} are cubical for all i ∈ I and such that every action u of W is the image of an action of A_{i_{u}} for some i_{u} ∈ I. Then the ω-final lift \overline{W} is cubical.

2.5. Proposition. [Gaucher, 2015b, Proposition 4.1] Let X be a cubical transition system. Let Y be a weak transition system satisfying CSA2. Let f : X → Y be a map of weak transition systems which is one-to-one on states. Then X is regular, and in particular satisfies CSA2.

3. Colimit of regular transition systems

Theorem 3.3 states that the set of transitions of a colimit of regular transition systems is the union of the set of transitions. Its proof is similar to the proofs of [Gaucher, 2010a, Theorem 4.7] and [Gaucher, 2015b, Proposition A.3].

We need to recall two lemmas about colimits of weak transition systems and cubical transition systems coming from [Gaucher, 2015a].

3.1. Lemma. The forgetful functor mapping a weak transition system to its set of states is colimit-preserving. The forgetful functor mapping a weak transition system to its set of actions is colimit-preserving.

Proof. The lemma is a consequence of the fact that the functor ω : WTS ⟶ 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.

3.2. Lemma. The forgetful functor mapping a cubical transition system to its set of states is colimit-preserving. The forgetful functor mapping a cubical transition system to its set of actions is colimit-preserving.

Proof. Since the category of cubical transition systems is a coreflective subcategory of the category of weak transition systems by [Gaucher, 2011, Corollary 3.15], this lemma is a consequence of Lemma 3.1.

3.3. Theorem. Let (i ↦ X_{i}) be a small diagram of RTS. The set of states \underline{S}(\underrightarrow{lim} X_{i}) is a quotient of the set \underrightarrow{lim} \underline{S}(X_{i}), the set of actions \underline{L}(\underrightarrow{lim} X_{i}) is equal to \underrightarrow{lim} \underline{L}(X_{i}) and the set of transitions of \underrightarrow{lim} X_{i} is equal to ⋃_{i} ϕ_{i}(\underline{T}(X_{i})) where ϕ_{i} : X_{i} → \underrightarrow{lim} X_{i} is the canonical map. In particular, the regular transition system \underrightarrow{lim} X_{i} is equipped with the ω-final structure.

Proof. The proof is divided in two parts. The first one is easy. The second one requires to be more careful and shows how the patching axiom can be used.

\underline{The case of states and actions}. The colimit \underrightarrow{lim} X_{i} in RTS is equal to CSA_{2}(\underrightarrow{lim}^{CTS} X_{i}) where \underrightarrow{lim}^{CTS} X_{i} is the colimit calculated in CTS. Since the functors \underline{S} : CTS → Set and \underline{L} : CTS → Set are colimit-preserving by Lemma 3.2, we have the bijection of sets \underrightarrow{lim} \underline{S}(X_{i}) ≅ \underline{S}(\underrightarrow{lim}^{CTS} X_{i}) and \underrightarrow{lim} \underline{L}(X_{i}) ≅ \underline{L}(\underrightarrow{lim}^{CTS} X_{i}). The unit map \underrightarrow{lim}^{CTS} X_{i} → CSA_{2}(\underrightarrow{lim}^{CTS} X_{i}) is onto on states and bijective on actions by [Gaucher, 2015b, Proposition 4.2]: the functor CSA_{2} : CTS → RTS forces CSA2 to hold by making identifications of states. We deduce that the set of states of \underrightarrow{lim} X_{i} is a quotient of \underrightarrow{lim} \underline{S}(X_{i}) and that the set of actions of \underrightarrow{lim} X_{i} is exactly \underrightarrow{lim} \underline{L}(X_{i}).

\underline{The case of transitions}. Let T = ⋃_{i} ϕ_{i}(\underline{T}(X_{i})). Let (f_{i}(α), f_{i}(u_{1}), …, f_{i}(u_{n}), f_{i}(β)) be a tuple of T. Then the tuple (α, u_{σ(1)}, …, u_{σ(n)}, β) is a transition of X_{i} for all permutations σ of {1, …, n}. So the tuple (f(α), f(u_{σ(1)}), …, f(u_{σ(n)}), f(β)) belongs to T. This means that the set of tuples T satisfies the multiset axiom. Let n ⩾ 3 and p, q ⩾ 1 with p+q < n. Let

(α, u_{1}, …, u_{n}, β), (α, u_{1}, …, u_{p}, μ), (μ, u_{p+1}, …, u_{n}, β), (α, u_{1}, …, u_{p+q}, ν), (ν, u_{p+q+1}, …, u_{n}, β)

be five tuples of T. Let (α, u_{1}, …, u_{n}, β) = (f_{i}(γ), f_{i}(v_{1}), …, f_{i}(v_{n}), f_{i}(δ)) where the tuple (γ, v_{1}, …, v_{n}, δ) is a transition of X_{i}. There exist two states ϵ and η of X_{i} such that the five tuples

(γ, v_{1}, …, v_{p}, ϵ), (γ, v_{1}, …, v_{p+q}, η), (ϵ, v_{p+1}, …, v_{n}, δ), (η, v_{p+q+1}, …, v_{n}, δ), (ϵ, v_{p+1}, …, v_{p+q}, η)

are transitions of X_{i} since X_{i} is cubical and by using the patching axiom in X_{i}. Therefore, the five tuples

(α, u_{1}, …, u_{p}, f_{i}(ϵ)), (α, u_{1}, …, u_{p+q}, f_{i}(η)),

(f_{i}(ϵ), u_{p+1}, …, u_{n}, β), (f_{i}(η), u_{p+q+1}, …, u_{n}, β),

(f_{i}(ϵ), u_{p+1}, …, u_{p+q}, f_{i}(η))

are transitions of \underrightarrow{lim} X_{i}. The point is that \underrightarrow{lim} X_{i} satisfies CSA2. We deduce that f_{i}(ϵ) = μ and f_{i}(η) = ν. We obtain that

(μ, u_{p+1}, …, u_{p+q}, ν) = (f_{i}(ϵ), f_{i}(v_{p+1}), …, f_{i}(v_{p+q}), f_{i}(η)) ∈ T.

This means that the set of tuples T satisfies the patching axiom. Write Z for the weak transition system having the set of transitions T. We have obtained a morphism of cocones of weak transition systems

[figure: (X_{i}); (X_{i}); Z; ⊂; \underrightarrow{lim} X_{i}.]

The map Z → \underrightarrow{lim} X_{i} is bijective on states and on actions, and therefore one-to-one on transitions by Proposition 2.3. We have also proved that the weak transition system Z is the ω-final lift of the cocone (ω(X_{i}) → ω(Z)) of Set^{{s}∪Σ}. By Theorem 2.4, the weak transition system Z is cubical. Since the map Z → \underrightarrow{lim} X_{i} is one-to-one on states, the cubical transition system Z satisfies CSA2 by Proposition 2.5. We have proved that Z = \underrightarrow{lim} X_{i}.

3.4. Corollary. Consider a pushout diagram of RTS

[figure: A; ϕ; p; X; f; B; ψ; Y]

such that the left vertical map A → B is onto on states, on actions and on transitions. Then the right vertical map is onto on states, on actions and on transitions.

Proof. Since the map A → B is onto on states and on actions, the map X → Y is onto on states and on actions as well by Theorem 3.3. By Theorem 3.3, we have the equality \underline{T}(Y) = f(\underline{T}(X)) ∪ ψ(\underline{T}(B)). Since A → B is onto on transitions, we also have the equalities ψ(\underline{T}(B)) = ψ(p(\underline{T}(A)) = f(ϕ(\underline{T}(A)). We deduce the inclusion ψ(\underline{T}(B)) ⊂ f(\underline{T}(X)). We obtain \underline{T}(Y) = f(\underline{T}(X)).

In Corollary 3.4, RTS cannot be replaced by CTS (cf. [Gaucher, 2015b, Proposition A.1]). This “good” behavior of colimits in RTS is due to CSA2.

4. Cattani-Sassone transition system

All sets, all double transitions and all cubes are Cattani-Sassone transition systems. All weak transition systems coming from a process algebra are Cattani-Sassone transition systems [Gaucher, 2008] [Gaucher, 2010b].

4.1. Notation. Let U = {C_{1}[x] ⊔_{{0_{1},1_{1}}} C_{1}[x] → C_{1}[x] | x ∈ Σ}.

4.2. Proposition. Let X be a weak transition system. The following conditions are equivalent:

1. X is U-injective.

2. X is U-orthogonal.

3. X satisfies CSA1.

Proof. Every map of U is bijective on states and onto on actions. Thus, every map of U is epic. We deduce the equivalence (1) ⇔ (2). The equivalence (1) ⇔ (3) is clear.

4.3. Proposition. Every map of cell_{RTS}(U) is onto on states, on actions and on transitions. In particular, every map of cell_{RTS}(U) is epic.

Proof. Every pushout in RTS of a map of U is onto on states, on actions and on transitions by Corollary 3.4. Every transfinite composition in RTS of maps onto on states, on actions and on transitions is onto on states, on actions and on transitions by Theorem 3.3. Therefore, every map of cell_{RTS}(U) is onto on states, on actions and on transitions. In particular, every map of cell_{RTS}(U) is epic.

Since every map of cell_{RTS}(U) is epic by Proposition 4.3, the canonical map X → 1 from X to the terminal object of RTS factors functorially and uniquely, up to isomorphism, as a composite

\xymatrix{X \ar[r]^{∈cell_{RTS}(U)} & CSA_{1}(X) \ar[r]^{∈inj_{RTS}(U)} & 1}

in RTS where the left-hand map belongs to cell_{RTS}(U) and the right-hand map belongs to inj_{RTS}(U) (see [Gaucher, 2015a, Proposition A.1] for a proof of uniqueness). By Proposition 4.2, the regular transition system CSA_{1}(X) satisfies CSA1. We have obtained a well-defined functor CSA_{1} : RTS → RTS.

4.4. Proposition. The category CSTS is a reflective locally finitely presentable subcategory of RTS. The left adjoint of the inclusion CSTS ⊂ RTS is precisely the functor CSA_{1} : RTS → RTS.

Proof. By Proposition 4.2, CSTS is a small-orthogonality class of RTS. Hence it is a reflective subcategory. Thus, CSTS is complete and cocomplete. The set of cubes and double transitions is a dense and hence strong generator of finitely presentable objects of RTS by [Gaucher, 2011, Theorem 3.11], and therefore of CSTS. Consequently, the category CSTS is locally finitely presentable by [Adámek and Rosický, 1994, Theorem 1.20]. Let f : X → Z be a map of regular transition systems such that Z satisfies CSA1. Then we have the commutative diagram of RTS

\xymatrix{X \ar[r] \ar[d] & Z \ar[d] \\ CSA_{1}(X) \ar@{-->}[ur]^{ℓ} \ar[r] & 1.}

By construction, the left vertical map belongs to cell_{RTS}(U). Since Z satisfies CSA1, the right vertical map belongs to inj_{RTS}(U) by Proposition 4.2. Therefore the lift ℓ exists and it is unique since the left vertical map is epic by Proposition 4.3. Thus, the map X → Z factors uniquely as a composite X → CSA_{1}(X) → Z.

4.5. Theorem. Let (i ↦ X_{i}) be a small diagram of CSTS. The set of states \underline{S}(\underrightarrow{lim} X_{i}) is a quotient of the set \underrightarrow{lim} \underline{S}(X_{i}), the set of actions \underline{L}(\underrightarrow{lim} X_{i}) is a quotient of the set \underrightarrow{lim} \underline{L}(X_{i}) and the set of transitions of \underrightarrow{lim} X_{i} is equal to ⋃_{i} ϕ_{i}(\underline{T}(X_{i})) where ϕ_{i} : X_{i} → \underrightarrow{lim} X_{i} is the canonical map. In particular, the Cattani-Sassone transition system \underrightarrow{lim} X_{i} is equipped with the ω-final structure.

Proof. We have \underrightarrow{lim} X_{i} ≅ CSA_{1}(\underrightarrow{lim}^{RTS} X_{i}) where \underrightarrow{lim}^{RTS} is the colimit calculated in RTS. The unit map \underrightarrow{lim}^{RTS} X_{i} → CSA_{1}(\underrightarrow{lim}^{RTS} X_{i}) belongs to cell_{RTS}(U). Therefore it is onto on states, on actions and on transitions by Proposition 4.3. The proof is complete thanks to Theorem 3.3.

4.6. Corollary. Consider a pushout diagram of CSTS

[figure: A; ϕ; p; X; f; B; ψ; Y]

such that the left vertical map A → B is onto on states, on actions and on transitions. Then the right vertical map is onto on states, on actions and on transitions.

Proof. The proof is mutatis mutandis the proof of Corollary 3.4.

5. Homotopy theory of non star-shaped objects

Let X be a weak transition system. By [Gaucher, 2015a, Proposition 2.10], there exists a weak transition system Cyl(X) with the set of states \underline{S}(X) × \{0, 1\}, the set of actions \underline{L}(X) × \{0, 1\}, the labelling map the composite map μ : \underline{L}(X) × \{0, 1\} → \underline{L}(X) → Σ, and such that a tuple ((α, ϵ_{0}), (u_{1}, ϵ_{1}), …, (u_{n}, ϵ_{n}), (β, ϵ_{n+1})) is a transition of Cyl(X) if and only if the tuple (α, u_{1}, …, u_{n}, β) is a transition of X.

5.1. Notation. Let Z ⊂ \underline{S}(X). The ω-final lift of the map

ω(Cyl(X)) ⟶ (Z × \{0\} ⊔ (\underline{S}(X)\Z) × \{0, 1\}, \underline{L}(X) × \{0, 1\})

of Set^{\{s\}∪Σ} taking (s, ϵ) ∈ Z×\{0, 1\} to (s, 0) and which is the identity on (\underline{S}(X)\Z)×\{0, 1\} and on \underline{L}(X) × \{0, 1\} is denoted by Cyl(X)//Z.

The set of transitions of Cyl(X)//Z is the set of tuples ((α, ϵ_{0}), (u_{1}, ϵ_{1}), …, (u_{n}, ϵ_{n}), (β, ϵ_{n+1})) such that (α, u_{1}, …, u_{n}, β) is a transition of X. Indeed, the ω-final structure contains this set of tuples and this set of tuples obviously satisfies the multiset axiom and the patching axiom; consequently, it is the ω-final structure.

By [Gaucher, 2015a, Theorem 3.3], if the weak transition system X is cubical, then the weak transition system Cyl(X) introduced above is cubical as well. The map

ω(Cyl(X)) ⟶ (Z × \{0\} ⊔ (\underline{S}(X)\Z) × \{0, 1\}, \underline{L}(X) × \{0, 1\})

of Set^{\{s\}∪Σ} induces the identity of \underline{L}(X) × \{0, 1\} on actions, and thus, is onto on actions. By Theorem 2.4, we deduce that if the weak transition system X is cubical, then the weak transition system Cyl(X)//Z is cubical as well.

5.2. Notation. Let Z ⊂ \underline{S}(X). The ω-final lift of the map of Set^{\{s\}∪Σ}

ω(Cyl(X)) ⟶ (Z × \{0\} ⊔ (\underline{S}(X)\Z) × \{0, 1\}, \underline{L}(X))

taking (s, ϵ) ∈ Z × \{0, 1\} to (s, 0) and taking the action (u, ϵ) ∈ \underline{L}(X) × \{0, 1\} to u is denoted by Cyl(X)///Z.

5.3. Proposition. Let X be a cubical transition system. Let Z ⊂ \underline{S}(X) be a subset of the set of states of X. The weak transition system Cyl(X)///Z is cubical. A tuple ((α, ϵ_{0}), u_{1}, …, u_{n}, (β, ϵ_{n+1})) is a transition of Cyl(X)///Z if and only if the tuple (α, u_{1}, …, u_{n}, β) is a transition of X. Moreover, if X satisfies CSA1, then Cyl(X)///Z satisfies CSA1 as well.

Proof. By Theorem 2.4, the weak transition system Cyl(X)///Z is cubical since the projection map \underline{L}(X) × \{0, 1\} → \underline{L}(X) is onto. The set of transitions of Cyl(X)///Z is the ω-final structure generated by the set of tuples

T = \{((α, ϵ_{0}), u_{1}, …, u_{n}, (β, ϵ_{n+1})) | (α, u_{1}, …, u_{n}, β) ∈ \underline{T}(X)\}.

The set T of transitions satisfies the multiset axiom and the patching axiom. Therefore it is the ω-final structure: T = \underline{T}(Cyl(X)///Z). Assume that X satisfies CSA1. Let ((α, ϵ_{0}), u, (β, ϵ_{1})) and ((α, ϵ_{0}), v, (β, ϵ_{1})) be two transitions of the cubical transition system Cyl(X)///Z with μ(u) = μ(v). Then the tuples (α, u, β) and (α, v, β) are two transitions of X. Since X satisfies CSA1 by hypothesis, we obtain u = v. Consequently, Cyl(X)///Z satisfies CSA1 if X does.

5.4. Definition. [Gaucher, 2015a] Let X be a weak transition system. A state α of X is internal if there exists three transitions (γ, u_{1}, …, u_{n}, δ), (γ, u_{1}, …, u_{p}, α) and (α, u_{p+1}, …, u_{n}, δ) with n ⩾ 2 and p ⩾ 1. A state α is external if it is not internal.

5.5. Notation. The set of internal states of a weak transition system X is denoted by \underline{I}(X). The complement is denoted by \underline{E}(X) = \underline{S}(X)\ \underline{I}(X).

For any map f : X → Y of weak transition systems, we have f(\underline{I}(X)) ⊂ \underline{I}(Y): any internal state of X is mapped to an internal state of Y. In general, we have f(\underline{E}(X)) ⊈ \underline{E}(Y). In the example of the inclusion 00 ⟶^{u} 01 ⟶^{v} 11 ⊂ C_{2}[μ(u), μ(v)], all states of the domains are external, and the middle state 01 is mapped to an internal state of C_{2}[μ(u), μ(v)]. We actually have the following characterization:

5.6. Proposition. A state α of a cubical transition systems X is internal if and only if there exist three transitions (γ, u_{1}, u_{2}, δ), (γ, u_{1}, α) and (α, u_{2}, δ).

Proof. The “if” part is a consequence of the definition. The “only if” part is a consequence of the fact that X is cubical.

5.7. Proposition. Let X be a Cattani-Sassone transition system. Then the cubical transition system Cyl(X)/// \underline{I}(X) is a Cattani-Sassone transition system.

Proof. Consider the five transitions

((α, ϵ_{0}), u_{1}, …, u_{n}, (β, ϵ_{n+1}))
((α, ϵ_{0}), u_{1}, …, u_{p}, (γ, ϵ)), ((γ, ϵ), u_{p+1}, …, u_{n}, (β, ϵ_{n+1}))
((α, ϵ_{0}), u_{1}, …, u_{p}, (γ′, ϵ′)), ((γ′, ϵ′), u_{p+1}, …, u_{n}, (β, ϵ_{n+1}))

of Cyl(X)/// \underline{I}(X). Then the five tuples

(α, u_{1}, …, u_{n}, β)
(α, u_{1}, …, u_{p}, γ), (γ, u_{p+1}, …, u_{n}, β)
(α, u_{1}, …, u_{p}, γ′), (γ′, u_{p+1}, …, u_{n}, β)

are transitions of X. Since X is regular, we have γ = γ′. And since γ = γ′ is an internal state of X, we have (γ, ϵ) = (γ, 0) and (γ′, ϵ) = (γ′, 0) in Cyl(X)/// \underline{I}(X). We deduce that Cyl(X)/// \underline{I}(X) is regular. The proof is complete using Proposition 5.3.

5.8. Theorem. Let X be a Cattani-Sassone transition system. Then there is the natural isomorphism CSA_{1} CSA_{2} Cyl(X) ≅ Cyl(X)/// \underline{I}(X).

Proof. By [Gaucher, 2015a, Lemma 3.14], we have the isomorphism of weak transition systems

CSA_{2} Cyl(X) ≅ Cyl(X)// \underline{I}(X).

In particular, this means that Cyl(X)// \underline{I}(X) is regular. Let u ∈ \underline{L}(X). Since X is cubical, there exists a transition (α_{u}, u, β_{u}) of X. We deduce that ((α_{u}, 0), (u, 0), (β_{u}, 0)) and ((α_{u}, 0), (u, 1), (β_{u}, 0)) are two transitions of Cyl(X), and therefore two transitions of Cyl(X)// \underline{I}(X). Consider the map ϕ_{u} : C_{1}[μ(u)] ⊔_{0_{1},1_{1}} C_{1}[μ(u)] → Cyl(X)// \underline{I}(X) which sends the two transitions of the domain to the transitions ((α_{u}, 0), (u, 0), (β_{u}, 0)) and ((α_{u}, 0), (u, 1), (β_{u}, 0)) respectively. Consider the pushout diagram of RTS

[figure: ⨆_{u∈\underline{L}(X)} C_{1}[μ(u)] ⊔_{0_{1},1_{1}} C_{1}[μ(u)]; ⨆_{u∈\underline{L}(X)} ϕ_{u}; Cyl(X)// \underline{I}(X); ⨆_{u∈\underline{L}(X)} C_{1}[μ(u)]; Z.]

By Theorem 3.3, the set of states \underline{S}(Z) is a quotient of the set of states \underline{S}(Cyl(X)// \underline{I}(X)), the set of actions \underline{L}(Z) of Z is equal to \underline{L}(X) and the set of transitions of Z is given by the ω-final structure. The map of Set^{{s}∪Σ}

ω(Cyl(X)) ⟶ (\underline{I}(X) × \{0\} ⊔ \underline{E}(X) × \{0, 1\}, \underline{L}(X))

factors as a composite

ω(Cyl(X)) ⟶ (\underline{I}(X) × \{0\} ⊔ \underline{E}(X) × \{0, 1\}, \underline{L}(X) × \{0, 1\}) ⟶ (\underline{I}(X) × \{0\} ⊔ \underline{E}(X) × \{0, 1\}, \underline{L}(X))

where the left hand map is the identity on \underline{L}(X)×\{0, 1\}. Consequently, the map Cyl(X) → Cyl(X)/// \underline{I}(X) factors uniquely as a composite

Cyl(X) → Cyl(X)// \underline{I}(X) → Cyl(X)/// \underline{I}(X).

The right-hand map

Cyl(X)// \underline{I}(X) → Cyl(X)/// \underline{I}(X)

is bijective on states and Cyl(X)/// \underline{I}(X) is obtained from Cyl(X)// \underline{I}(X) by making the identifications (u, 0) = (u, 1) for all actions u of X. Consequently, by the universal property of the pushout, the map Cyl(X)// \underline{I}(X) → Cyl(X)/// \underline{I}(X) factors uniquely as a composite

Cyl(X)// \underline{I}(X) ⟶ Z ⟶ Cyl(X)/// \underline{I}(X).

The latter composite set map yields the factorization of Id_{\underline{S}(Cyl(X)// \underline{I}(X))} as the composite

\underline{S}(Cyl(X)// \underline{I}(X)) ↠ \underline{S}(Z) ⟶ \underline{S}(Cyl(X)/// \underline{I}(X)).

We deduce that the left-hand map is one-to-one, and then bijective. We have obtained the isomorphism Z ≅ Cyl(X)/// \underline{I}(X) because the two Cattani-Sassone transition systems are the ω-final lift of the same map of Set^{{s}∪Σ}. We obtain a factorization of the canonical map Cyl(X)// \underline{I}(X) → 1 as a composite Cyl(X)// \underline{I}(X) → Cyl(X)/// \underline{I}(X) → 1 where the left-hand map belongs to cell_{RTS}(U) and where, by Proposition 5.3 and Proposition 4.2, the right-hand map belongs to inj_{RTS}(U). We deduce the isomorphism CSA_{1}(Cyl(X)// \underline{I}(X)) ≅ Cyl(X)/// \underline{I}(X).

5.9. Notation. For every X ∈ CSTS, let Cyl^{CSTS}(X) := CSA_{1} CSA_{2} Cyl(X).

Let X be an object of CSTS. The cylinder Cyl^{CSTS}(X) of X in CSTS is then the Cattani-Sassone transition systems with the set of states \underline{I}(X) × \{0\} ⊔ \underline{E}(X) × \{0, 1\}, the set of actions \underline{L}(X) with the same labelling map as X, and such that a tuple

((α, ϵ_{0}), u_{1}, …, u_{n}, (β, ϵ_{n+1}))

is a transition of Cyl^{CSTS}(X) if and only if the tuple (α, u_{1}, …, u_{n}, β) is a transition of X. The canonical map γ^{ϵ} : X → Cyl^{CSTS}(X) with ϵ ∈ {0, 1} is induced by the mapping α ↦ (α, ϵ) for α ∈ \underline{S}(X)\ \underline{I}(X) or ϵ = 0, by the mapping α ↦ (α, 0) for α ∈ \underline{I}(X) and ϵ = 1 and by the identity of \underline{L}(X) on actions. The canonical map Cyl^{CSTS}(X) → X is induced by the mapping (α, ϵ) ↦ α on states and by the identity of \underline{L}(X) on actions.

5.10. Proposition. For every Cattani-Sassone transition system X, the unit map

CSA_{2} Cyl(X) → CSA_{1} CSA_{2} Cyl(X)

is split epic.

Proof. For every Cattani-Sassone transition system X, the map

CSA_{2} Cyl(X) → CSA_{1} CSA_{2} Cyl(X)

is the identity on states and takes the action (u, ϵ) of CSA_{2} Cyl(X) to the action u of CSA_{1} CSA_{2} Cyl(X). The inclusion map

CSA_{1} CSA_{2} Cyl(X) ⊂ CSA_{2} Cyl(X)

induced by the identity on states and the mapping u ↦ (u, 0) on actions yields a section of the map CSA_{2} Cyl(X) → CSA_{1} CSA_{2} Cyl(X).

5.11. Definition. Let n ⩾ 1 and x_{1}, …, x_{n} ∈ Σ. Let ∂C_{n}[x_{1}, …, x_{n}] be the regular transition system defined by removing from the n-cube C_{n}[x_{1}, …, x_{n}] all its n-transitions. It is called the boundary of C_{n}[x_{1}, …, x_{n}].

5.12. Notation. Let

I^{CTS} = {C : ∅ → {0}} ∪ {∂C_{n}[x_{1}, …, x_{n}] ⊂ C_{n}[x_{1}, …, x_{n}] | n ⩾ 1 and x_{1}, …, x_{n} ∈ Σ} ∪ {C_{0} ⊔ C_{0} ⊔ C_{1}[x] →↑x↑| x ∈ Σ}

where the maps C_{0} ⊔ C_{0} ⊔ C_{1}[x] →↑x↑ for x running over Σ are defined to be bijective on states.

The definition of I^{CTS} is not the same as the one of [Gaucher, 2015a]. The maps C_{1}[x] →↑x↑ for x running over Σ are replaced by the maps C_{0} ⊔ C_{0} ⊔ C_{1}[x] →↑x↑ for x running over Σ which are defined to be bijective on states. The class of maps cell_{CTS}(I^{CTS}) with I^{CTS} defined as above is exactly the class of monomorphisms of weak transition systems (i.e. one-to-one on states and actions by [Gaucher, 2011, Proposition 3.1]) between cubical transition systems by [Gaucher, 2015a, Theorem 3.7] (which is fixed in Appendix A). This choice is more convenient because the maps C_{0} ⊔ C_{0} ⊔ C_{1}[x] →↑x↑ for x ∈ Σ are bijective on states and on actions. Note that the maps C_{0} ⊔ C_{0} ⊔ C_{1}[x] →↑x↑ for x running over Σ are already used e.g. in the proof of [Gaucher, 2014b, Theorem 4.6].

Let X be a weak transition system. By [Gaucher, 2015a, Proposition 2.14], there exists a well-defined weak transition system Path(X) with the set of states \underline{S}(X) × \underline{S}(X), the set of actions is the set \underline{L}(X) ×_{Σ} \underline{L}(X) and the labelling map is the composite map \underline{L}(X)×_{Σ} \underline{L}(X) → \underline{L}(X) → Σ and such that a tuple ((α^{0}, α^{1}), (u_{1}^{0}, u_{1}^{1}), …, (u_{n}^{0}, u_{n}^{1}), (β^{0}, β^{1})) is a transition if and only if for any ϵ_{0}, …, ϵ_{n+1} ∈ {0, 1}, the tuple (α^{ϵ_{0}}, u_{1}^{ϵ_{1}}, …, u_{n}^{ϵ_{n}}, β^{ϵ_{n+1}}) is a transition of X. The functor Path : WTS → WTS is a right adjoint of the functor Cyl : WTS → WTS by [Gaucher, 2015a, Proposition 2.15]. The right adjoint Path^{CTS} : CTS → CTS of the restriction of Cyl to the full subcategory of cubical transition systems is the composite map

Path^{CTS} : CTS ⊂ WTS ⟶^{Path} WTS ⟶ CTS

where the right-hand map is the coreflection.

5.13. Proposition. Let X be a cubical transition system. The cubical transition system Path^{CTS}(X) can be identified to a subobject of Path(X) having the same set of states.

Proof. By [Gaucher, 2015a, Proposition 3.4], the counit map Path^{CTS}(X) → Path(X) is bijective on states and one-to-one on actions and transitions.

5.14. Proposition. For every Cattani-Sassone transition system X, the cubical transition system Path^{CTS}(X) is a Cattani-Sassone regular transition system.

Proof. Since X is regular, the cubical transition system Path^{CTS}(X) is regular as well by [Gaucher, 2015a, Proposition 3.10]. Let

((α^{−}, α^{+}), (u^{−}, u^{+}), (β^{−}, β^{+})), ((α^{−}, α^{+}), (v^{−}, v^{+}), (β^{−}, β^{+}))

be two transitions of Path^{CTS}(X). By definition of Path^{CTS}(X), the tuples (α^{−}, u^{±}, β^{−}) and (α^{−}, v^{±}, β^{−}) are transitions of X. Since X satisfies CSA1, we deduce that u^{−} = u^{+} = v^{+} = v^{−}. We obtain (u^{−}, u^{+}) = (v^{−}, v^{+}), which means that Path^{CTS}(X) satisfies CSA1.

5.15. Theorem. There exists a left determined model structure on CSTS with the set of generating cofibrations I^{CTS}. This model category is an Olschok model category with the very good cartesian cylinder Cyl^{CSTS} : CSTS → CSTS. All objects are cofibrant.

Proof. By [Gaucher, 2015a, Theorem 3.16], there exists a unique left determined model structure on RTS such that the set of generating cofibrations is CSA_{2}(I^{CTS}) = I^{CTS}. This model structure is an Olschok model structure with the very good cylinder CSA_{2} Cyl and, by [Gaucher, 2015a, Proposition 3.10], with the cocylinder Path^{CTS}. We want to restrict this model structure to the subcategory CSTS. 1) It turns out that CSTS is a reflective subcategory of RTS by Proposition 4.4. 2) We have CSA_{1}(I^{CTS}) = I^{CTS} since every domain and every codomain of a map of I^{CTS} satisfies CSA1 and since CSTS is a full subcategory of RTS. 3) We have Path^{CTS}(CSTS) ⊂ CSTS by Proposition 5.14. 4) The map CSA_{2} Cyl(X) → CSA_{1} CSA_{2} Cyl(X) is split by Proposition 5.10. Therefore, we can apply [Gaucher, 2015c, Theorem 3.1] and the proof is complete.

The following proposition will be used later:

5.16. Proposition. Let f : X → Y be a map of CSTS. If f is one-to-one on states and on actions, then it belongs to cell_{CSTS}(I^{CTS}). The converse is false: there exist maps of cell_{CSTS}(I^{CTS}) which are not one-to-one on states and on actions.

Proof. Since f is one-to-one on states and on actions, it belongs to cell_{CTS}(I^{CTS}). The inclusion functor CSTS ⊂ CTS has a left adjoint CSA_{1} CSA_{2} : CTS → CSTS. Thus, the functor CSA_{1} CSA_{2} is colimit-preserving and CSA_{1} CSA_{2}(f) : CSA_{1} CSA_{2}(X) → CSA_{1} CSA_{2}(Y) belongs to cell_{CSTS}(CSA_{1} CSA_{2}(I^{CTS})). Since CSA_{1} CSA_{2}(f) = f and CSA_{1} CSA_{2}(I^{CTS}) = I^{CTS}, we deduce that f belongs to cell_{CSTS}(I^{CTS}). Let x ∈ Σ. The map γ_{C_{2}[x,x]} : C_{2}[x, x] ⊔ C_{2}[x, x] → Cyl^{CSTS}(C_{2}[x, x]) is a cofibration of CSTS. The state 01 is an internal state of C_{2}[x, x]. Thus, the states 01 of the two copies of C_{2}[x, x] are identified to the same state of Cyl^{CSTS}(C_{2}[x, x]). This means that γ_{C_{2}[x,x]} is not one-to-one on states. The actions (x, 1) of the two copies of C_{2}[x, x] are identified to the same action (x, 1) of Cyl^{CSTS}(C_{2}[x, x]). This implies that γ_{C_{2}[x,x]} is not one-to-one on actions.

6. Computation of the path functor

6.1. Proposition. Let X be a regular transition system. Consider the family of sets (T_{n})_{n⩾1} constructed by induction on n as follows:

• T_{1} is the set of triples ((α^{−}, α^{+}), u_{1}, (β^{−}, β^{+})) such that the triples (α^{±}, u_{1}, β^{±}) are transitions of X.

• For n ⩾ 2, T_{n} is the set of tuples ((α^{−}, α^{+}), u_{1}, …, u_{n}, (β^{−}, β^{+})) such that the tuples (α^{±}, u_{1}, …, u_{n}, β^{±}) are transitions of X and such that for all permutations σ of {1, …, n} and all 1 ⩽ p < n, there exists a pair of states (γ_{σ}^{−}, γ_{σ}^{+}) of X such that the tuple ((α^{−}, α^{+}), u_{σ(1)}, …, u_{σ(p)}, (γ_{σ}^{−}, γ_{σ}^{+})) belongs to T_{p} and such that the tuple ((γ_{σ}^{−}, γ_{σ}^{+}), u_{σ(p+1)}, …, u_{σ(n)}, (β^{−}, β^{+})) belongs to T_{n−p}.

Let T = ⋃_{n⩾1} T_{n}. Then we have:

a) For every transition (α, u_{1}, …, u_{n}, β) of X, the tuple ((α, α), u_{1}, …, u_{n}, (β, β)) belongs to T .

b) The set of states \underline{S}(X)×\underline{S}(X), the labelling map μ : \underline{L}(X) → Σ and the set of tuples T assemble to a regular transition system denoted by PseudoPath(X).

Proof. a) Consider the statement P_{n} defined for n ⩾ 1 by:

for every transition (α, u_{1}, …, u_{m}, β) of X with m ⩽ n, the tuple
((α, α), u_{1}, …, u_{m}, (β, β)) belongs to T .

Let (α, u_{1}, β) be a transition of X. The tuple ((α, α), u_{1}, (β, β)) belongs to T_{1} by definition of T_{1}. We have proved P_{1}. Let n ⩾ 2. Assume P_{n−1}. We want to prove P_{n}. Let (α, u_{1}, …, u_{n}, β) be a transition of X. Let 1 ⩽ p < n. Let σ be a permutation of {1, …, n}. Since X is cubical, there exists a state γ of X such that the tuples (α, u_{σ(1)}, …, u_{σ(p)}, γ) and (γ, u_{σ(p+1)}, …, u_{σ(n)}, β) are transitions of X. By the induction hypothesis, the tuples ((α, α), u_{σ(1)}, …, u_{σ(p)}, (γ, γ)) and ((γ, γ), u_{σ(p+1)}, …, u_{σ(n)}, (β, β)) belong to T since p ⩽ n − 1 and n − p ⩽ n − 1. Hence we have proved P_{n} from P_{n−1}.

b) The set of tuples T satisfies the multiset axiom because of the internal symmetry of its definition. Let ((α^{−}, α^{+}), u_{1}, …, u_{n}, (β^{−}, β^{+})) be an element of T with n ⩾ 3. Let p, q ⩾ 1 with p + q < n such that the tuples

((α^{−}, α^{+}), u_{1}, …, u_{n}, (β^{−}, β^{+})),
((α^{−}, α^{+}), u_{1}, …, u_{p}, (ν_{1}^{−}, ν_{1}^{+})), ((ν_{1}^{−}, ν_{1}^{+}), u_{p+1}, …, u_{n}, (β^{−}, β^{+})),
((α^{−}, α^{+}), u_{1}, …, u_{p+q}, (ν_{2}^{−}, ν_{2}^{+})), ((ν_{2}^{−}, ν_{2}^{+}), u_{p+q+1}, …, u_{n}, (β^{−}, β^{+}))

belong to T . Then by definition of T , the tuples

(α^{±}, u_{1}, …, u_{n}, β^{±}),
(α^{±}, u_{1}, …, u_{p}, ν_{1}^{±}), (ν_{1}^{±}, u_{p+1}, …, u_{n}, β^{±}),
(α^{±}, u_{1}, …, u_{p+q}, ν_{2}^{±}), (ν_{2}^{±}, u_{p+q+1}, …, u_{n}, β^{±})

are transitions of X. Since X satisfies CSA2, we obtain ν_{1}^{−} = ν_{1}^{+} = ν_{1} and ν_{2}^{−} = ν_{2}^{+} = ν_{2}. By the patching axiom, the tuple (ν_{1}, u_{p+1}, …, u_{p+q}, ν_{2}) is a transition of X. By a), we deduce that the ((ν_{1}^{−}, ν_{1}^{+}), u_{p+1}, …, u_{p+q}, (ν_{2}^{−}, ν_{2}^{+})) belongs to T_{q}. We have proved that T satisfies the patching axiom and that the set of states \underline{S}(X) × \underline{S}(X), the labelling map μ : \underline{L}(X) → Σ and the set of tuples T assemble to a weak transition system PseudoPath(X). Let u be an action of X. Since X is cubical, there exists a transition (α, u, β) of X. Thus, the triple ((α, α), u, (β, β)) is a transition of PseudoPath(X). Hence, all actions of PseudoPath(X) are used. By definition of T , PseudoPath(X) satisfies the Intermediate state axiom. This means that PseudoPath(X) is a cubical transition system. Since X is regular, it satisfies CSA2. This means that in the definition of T , the equality γ_{σ}^{−} = γ_{σ}^{+} always holds and that this state is unique. Hence the cubical transition system PseudoPath(X) satisfies CSA2 as well.

The natural mapping X ↦ PseudoPath(X) yields a well-defined functor

PseudoPath : RTS → RTS.

6.2. Theorem. Let X be a Cattani-Sassone transition system. There exists a natural isomorphism PseudoPath(X) ≅ Path^{CTS}(X).

Proof. By definition of Path : WTS → WTS, the identity of \underline{S}(X) × \underline{S}(X) and the diagonal map \underline{L}(X) → \underline{L}(X) ×_{Σ} \underline{L}(X) induces a map of weak transition systems

PseudoPath(X) → Path(X).

This map is one-to-one on states and on actions, and therefore one-to-one on transitions by Proposition 2.3. By Proposition 6.1, the weak transition system PseudoPath(X) is cubical. Since CTS is a coreflective subcategory of WTS, the map PseudoPath(X) → Path(X) then factors uniquely as a composite

PseudoPath(X) → Path^{CTS}(X) → Path(X).

By Proposition 5.13, the cubical transition system Path^{CTS}(X) has the set of states \underline{S}(X) × \underline{S}(X) and the set of actions (of transitions resp.) of Path^{CTS}(X) is a subset of the set of actions (of transitions resp.) of Path(X), i.e. \underline{L}(X) ×_{Σ} \underline{L}(X). We deduce that the map PseudoPath(X) → Path^{CTS}(X) induces the identity of \underline{S}(X)×\underline{S}(X) on states and the diagonal of \underline{L}(X) on actions. Therefore, the set of actions of Path^{CTS}(X) contains the diagonal of \underline{L}(X). Let (u^{−}, u^{+}) ∈ \underline{L}(X)×_{Σ}\underline{L}(X) be an action of Path^{CTS}(X). Since Path^{CTS}(X) is cubical, there exists a transition ((α^{−}, α^{+}), (u^{−}, u^{+}), (β^{−}, β^{+})) of Path^{CTS}(X). Since the latter tuple is also a transition of Path(X) by Proposition 5.13, the triples (α^{±}, u^{±}, β^{±}) are transitions of X by definition of Path : WTS → WTS. Since X satisfies CSA1 by hypothesis, we deduce that u^{−} = u^{+}. Thus, the set of actions of Path^{CTS}(X) is a subset of the diagonal of \underline{L}(X). This implies that the set of actions of Path^{CTS}(X) is exactly the diagonal of \underline{L}(X). We deduce that the map PseudoPath(X) → Path^{CTS}(X) induces the bijection \underline{L}(X) ≅ \{(u, u) | u ∈ \underline{L}(X)\} on actions. For the sequel, the diagonal of \underline{L}(X) can be identified with the set \underline{L}(X).

We have proved so far that the map PseudoPath(X) → Path^{CTS}(X) is bijective on states (it is the identity of \underline{S}(X) × \underline{S}(X)) and bijective on actions (it is the bijection \underline{L}(X) ≅ \{(u, u) | u ∈ \underline{L}(X)\}). It is then one-to-one on transitions by Proposition 2.3. Let ((α^{−}, α^{+}), (u_{1}, u_{1}), …, (u_{n}, u_{n}), (β^{−}, β^{+})) be a transition of Path^{CTS}(X). It is a transition of Path(X) by Proposition 5.13. By definition of Path : WTS → WTS, the tuples (α^{±}, u_{1}, …, u_{n}, β^{±}) are transitions of X. If n = 1, then the tuple ((α^{−}, α^{+}), u_{1}, (β^{−}, β^{+})) is a transition of PseudoPath(X) by definition of PseudoPath(X). Assume that n ⩾ 2. Let σ be a permutation of {1, …, n}. Let 1 ⩽ p < n. Since Path^{CTS}(X) is cubical, there exists a pair of states (γ_{σ}^{−}, γ_{σ}^{+}) of X such that the tuples

((α^{−}, α^{+}), (u_{σ(1)}, u_{σ(1)}), …, (u_{σ(p)}, u_{σ(p)}), (γ_{σ}^{−}, γ_{σ}^{+}))

and

((γ_{σ}^{−}, γ_{σ}^{+}), (u_{σ(p+1)}, u_{σ(p+1)}), …, (u_{σ(n)}, u_{σ(n)}), (β^{−}, β^{+}))

are transitions of Path^{CTS}(X). By definition of Path : WTS → WTS, this implies that the tuples (α^{±}, u_{σ(1)}, …, u_{σ(p)}, γ_{σ}^{±}) and (γ_{σ}^{±}, u_{σ(p+1)}, …, u_{σ(n)}, β^{±}) are transitions of X. Therefore the tuple ((α^{−}, α^{+}), (u_{1}, u_{1}), …, (u_{n}, u_{n}), (β^{−}, β^{+})) is a transition of PseudoPath(X) by Proposition 6.1. We have proved that the map PseudoPath(X) → Path^{CTS}(X) is onto on transitions.

The path object of X in CSTS is then the Cattani-Sassone transition system denoted by Path^{CSTS}(X) with the set of states \underline{S}(X) × \underline{S}(X), the set of actions \underline{L}(X) and such that a tuple

((α^{−}, α^{+}), u_{1}, …, u_{n}, (β^{−}, β^{+}))

is a transition of Path^{CSTS}(X) if and only if the tuples (α^{±}, u_{1}, …, u_{n}, β^{±}) are transitions of X. The canonical map τ_{X} : X → Path^{CSTS}(X) is induced by the diagonal of \underline{S}(X) on states and the identity on actions. The canonical map π_{X}^{ϵ} : Path^{CSTS}(X) → X with ϵ ∈ \{0, 1\} is induced by the projection on the (ϵ + 1)-th component \underline{S}(X) × \underline{S}(X) → \underline{S}(X) on states and by the identity on actions.

Table 2 summarizes the computation of the cylinder functor and of the path functor of CSTS.

7. Characterization in the non star-shaped case

7.1. Proposition. Let X be a fibrant object of CSTS. Then the labelling map μ : \underline{L}(X) → Σ is one-to-one.

X  Cyl^{CSTS}(X)  Path^{CSTS}(X)
\underline{S}(X)  \underline{I}(X) × \{0\} ⊔ \underline{E}(X) × \{0, 1\}  \underline{S}(X) × \underline{S}(X)
\underline{L}(X)  \underline{L}(X)  \underline{L}(X)
\underline{T}(X)  ((α, ϵ_{0}), u_{1}, …, u_{n}, (β, ϵ_{n+1}))  ((α^{−}, α^{+}), u_{1}, …, u_{n}, (β^{−}, β^{+}))
such that (α, u_{1}, …, u_{n}, β) ∈ \underline{T}(X) such that (α^{±}, u_{1}, …, u_{n}, β^{±}) ∈ \underline{T}(X)

Table 2: Cylinder functor and path functor of CSTS

Proof. Let u and v be two actions of X with μ(u) = μ(v). Since X is cubical, there exist two transitions (α_{u}, u, β_{u}) and (α_{v}, v, β_{v}) of X. Consider the commutative diagram of CSTS

\xymatrix{\{0_{1}, 1_{1}\} = ∂C_{1}[μ(u)] \ar[r]^{\begin{matrix}0_{1} ↦ (α_{u}, α_{v}) \\ 1_{1} ↦ (β_{u}, β_{v}) \end{matrix}} \ar[d] & Path^{CSTS}(X) \ar[d]_{π^{0}} \\ C_{1}[μ(u)] \ar@{-->}[ur]^{ℓ} \ar[r]_{\begin{matrix}0_{1} ↦ α_{u} \\ 1_{1} ↦ β_{u} \\ (μ(u), 1) ↦ u \end{matrix}} & X.}

Since X is fibrant by hypothesis, it is injective with respect to the anodyne cofibration (∂C_{1}[μ(u)] ⊂ C_{1}[μ(u)]) ⋆ γ^{0}. By adjunction, we deduce that the lift ℓ in the diagram above exists. Therefore the triple ℓ(0_{1}, (μ(u), 1), 1_{1}) = ((α_{u}, α_{v}), u, (β_{u}, β_{v})) is a transition of Path^{CSTS}(X). This implies that the triple (α_{v}, u, β_{v}) is a transition of X. Since X satisfies CSA1, we deduce that u = v.

7.2. Proposition. Let X and Y be two objects of CSTS with Y fibrant. Then the set π_{CSTS}(X, Y) has at most one element: all maps from X to Y are homotopy equivalent.

Proof. Let f, g : X ⇉ Y be two maps of CSTS. We have μ(f(u)) = μ(g(u)) = μ(u) since maps of CSTS preserve labels. Since Y is fibrant, μ is one-to-one by Proposition 7.1. Thus, we deduce that f and g coincide on actions. Since X is cofibrant by Theorem 5.15 and Y fibrant by hypothesis, it suffices to prove that f and g are right homotopic to conclude the proof. The only possible definition of this right homotopy is H(α) = (f(α), g(α)) for all states α of X and H(u) = f(u) = g(u) = μ(u) for all actions u of X. We have to prove that H yields a well-defined map of transition systems, i.e. that for all transitions (α, u_{1}, …, u_{n}, β) of X, the tuple ((f(α), g(α)), H(u_{1}), …, H(u_{n}), (f(β), g(β))) is a transition of Path^{CSTS}(Y).

The n-transition (f(α), f(u_{1}), …, f(u_{n}), f(β)) gives rise to a (unique) map of weak transition systems C_{n}^{ext}[μ(u_{1}), …, μ(u_{n})] → Y (the definition of C_{n}^{ext}[μ(u_{1}), …, μ(u_{n})] is recalled in Section 2). Since Y satisfies CSA2, it factors (uniquely) as a composite

C_{n}^{ext}[μ(u_{1}), …, μ(u_{n})] → C_{n}[μ(u_{1}), …, μ(u_{n})] → Y

by [Gaucher, 2010a, Theorem 5.6]. We obtain the commutative diagram of CSTS

\xymatrix{\{0_{n}, 1_{n}\} \ar[r]^{\begin{matrix}0_{n} ↦ (f(α), g(α)) \\ 1_{n} ↦ (f(β), g(β)) \end{matrix}} \ar[d] & Path^{CSTS}(Y) \ar[d]_{π^{0}} \\ C_{n}[μ(u_{1}), …, μ(u_{n})] \ar@{-->}[ur]^{ℓ} \ar[r] & Y.}

Since Y is fibrant by hypothesis, it is injective with respect to the anodyne cofibration ({0_{n}, 1_{n}} ⊂ C_{n}[μ(u_{1}), …, μ(u_{n})]) ⋆ γ^{0}. By adjunction, we deduce that the lift ℓ in the diagram above exists. By Table 2, the right vertical map π^{0} is the identity on actions. We deduce that the tuple

ℓ(0_{n}, (μ(u_{1}), 1), (μ(u_{n}), n), 1_{n}) = ((f(α), g(α)), f(u_{1}), …, f(u_{n}), (f(β), g(β)))

is a transition of Path^{CSTS}(Y).

7.3. Proposition. Let w : X → Y be a map of CSTS which is onto on states, on actions and on transitions. Then w is a weak equivalence.

Proof. Let Z be a fibrant object. We have to prove that the set map π_{CSTS}(Y, Z) → π_{CSTS}(X, Z) induced by the precomposition with w is bijective. By Proposition 7.2, it suffices to prove that it is onto. Suppose first that Z = ∅. Let f : X → Z. Then X = ∅. Since w : X → Y is onto on states, Y does not contain any state. Consequently, Y = ∅ because all actions of Y are used. We deduce that w = Id_{∅}, and that π_{CSTS}(Y, Z) = π_{CSTS}(X, Z) = π_{CSTS}(∅, ∅) = {Id_{∅}}. Suppose now that Z ≠ ∅. By Proposition 7.1, we have the inclusion \underline{L}(Z) ⊂ Σ. Let f : X → Z be a map of CSTS. Let ξ be a state of Z. Let g : Y → Z defined on states by g(α) = ξ and on actions by g(u) = μ(u). It suffices to prove that g yields a well-defined map of CSTS from Y to Z to complete the proof. Let (α, u_{1}, …, u_{n}, β) be a transition of Y. By hypothesis, there exists a transition (\overline{α}, \overline{u_{1}}, …, \overline{u_{n}}, \overline{β}) of X with w(\overline{α}, \overline{u_{1}}, …, \overline{u_{n}}, \overline{β}) = (α, u_{1}, …, u_{n}, β). We obtain the transition (f(\overline{α}), μ(u_{1}), …, μ(u_{n}), f(\overline{β})) of Z which yields a map of cubical transition systems C_{n}[μ(u_{1}), …, μ(u_{n})] → Z. Since Z is fibrant, it is injective with respect to the anodyne cofibration ({0_{n}, 1_{n}} ⊂ C_{n}[μ(u_{1}), …, μ(u_{n})])⋆γ^{0}. By adjunction, we deduce that the lift ℓ exists in the commutative diagram of solid arrows of CSTS

\xymatrix{\{0_{n}, 1_{n}\} \ar[r]^{\begin{matrix}0_{n} ↦ (f(\overline{α}), ξ) \\ 1_{n} ↦ (f(\overline{β}), ξ) \end{matrix}} \ar[d] & Path^{CSTS}(Z) \ar[d]_{π^{0}} \\ C_{n}[μ(u_{1}), …, μ(u_{n})] \ar@{-->}[ur]^{ℓ} \ar[r]_{\begin{matrix}0_{n} ↦ f(\overline{α}) \\ 1_{n} ↦ f(\overline{β}) \\ (μ(u_{i}), i) ↦ μ(u_{i}) \end{matrix}} & Z.}

Therefore the tuple ((f(\overline{α}), ξ), μ(u_{1}), …, μ(u_{n}), (f(\overline{β}), ξ)) is a transition of Path^{CSTS}(Z). We deduce that the tuple (ξ, μ(u_{1}), …, μ(u_{n}), ξ) is a transition of Z. We have proved that g(α, u_{1}, …, u_{n}, β) = (ξ, μ(u_{1}), …, μ(u_{n}), ξ) is a transition of Z and that g is a well-defined map of Cattani-Sassone transition systems.

7.4. Theorem. Let R : {0, 1} → {0}. Every map of cell_{CSTS}({R}) is onto on states, on actions and on transitions. Every map of cell_{CSTS}({R}) is a weak equivalence of CSTS.

Proof. Every pushout of R : {0, 1} → {0} is onto on states, on actions and on transitions by Corollary 4.6. Every transfinite composition of pushouts of R : {0, 1} → {0} is also onto on states, on actions and on transitions by Theorem 4.5. We deduce the first assertion of the theorem. The second assertion of the theorem is then a corollary of Proposition 7.3.

Note that every map of CSA_{1}(CSA_{2}(I^{CTS})) = I^{CTS} is a map between finitely presentable objects. Thus, by [Raptis and Rosický, 2015, Proposition 4.1], the class of weak equivalences of CSTS is closed under transfinite composition.

Let X be a Cattani-Sassone transition system. For all objects X of CSTS, the unique map X → 1 from X to the terminal object of CSTS factors functorially as a composite

\xymatrix{X \ar[r]^{∈cell_{CSTS}(\{R\})} & R^{⊥}(X) \ar[r]^{∈inj_{CSTS}(\{R\})} & 1}

in CSTS where the left-hand map belongs to cell_{CSTS}({R}) and the right-hand map belongs to inj_{CSTS}({R}). Since all maps of cell_{CSTS}({R}) are epic by Theorem 7.4, this decomposition is unique up to isomorphism by [Gaucher, 2015a, Proposition A.1]. Since R : {0, 1} → {0} is epic, an object is R-injective if and only if it is R-orthogonal, i.e. if and only if X has at most one state. Let us denote by \overline{CSTS} this small-orthogonality class. The functor R^{⊥} : CSTS → \overline{CSTS} is a left adjoint of the inclusion \overline{CSTS} ⊂ CSTS. By [Adámek and Rosický, 1994, Theorem 1.39], the category \overline{CSTS} is locally presentable.

7.5. Theorem. The left adjoint R^{⊥} : CSTS → inj_{CSTS}({R}) induces a Quillen equivalence between the model category CSTS and the category \overline{CSTS} equipped with the discrete model category structure.

Proof. For any R-orthogonal Cattani-Sassone transition system X, we have by Table 2 the equalities Path^{CSTS}(X) = X and R^{⊥}(Cyl^{CSTS}(X)) = X. Using [Gaucher, 2015c, Theorem 3.1], we obtain a left determined Olschok model structure on \overline{CSTS} such that the cylinder and the path functors are the identity functor. Therefore, we have the equalities π\overline{CSTS}(X, Y) = πl ; \overline{CSTS}(X, Y) = πr ; \overline{CSTS}(X, Y) = \overline{CSTS}(X, Y) for all R-orthogonal Cattani-Sassone transition systems X and Y. This means that the weak equivalences of \overline{CSTS} are the isomorphisms. For every R-orthogonal Cattani-Sassone transition system Y, the canonical map R^{⊥}(Y) → Y is an isomorphism. We deduce that the left adjoint R^{⊥} : CSTS → \overline{CSTS} is a homotopically surjective left Quillen adjoint from CSTS to \overline{CSTS} equipped with the discrete model structure. By Theorem 7.4, the canonical map X → R^{⊥}(X) is a weak equivalence of CSTS for all Cattani-Sassone transition systems X. Thus, this left Quillen adjoint is a left Quillen equivalence.

7.6. Corollary. A map f of CSTS is a weak equivalence if and only if R^{⊥}(f) is an isomorphism.

Proof. Since all objects of CSTS are cofibrant by Theorem 5.15, a weak equivalence f is mapped to a weak equivalence R^{⊥}(f) of \overline{CSTS}, i.e. an isomorphism. Conversely, if R^{⊥}(f) is an isomorphism, then by Theorem 7.4 and the two-out-of-three property, f is a weak equivalence of CSTS.

8. Homotopy theory of star-shaped objects

A pointed (Cattani-Sassone) transition system is a pair (X, ∗) where X is a Cattani-Sassone transition system and where ∗ is a state of X called the base state. A map of pointed transition system is a map of CSTS preserving the base state. The category of pointed (Cattani-Sassone) transition systems is denoted by CSTS_{∗}. Let ω^{∗} : CSTS_{∗} → CSTS be the forgetful functor. It is a right adjoint which preserves connected colimits. The left adjoint ρ^{∗} : CSTS → CSTS_{∗} is defined on objects by ρ^{∗}(X) = ({∗} ⊔ X, ∗) and on morphisms by ρ^{∗}(f) = Id_{{∗}} ⊔f. By [Adámek and Rosický, 1994, Proposition 1.57] and [Hirschhorn, 2015, Theorem 2.7], there exists a structure of combinatorial model category on CSTS_{∗} such that the cofibrations (the fibrations, the weak equivalences resp.) belong to the inverse image by the forgetful functor of the class of cofibrations (fibrations, weak equivalences resp.) of CSTS. The set of generating cofibrations of the category CSTS_{∗} is the set ρ^{∗}(I^{CTS}).

Note that pointed weak, cubical or regular transition systems are defined exactly as pointed Cattani-Sassone transition systems. Without further precision, a pointed transition system is supposed to be a pointed Cattani-Sassone transition system.

8.1. Remark. It is important to keep in mind that the functors ω : WTS → Set^{{s}∪Σ} and ω^{∗} : CSTS_{∗} → CSTS are two different functors.

8.2. Notation. Let \underline{S}(X, ∗) = \underline{S}(X), \underline{L}(X, ∗) = \underline{L}(X) and \underline{T}(X, ∗) = \underline{T}(X).

Let Cyl_{∗} : CSTS_{∗} → CSTS_{∗} be the functor defined by the following natural pushout diagram of CSTS ((X, ∗) being an object of CSTS_{∗}):

[figure: {∗} ⊔ {∗}; {∗}; Cyl_{∗}(X); X ⊔ X; γ_{X}; Cyl^{CSTS}(X); ω^{∗}(Cyl_{∗}(X, ∗)),]

where the pushout is taken in CSTS.

8.3. Theorem. The combinatorial model category CSTS_{∗} is a left determined Olschok model category with the very good cylinder Cyl_{∗} : CSTS_{∗} → CSTS_{∗}.

Proof. By Proposition 5.16, every map with domain a singleton is a cofibration of CSTS. The map {∗}⊔{∗} → Cyl^{CSTS}({∗}) is an isomorphism. By [Gaucher, 2015c, Theorem 5.8], we deduce that the model category CSTS_{∗} is an Olschok model category. Let (X, ∗) be an object of CSTS_{∗}. We know that the set of states of Cyl^{CSTS}(X) is \underline{I}(X)×\{0\}⊔\underline{E}(X)×\{0, 1\}, that the set of actions of Cyl^{CSTS}(X) is \underline{L}(X), and that a tuple ((α, ϵ_{0}), u_{1}, …, u_{n}, (β, ϵ_{n+1})) is a transition of Cyl^{CSTS}(X) if and only if the tuple (α, u_{1}, …, u_{n}, β) is a transition of X. Consider now the pushout diagram of cubical transition systems

[figure: {∗} ⊔ {∗}; {∗}; X ⊔ X; γ_{X}; Cyl^{CSTS}(X); U.]

By Lemma 3.2, the forgetful functor mapping a cubical transition system to its set of states (to its set of actions resp.) is colimit-preserving. We deduce that the set of states of U is (\underline{I}(X) ∪ \{∗\}) × \{0\} ⊔ (\underline{S}(X)\(\underline{I}(X) ∪ \{∗\})) × \{0, 1\} and that the set of actions of U is \underline{L}(X). Therefore, the cubical transition system U is the ω-final lift of the cocone of Set^{{s}∪Σ} consisting of the unique map

ω(Cyl(X)) ⟶ ((\underline{I}(X) ∪ \{∗\}) × \{0\} ⊔ (\underline{S}(X)\(\underline{I}(X) ∪ \{∗\})) × \{0, 1\}, \underline{L}(X)).

By Proposition 5.3, we obtain U = Cyl(X)///(\underline{I}(X) ∪ \{∗\}). There is an inclusion

Cyl(X)///(\underline{I}(X) ∪ \{∗\}) ⊂ Cyl(X)/// \underline{I}(X).

By Theorem 5.8, we obtain the inclusion

Cyl(X)///(\underline{I}(X) ∪ \{∗\}) ⊂ CSA_{1} CSA_{2} Cyl(X).

By Proposition 2.5, the cubical transition system Cyl(X)///(\underline{I}(X)∪\{∗\}) is regular. And it satisfies CSA1 by Proposition 5.3. Thus, the cubical transition system Cyl(X)///(\underline{I}(X) ∪ {∗}) is a Cattani-Sassone transition system and we obtain the pushout diagram of CSTS

[figure: \{∗\} ⊔ \{∗\}; \{∗\}; X ⊔ X; γ_{X}; Cyl^{CSTS}(X); Cyl(X)///(\underline{I}(X) ∪ \{∗\}).]

We deduce the isomorphism

ω^{∗}(Cyl_{∗}(X, ∗)) ≅ Cyl(X)///(\underline{I}(X) ∪ \{∗\}).

The inclusion Cyl(X)///(\underline{I}(X)∪\{∗\}) ⊂ CSA_{1} CSA_{2} Cyl(X) yields a section of the bottom horizontal map. Thus, by [Gaucher, 2015c, Corollary 5.9], the Olschok model category CSTS_{∗} is left determined and the functor Cyl_{∗} : CSTS_{∗} → CSTS_{∗} yields a very good cylinder.

After the previous calculations, the following definition makes sense:

8.4. Definition. A state of a pointed transition system (X, ∗) is internal if it is equal to the base state ∗ or it is internal in X. Let \underline{I}(X, ∗) = \underline{I}(X) ∪ \{∗\}, and \underline{E}(X, ∗) = \underline{S}(X)\ \underline{I}(X, ∗). A state which is not internal is external. Note that for any Cattani-Sassone transition system X, there are the equalities \underline{I}(ρ^{∗}(X), ∗) = \underline{I}(X) ⊔ \{∗\} and \underline{E}(ρ^{∗}(X), ∗) = \underline{E}(X).

Thus, we have for any pointed transition system (X, ∗) the equalities Cyl^{CSTS}(X) = Cyl(X)/// \underline{I}(X) and ω^{∗}(Cyl_{∗}(X, ∗)) = Cyl(X)/// \underline{I}(X, ∗). For any map f : (X, ∗) → (Y, ∗) of pointed transition systems, we have f(\underline{I}(X, ∗)) ⊂ \underline{I}(Y, ∗): any internal state of (X, ∗) is mapped to an internal state of (Y, ∗). In general, we have f(\underline{E}(X, ∗)) ⊈ \underline{E}(Y, ∗).

8.5. Definition. The path (P (w), 0) indexed by w with n ⩾ 0, w = x_{1} … x_{n} ∈ Σ^{n} for n ⩾ 0 is by definition the pointed transition system

\xymatrix{P (w) = 0 \ar[r]^{(x_{1},1)} & 1 \ar[r]^{(x_{2},2)} & 2 … n − 1 \ar[r]^{(x_{n},n)} & n} ,

which means that the set of actions is {(x_{i}, i) | 1 ⩽ i ⩽ n} with the labelling map μ(x_{i}, i) = x_{i} for 1 ⩽ i ⩽ n. Let p^{w} : ρ^{∗}({n}) ⊂ (P (w), 0) with n ⩾ 0 and w ∈ Σ^{n} be the inclusion. The state 0 is also called the initial state of (P (w), 0) and the state n the final state of (P (w), 0). We have the equality (P (∅), 0) = {0}.

8.6. Definition. Let (X, ∗) be a pointed Cattani-Sassone transition system. A state α of X is reachable if there exists w ∈ Σ^{n} with n ⩾ 0 and a map (P (w), 0) → (X, ∗) taking n to α. A transition (α, u_{1}, …, u_{n}, β) of (X, ∗) is reachable if its initial state α is reachable.

8.7. Definition. A star-shaped (Cattani-Sassone) transition system is a pointed Cattani-Sassone transition system (X, ∗) such that every state of X is reachable. The full subcategory of CSTS_{∗} of star-shaped transition systems is denoted by CSTS_{•}.

Note that star-shaped weak, cubical or regular transition systems are defined exactly as star-shaped Cattani-Sassone transition systems. Without further precision, a star-shaped transition system is supposed to be a star-shaped Cattani-Sassone transition system.

The category CSTS_{•} is a coreflective subcategory of CSTS_{∗}. By [Gaucher, 2015a, Proposition 5.5], the coreflection CSTS_{∗} → CSTS_{•} removes all states which are not reachable, all actions which are not used by a reachable transition, and all transitions which are not reachable.

8.8. Notation. Let (X, ∗) be a star-shaped transition system. Let α be a state of (X, ∗). Let ℓ(α) = min{n ∈ ℕ | ∃w ∈ Σ^{n}, ∃f : (P (w), 0) → (X, ∗), f(n) = α}. The integer ℓ(α) is well-defined since (X, ∗) is star-shaped. We have ℓ(∗) = 0.

8.9. Theorem. Consider a map f → g of Mor(CSTS_{∗}) (i.e. a commutative square) where f is a map of CSTS_{∗} which is one-to-one on states and on actions and where g is a map of CSTS_{•}. Then f → g factors as a composite f → f ⊘ g → g where f ⊘ g is a map of CSTS_{•} which is one-to-one on states and on actions. In particular, f ⊘ g is a cofibration of CSTS_{•}. Finally, the class of maps {f ⊘ g | g ∈ Mor(CSTS_{•})} is a set.

Note that the factorization f → f ⊘ g → g is not unique.

Proof. The proof of this theorem is similar to the proof of [Gaucher, 2015a, Theorem 5.9]. This one is more explicit because we need an explicit calculation of f ⊘ g for the sequel. Consider the commutative diagram of CSTS_{∗}

\xymatrix{(A, ∗) \ar[d]_{f} \ar[r]^{ϕ} & (X, ∗) \ar[d]_{g} \\ (B, ∗) \ar[r]^{ψ} & (Y, ∗)}

with (X, ∗) and (Y, ∗) star-shaped and f one-to-one on states and on actions. Since (X, ∗) is star-shaped, for any state α of (A, ∗), the state ϕ(α) is reachable from ∗ in (X, ∗) using a path of length ℓ(ϕ(α)) labelled with a finite sequence w_{α} of length ℓ(ϕ(α)) of Σ. Thus, the composite map

\xymatrix{ρ^{∗}(\{ℓ(ϕ(α))\}) \ar[r]^{ℓ(ϕ(α))↦α} & (A, ∗) \ar[r]^{ϕ} & (X, ∗)}

factors as a composite

\xymatrix{ρ^{∗}(\{ℓ(ϕ(α))\}) \ar[r]^{p^{wα}} & P (w_{α}) \ar[r] & (X, ∗)} .

We obtain the commutative diagram of CSTS_{∗}

\xymatrix{(M, ∗) = ρ^{∗} ( ⨆_{α∈\underline{S}(A)}\{ℓ(ϕ(α))\}) \ar[d]_{⨆_{α∈\underline{S}(A)} p^{wα}} \ar[r] & (A, ∗) \ar[d]_{ϕ} \\ (N, ∗) = ⨆_{α∈\underline{S}(A)} P (w_{α}) \ar[r] & (X, ∗).}

For any state α of \underline{S}(A), the state g(ϕ(α)) is reachable from ∗ in (Y, ∗) using a path of length ℓ(ϕ(α)) labelled with a finite sequence w_{α} of length ℓ(ϕ(α)) of Σ. Since (Y, ∗) is star-shaped, for any state β of \underline{S}(B)\ \underline{S}(A), the state ψ(β) is reachable from ∗ in (Y, ∗) using a path of length ℓ(ψ(β)) labelled with a finite sequence w_{β} of length ℓ(ψ(β)) of Σ. We obtain the commutative diagram of CSTS_{∗}

\xymatrix{(P, ∗) = ρ^{∗} ( ⨆_{α∈\underline{S}(A)}\{ℓ(ϕ(α))\} ⊔ ⨆_{β∈\underline{S}(B)\ \underline{S}(A)}\{ℓ(ψ(β))\}) \ar[d]|{⨆_{α∈\underline{S}(A)} p^{wα}⊔  ⨆_{β∈\underline{S}(B)\ \underline{S}(A)} p^{w_{β}}} \ar[r] & (B, ∗) \ar[d]_{ψ} \\ (Q, ∗) = ⨆_{α∈\underline{S}(A)} P (w_{α}) ⊔ ⨆_{β∈\underline{S}(B)\ \underline{S}(A)} P (w_{β}) \ar[r] & (Y, ∗).}

We obtain the commutative diagram of CSTS_{∗}:

[figure: (M, ∗); (A, ∗); f; ϕ; X; g; (N, ∗); ⊂; (Â, ∗); ∃!; ∃!; (P, ∗); (B, ∗); ψ; Y; (Q, ∗); (B̂, ∗); ∃!]

The map (Â, ∗) → (B̂, ∗) making the diagram commutative exists by the universal property of the pushout and it is one-to-one on states and on actions. By Proposition 5.16, the underlying map is then a cofibration between Cattani-Sassone transition system. Thus, since (Â, ∗) and (B̂, ∗) are star-shaped by construction, it is a cofibration of CSTS_{•}. We obtain the factorization

\xymatrix{(A, ∗) \ar[rr]^{ϕ} \ar[r]^{⊂} \ar[d]_{f} & Â \ar[d]_{f⊘g} \ar[r] & X \ar[d]_{g} \\ (B, ∗) \ar[rr]_{ψ} \ar[r]^{⊂} & B̂ \ar[r] & Y.}

Finally, the class of maps \{f ⊘ g | g ∈ Mor(CSTS_{•})\} has at most (#Σ)^{(# \underline{S}(B))ℵ_{0}} elements. Thus, it is a set.

8.10. Corollary. The set of generating cofibrations ρ^{∗}(I^{CTS}) of CSTS_{∗} has a solution set of cofibrations with respect to CSTS_{•}, i.e. there exists a set I_{•} of cofibrations of CSTS_{∗} between star-shaped objects such that every map i → g from a generating cofibration i of CSTS_{∗} to a map g of CSTS_{•} factors as a composite i → j → g with j ∈ I_{•}.

Proof. The set I_{•} = {ρ^{∗}(i) ⊘ g | i ∈ ρ^{∗}(I^{CTS}) and g ∈ Mor(CSTS_{•})} is a solution.

8.11. Theorem. There exists a left determined Olschok model structure on the category CSTS_{•} of star-shaped transition systems with respect to the class of maps such that the underlying map is a cofibration of CSTS. A very good cylinder is given by the restriction of the functor Cyl_{∗} : CSTS_{∗} → CSTS_{∗} to the coreflective subcategory CSTS_{•} of CSTS_{∗}.

Proof. By Theorem 8.3, the combinatorial model category CSTS_{∗} is a left determined Olschok model category. We have seen that CSTS_{•} is a coreflective subcategory of CSTS_{∗}. By [Gaucher, 2011, Lemma A.3], cof_{CSTS_{•}}(I_{•}) = cof_{CSTS_{∗}}(ρ^{∗}(I^{CTS})) ∩ Mor(CSTS_{•}) where I_{•} is the set constructed in Corollary 8.10. The proof will be complete by applying [Gaucher, 2015c, Theorem 4.1]. It therefore remains to prove that Cyl_{∗}(CSTS_{•}) ⊂ CSTS_{•}. Let (X, ∗) be a star-shaped transition system. We have the pushout diagram (in CSTS):

[figure: {∗} ⊔ {∗}; {∗}; Cyl_{∗}(X); X ⊔ X; γ_{X}; Cyl^{CSTS}(X); ω^{∗}(Cyl_{∗}(X, ∗)),]

In Cyl_{∗}(X, ∗)), every state (α, ϵ) is reachable from (∗, ϵ) since (X, ∗) is star-shaped by hypothesis. Since (∗, 0) = (∗, 1) = ∗ in ω^{∗}(Cyl_{∗}(X, ∗)), every state of Cyl_{∗}(X, ∗)) is therefore reachable from ∗. Thus, the Cattani-Sassone transition system Cyl_{∗}(X, ∗)) is star-shaped.

(X, ∗)  Cyl_{∗}(X)  Path_{∗}(X)

\underline{I}(X, ∗) = \underline{I}(X) ∪ \{∗\} \underline{E}(X, ∗) = \underline{E}(X)\\{∗\}

\underline{S}(X) \underline{I}(X, ∗) × \{0\} ⊔ \underline{E}(X, ∗) × \{0, 1\}  \underline{S}(X) × \underline{S}(X)
\underline{L}(X)  \underline{L}(X)  \underline{L}(X)
\underline{T}(X)  ((α, ϵ_{0}), u_{1}, …, u_{n}, (β, ϵ_{n+1}))  ((α^{−}, α^{+}), u_{1}, …, u_{n}, (β^{−}, β^{+}))
such that (α, u_{1}, …, u_{n}, β) ∈ \underline{T}(X) such that (α^{±}, u_{1}, …, u_{n}, β^{±}) ∈ \underline{T}(X)

Table 3: Cylinder functor and path functor of CSTS_{∗}

We have Path^{CTS}({∗}) ≅ {(∗, ∗)}. By [Gaucher, 2015c, Lemma 5.2], the cylinder functor Cyl_{∗} : CSTS_{∗} → CSTS_{∗} has a right adjoint Path_{∗} : CSTS_{∗} → CSTS_{∗} defined on objects by mapping (X, ∗) to the composite {∗} →^{≅} Path^{CTS}({∗}) → Path^{CTS}(X) and on maps by mapping the commutative triangle {∗} → f to the composite {∗} →^{≅} Path^{CTS}({∗}) → Path^{CTS}(f). By Theorem 8.11, the restriction of Cyl_{∗} : CSTS_{∗} → CSTS_{∗} to CSTS_{•} gives rise to a very good cylinder Cyl_{•} : CSTS_{•} → CSTS_{•}. A right adjoint is given by the composite functor

Path_{•} : \xymatrix{CSTS_{•} ⊂ CSTS_{∗} \ar[r]^{^{Path^{∗}}} & CSTS_{∗} \ar[r] & CSTS_{•}}

where the right-hand map is the coreflection, i.e. the right adjoint of the inclusion functor CSTS_{•} ⊂ CSTS_{∗}. In particular, this means that the underlying Cattani-Sassone transition system of Path_{•}(X, ∗) is a subobject of the underlying Cattani-Sassone transition system of Path_{∗}(X, ∗), i.e. of Path^{CTS}(X) calculated in Table 2.

Table 3 summarizes the computation of the cylinder functor and of the path functor of CSTS_{∗}.

9. Past-similarity of states

9.1. Definition. Let (X, ∗) be a star-shaped transition system. Two states α and β of X are past-similar (denoted by α ≃_{past} β) if there exists w ∈ Σ^{n} with n ⩾ 0 and two right homotopic maps (P (w), 0) ⇉ (X, ∗) sending n to α and β respectively.

In Figure 3, the states α and β are past-similar because there is a homotopy between any path from ∗ to α and any path from ∗ to β. In Figure 2, the states α and β are not

[figure: •; v; α; ∗; u; u; •; v; β]

Figure 2: α and β are not past-similar

[figure: •; v; v; α; ∗; u; u; •; v; v; β]

Figure 3: α and β are past-similar

past-similar. However, they are past-similar in any fibrant replacement. In fact, the starshaped transition system of Figure 3 is a fibrant replacement of the star-shaped transition system of Figure 2 because: 1) it is fibrant by Theorem 10.12, 2) the image by R_{•}^{⊥} of these two star-shaped transition systems is ∗ →^{u} • →^{v} • →^{w} • (see Section 11).

9.2. Proposition. Let (X, ∗) be a star-shaped transition system. Let α and β be two states of X. We have α ≃_{past} β if and only if (α, β) is a state of Path_{•}(X, ∗).

Proof. If α ≃_{past} β, then there exists w ∈ Σ^{n} for n ⩾ 0 and a map (P (w), 0) → Path_{•}(X, ∗) taking n to (α, β). Thus, the pair (α, β) is a state of Path_{•}(X, ∗). Conversely, if (α, β) is a state of Path_{•}(X, ∗), then it is reachable. Consequently, there exists a map (P (w), 0) → Path_{•}(X, ∗) with n ⩾ 0 and w ∈ Σ^{n} taking n to (α, β).

For all actions u of a Cattani-Sassone transition system X, there exists a transition (α, u, β) of X because X is cubical. Since α ≃_{past} α and β ≃_{past} β, the triple ((α, α), u, (β, β)) is a transition of Path_{•}(X, ∗). Thus, all actions of \underline{L}(X) are used in Path_{•}(X, ∗). Table 4 summarizes the computation of the cylinder functor and of the path functor of CSTS_{•}.

9.3. Proposition. Let f, g : (X, ∗) ⇉ (Y, ∗) be two maps of star-shaped transition systems. The following conditions are equivalent:

1. f and g are left homotopic

2. f and g are right homotopic

3. f and g are homotopic.

In particular, this means that

π_{CSTS_{•}}^{l}((X, ∗), (Y, ∗)) = π_{CSTS_{•}}^{r}((X, ∗), (Y, ∗)) = π_{CSTS_{•}}((X, ∗), (Y, ∗)).

Note that this proposition also holds in CSTS and in CSTS_{∗}.

(X, ∗)  Cyl_{•}(X)  Path_{•}(X)

\underline{I}(X, ∗) = \underline{I}(X) ∪ \{∗\} \underline{E}(X, ∗) = \underline{E}(X)\\{∗\}

\underline{S}(X) \underline{I}(X, ∗) × \{0\} ⊔ \underline{E}(X, ∗) × \{0, 1\}  ≃_{past}⊂ \underline{S}(X) × \underline{S}(X)
\underline{L}(X)  \underline{L}(X)  \underline{L}(X)
\underline{T}(X)  ((α, ϵ_{0}), u_{1}, …, u_{n}, (β, ϵ_{n+1}))  ((α^{−}, α^{+}), u_{1}, …, u_{n}, (β^{−}, β^{+}))
such that (α, u_{1}, …, u_{n}, β) ∈ \underline{T}(X) such that (α^{±}, u_{1}, …, u_{n}, β^{±}) ∈ \underline{T}(X)

Table 4: Cylinder functor and path functor of CSTS_{•}

Proof. We have (3) ⇒ (1) and (3) ⇒ (2) by definition. It suffices to prove the equivalence (1) ⇔ (2). By adjunction, the existence of a left homotopy H_{l} : Cyl_{•}(X, ∗) → (Y, ∗) is equivalent to the existence of a right homotopy H_{r} : (X, ∗) → Path_{•}(Y, ∗). The maps f and g are left homotopic if and only if H_{l}(α, 0) = f(α), H_{l}(α, 1) = g(α) for any state α of X and H(u) = f(u) = g(u) for any action u of X. The maps f and g are right homotopic if and only if H_{r}(α) = (f(α), g(α)) for any state α of X and H_{r}(u) = u for any action u of X.

9.4. Definition. The set of transitions of a star-shaped transition system (X, ∗) is closed under past-similarity if for all n ⩾ 1, for all transitions (α, u_{1}, …, u_{n}, β) of X, and for all states γ and δ of X, if α ≃_{past} γ and β ≃_{past} δ then the tuple (γ, u_{1}, …, u_{n}, δ) is a transition of X.

9.5. Proposition. Let (X, ∗) be a star-shaped transition system. If (X, ∗) is fibrant, then the set of transitions of X is closed under past-similarity.

The converse is proved in Theorem 10.12.

Proof. The proof is by induction on n.

Suppose that n = 1. Let (α, u_{1}, β) be a transition of X. Let γ and δ be two states of X such that α ≃_{past} γ and β ≃_{past} δ. Consider the diagram of CSTS

\xymatrix{\{0_{1}, 1_{1}\} \ar[d]_{⊂} & ω^{∗}(Path_{•}(X, ∗)) \ar[d]_{ω^{∗}(π^{0})} \\ C_{1}[μ(u_{1})] \ar@{-->}[ur]^{ℓ} \ar[r]_{\begin{matrix}0_{1} ↦ α \\ 1_{1} ↦ β \\ (μ(u_{1}), 1) ↦ u_{1} \end{matrix}} & ω^{∗}((X, ∗)).}

By hypothesis, we have α ≃_{past} γ and β ≃_{past} δ. By Proposition 9.2, (α, γ) and (β, δ) are two states of Path_{•}(X, ∗). We obtain the commutative diagram of solid arrows of CSTS

\xymatrix{\{0_{1}, 1_{1}\} \ar[d]_{⊂} \ar[r]^{\begin{matrix}0_{1} ↦ (α, γ) \\ 1_{1} ↦ (β, δ) \end{matrix}} & ω^{∗}(Path_{•}(X, ∗)) \ar[d]_{ω^{∗}(π^{0})} \\ C_{1}[μ(u_{1})] \ar@{-->}[ur]^{ℓ} \ar[r]_{\begin{matrix}0_{1} ↦ α \\ 1_{1} ↦ β \\ (μ(u_{1}), 1) ↦ u_{1} \end{matrix}} & ω^{∗}((X, ∗)).}

The map ρ^{∗}({0_{1}, 1_{1}} ⊂ C_{1}[μ(u_{1})]) ⊘ π^{0} is a cofibration by Theorem 8.9. Since (X, ∗) is fibrant, it is injective with respect to the trivial cofibration

(ρ^{∗}({0_{1}, 1_{1}} ⊂ C_{1}[μ(u_{1})]) ⊘ π^{0}) ⋆ γ^{0}.

Thus, the right vertical map satisfies the RLP with respect to ({0_{1}, 1_{1}} ⊂ C_{1}[μ(u_{1})]) ⊘ π^{0}, and then with respect to the left vertical map {0_{1}, 1_{1}} ⊂ C_{1}[μ(u_{1})]. Since π^{0} is the identity on actions, we obtain that the triple ((α, γ), u_{1}, (β, δ)) is a transition of ω^{∗}(Path_{•}(X, ∗)). By Table 4, we deduce that (γ, u_{1}, δ) is a transition of X.

Suppose the induction hypothesis proved for all p ⩽ n with n ⩾ 1. Choose a transition (α, u_{1}, …, u_{n+1}, β) of X, which gives rise to a map f : C_{n+1}[μ(u_{1}), …, μ(u_{n+1})] → ω^{∗}(X, ∗). Let γ and δ be two states of X such that α ≃_{past} γ and β ≃_{past} δ. By induction hypothesis, there is a commutative diagram of CSTS

\xymatrix{∂C_{n+1}[μ(u_{1}), …, μ(u_{n+1})] \ar[d]_{⊂} \ar[r]^{\begin{matrix}0_{n+1} ↦ (α, γ) \\ f : ζ ∈ \{0, 1\}^{n}\\{0_{n+1}, 1_{n+1}) ↦ (f(ζ), f(ζ)) \\ 1_{n+1} ↦ (β, δ) \\ (μ(u_{i}), i) ↦ u_{i} for 1 ⩽ i ⩽ n + 1 \end{matrix}} & ω^{∗}(Path_{•}(X, ∗)) \ar[d]_{ω^{∗}(π^{0})} \\ C_{n+1}[μ(u_{1}), …, μ(u_{n+1})] \ar@{-->}[ur]^{ℓ} \ar[r]^{f} & ω^{∗}(X, ∗).}

\xymatrix{ & ∗ \ar[dl]_{u} \ar[dr]^{v} \ar[d]_{u} \ar[d]^{v} \\ α & β & γ}

Figure 4: Example of non transitive past-similarity

The map ρ^{∗}(∂C_{n+1}[μ(u_{1}), …, μ(u_{n+1})] ⊂ C_{n+1}[μ(u_{1}), …, μ(u_{n+1})]) ⊘ π^{0} is a cofibration by Theorem 8.9. Thus, (X, ∗) is injective with respect to the trivial cofibration

(ρ^{∗}(∂C_{n+1}[μ(u_{1}), …, μ(u_{n+1})] ⊂ C_{n+1}[μ(u_{1}), …, μ(u_{n+1})]) ⊘ π^{0}) ⋆ γ^{0}.

Hence, the lift ℓ exists. Since π^{0} is the identity on actions, we obtain that the tuple ((α, γ), u_{1}, …, u_{n+1}, (β, δ)) is a transition of ω^{∗}(Path_{•}(X, ∗)). By Table 4, we deduce that (γ, u_{1}, …, u_{n+1}, δ) is a transition of X.

9.6. Proposition. Let (X, ∗) be a star-shaped transition system. Past-similarity is a reflexive and symmetric relation. There exists a star-shaped transition system (X, ∗) such that the binary relation ≃_{past} is not transitive. Let f : (X, ∗) → (Y, ∗) be a map of starshaped transition systems. If α and β are two past-similar states of X, then f(α) and f(β) are two past-similar states of Y.

Proof. Reflexivity and symmetry are obvious. Consider the following example of Figure 4 (with μ(u) ≠ μ(v)). We have α ≃_{past} β and β ≃_{past} γ. But α is not past-similar to γ. If α and β are two past-similar states of X, then there exists a right homotopy H : (P (w), 0) → Path_{•}(X, ∗) for w ∈ Σ^{n} sending n to (α, β). The map f induces a map Path_{•}(X, ∗) → Path_{•}(Y, ∗) by functoriality, and therefore a right homotopy (P (w), 0) → Path_{•}(X, ∗) → Path_{•}(Y, ∗) sending n to (f(α), f(β)). Thus, f(α) and f(β) are pastsimilar.

9.7. Proposition. Let (X, ∗) be a star-shaped transition system such that the set of transitions is closed under past-similarity. Then ≃_{past} is transitive. In particular, if (X, ∗) is fibrant, then ≃_{past} is transitive.

Proof. Let α, β, γ be three states of X with α ≃_{past} β and β ≃_{past} γ. Then there exists a map f : Cyl_{•}(P (w), 0) → (X, ∗) with w ∈ Σ^{n} and n ⩾ 0 such that f(n, 0) = α and f(n, 1) = β. If n = 0, then α = β and therefore α ≃_{past} γ. Let us suppose n ⩾ 1. Define g : Cyl_{•}(P (w), 0) → (X, ∗) on states by g(n, 1) = γ and g = f otherwise, and g = f on actions. The only transitions of Cyl_{•}(P (w), 0) involving the state (n, 1) are ((n−1, 0), (x_{n}, n), (n, 1)) and ((n − 1, 1), (x_{n}, n), (n, 1)) where w = x_{1} … x_{n}. Since f is a well-defined map of star-shaped transition systems, the triples (f(n − 1, 0), f(x_{n}, n), f((n, 1))) = (f(n − 1, 0), f(x_{n}, n), β) and (f(n − 1, 1), f(x_{n}, n), f((n, 1))) = (f(n − 1, 1), f(x_{n}, n), β) are two 1-transitions of X. Since β ≃_{past} γ and since the set of transitions of (X, ∗) is closed under past-similarity, the triples (g(n−1, 0), g(x_{n}, n), g((n, 1))) = (f(n−1, 0), f(x_{n}, n), γ) and (g(n − 1, 1), g(x_{n}, n), g((n, 1))) = (f(n − 1, 1), f(x_{n}, n), γ) are two 1-transitions of (X, ∗). We deduce that the map g : Cyl_{•}(P (w), 0) → (X, ∗) is a well-defined map of star-shaped transition systems. Thus, α ≃_{past} γ. The last sentence is a consequence of Proposition 9.5.

9.8. Theorem. Let (X, ∗) and (Y, ∗) be two objects of CSTS_{•} with (Y, ∗) fibrant. Two maps from (X, ∗) to (Y, ∗) are homotopy equivalent if and only if they coincide on actions and send any state of (X, ∗) to past-similar states of (Y, ∗).

Proof. Let f and g be two homotopy equivalent maps from (X, ∗) to (Y, ∗). There exists a right homotopy H : (X, ∗) → Path_{•}(Y, ∗) from f to g. Let u be an action of X. Since X is cubical, there exists a transition (α, u, β). We deduce that

H(α, u, β) = ((f(α), g(α)), u′, (f(β), g(β)))

with (f(α), u′, f(β)) = f(α, u, β) and (g(α), u′, g(β)) = g(α, u, β). We obtain u′ = f(u) = g(u). Let α be a state of X. Then H(α) = (f(α), g(α)). We deduce that f(α) ≃_{past} g(α) by Proposition 9.2.

Conversely, let f and g be two maps from (X, ∗) to (Y, ∗) which coincide on actions and such that for any state α of X, f(α) and g(α) are past-similar. We have to construct a right homotopy H : (X, ∗) → Path_{•}(Y, ∗) from f to g. The only possible definition is H(α) = (f(α), g(α)) for all states α of (X, ∗) and H(u) = f(u) = g(u) for all actions u of (X, ∗). We have to prove that H yields a well-defined map of transition systems, i.e. that for all transitions (α, u_{1}, …, u_{n}, β) of (X, ∗), the tuple ((f(α), g(α)), H(u_{1}), …, H(u_{n}), (f(β), g(β))) is a transition of Path_{•}(Y, ∗). We are going to prove by induction on n ⩾ 1 that for all states α and β of (X, ∗) and all actions u_{1}, …, u_{p} of X with 1 ⩽ p ⩽ n, the tuple ((f(α), g(α)), H(u_{1}), …, H(u_{p}), (f(β), g(β))) is a transition of Path_{•}(Y, ∗) if (α, u_{1}, …, u_{p}, β) is a transition of (X, ∗).

\underline{The case n = 1}. Consider the commutative diagram of solid arrows of CSTS

\xymatrix{\{0_{1}, 1_{1}\} \ar[d]_{⊂} \ar[r]^{\begin{matrix}0_{1} ↦ (f(α), g(α)) \\ 1_{1} ↦ (f(β), g(β)) \end{matrix}} & ω^{∗}(Path_{•}(Y, ∗)) \ar[d]_{ω^{∗}(π^{0})} \\ C_{1}[μ(u_{1})] \ar@{-->}[ur]^{ℓ} \ar[r]_{\begin{matrix}0_{1} ↦ f(α) \\ 1_{1} ↦ g(α) \\ (μ(u_{1}), 1) ↦ f(u_{1}) \end{matrix}} & ω^{∗}((Y, ∗)).}

Since (Y, ∗) is fibrant, the canonical map (Y, ∗) → 1 satisfies the RLP with respect to the trivial cofibration (ρ^{∗}(∂C_{1}[μ(u_{1})] ⊂ C_{1}[μ(u_{1})]) ⊘ π^{0}) ⋆ γ^{0}. By adjunction, this implies that the lift ℓ in the diagram above exists. Thus, we have proved that the triple

ℓ(0_{1}, μ(u_{1}), 1_{1})) = ((f(α), g(α)), f(u_{1}), (f(β), g(β)))

is a transition of Path_{•}(Y, ∗).

\underline{From n to n + 1 with n ⩾ 1}. By induction hypothesis, we have the commutative diagram of solid arrows of CSTS:

\xymatrix{∂C_{n+1}[μ(u_{1}), …, μ(u_{n+1})] \ar[d]_{⊂} \ar[r]^{\begin{matrix}0_{n+1} ↦ (f(α), g(α)) \\ 1_{n+1} ↦ (f(β), g(β)) \\ (μ(u_{i}), i) ↦ f(u_{i}) for 1 ⩽ i ⩽ n + 1 \end{matrix}} & ω^{∗}(Path_{•}(Y, ∗)) \ar[d]_{ω^{∗}(π^{0})} \\ C_{n+1}[μ(u_{1}), …, μ(u_{n+1})] \ar@{-->}[ur]^{ℓ} \ar[r]_{\begin{matrix}0_{n+1} ↦ f(α) \\ 1_{n+1} ↦ g(α) \\ (μ(u_{i}), i) ↦ f(u_{i}) for 1 ⩽ i ⩽ n + 1 \end{matrix}} & ω^{∗}(Y, ∗).}

Since (Y, ∗) is fibrant, the canonical map (Y, ∗) → 1 satisfies the RLP with respect to the trivial cofibration

(ρ^{∗} (∂C_{n+1}[μ(u_{1}), …, μ(u_{n+1})] ⊂ C_{n+1}[μ(u_{1}), …, μ(u_{n+1})]) ⊘ π^{0}) ⋆ γ^{0}.

By adjunction, this implies that the lift ℓ in the diagram above exists. Thus, we have proved that the triple

ℓ(0_{n+1}, μ(u_{1}), …, μ(u_{n+1}), 1_{n+1}) = ((f(α), g(α)), f(u_{1}), …, f(u_{n+1}), (f(β), g(β)))

is a transition of Path_{•}(Y, ∗).

9.9. Corollary. Every weak equivalence between two fibrant star-shaped transition systems is bijective on actions.

10. Fibrant star-shaped transition systems

10.1. Lemma. Consider a commutative square of CSTS_{•}

\xymatrix{(A, ∗) \ar[r] \ar[d] & (C, ∗) \ar[d] \\ (B, ∗) \ar[r] & (D, ∗).}

Then the set map \underline{S}(B, ∗) ⊔_{\underline{S}(A,∗)} \underline{S}(C, ∗) → \underline{S}(D, ∗) factors as a composite

\underline{S}(B, ∗) ⊔_{\underline{S}(A,∗)} \underline{S}(C, ∗) ↠ \underline{S}((B, ∗) ⊔_{(A,∗)} (C, ∗)) ⟶ \underline{S}(D, ∗)

where the left-hand map is onto and the set map \underline{L}(B, ∗) ⊔_{\underline{L}(A,∗)} \underline{L}(C, ∗) → \underline{L}(D, ∗) factors as a composite

\underline{L}(B, ∗) ⊔_{\underline{L}(A,∗)} \underline{L}(C, ∗) ↠ \underline{L}((B, ∗) ⊔_{(A,∗)} (C, ∗)) ⟶ \underline{L}(D, ∗)

where the left-hand map is onto.

Proof. A pushout (B, ∗) ⊔_{(A,∗)} (C, ∗) in CSTS_{•} can be calculated in CSTS_{∗} since the category CSTS_{•} is a coreflective subcategory of CSTS_{∗}. Since a pushout is a connected colimit, we have the isomorphism

(B, ∗) ⊔_{(A,∗)} (C, ∗) ≅ (B ⊔_{A} C, ∗).

A pushout B ⊔_{A} C in CSTS is calculated by taking the pushout B ⊔_{A}^{CTS} C in CTS, and then by applying the reflection CSA_{1} CSA_{2} : CTS → CSTS which identifies states and actions to force CSA1 and CSA2 to hold. We obtain the isomorphism of CSTS_{•}:

(B ⊔_{A} C, ∗) ≅ (CSA_{1} CSA_{2}(B ⊔_{A}^{CTS} C), ∗).

By adjunction, the map of cubical transition systems

B ⊔_{A}^{CTS} C → D

factors uniquely as a composite

B ⊔_{A}^{CTS} C ⟶ B ⊔_{A} C ⟶ D.

By Lemma 3.2, we have the bijections of sets

\underline{S}(B ⊔_{A}^{CTS} C) ≅ \underline{S}(B) ⊔_{\underline{S}(A)} \underline{S}(C) and \underline{L}(B ⊔_{A}^{CTS} C) ≅ \underline{L}(B) ⊔_{\underline{L}(A)} \underline{L}(C).

We obtain the composite set map

\underline{S}(B) ⊔_{\underline{S}(A)} \underline{S}(C) ↠ \underline{S}((B, ∗) ⊔_{(A,∗)} (C, ∗)) ⟶ \underline{S}(D)

where the left-hand map is onto and the composite set map

\underline{L}(B) ⊔_{\underline{L}(A)} \underline{L}(C) ↠ \underline{L}((B, ∗) ⊔_{(A,∗)} (C, ∗)) ⟶ \underline{L}(D)

where the left-hand map is onto.

10.2. Notation. Let

1. Λ_{0}(Z) = (Z ⋆ γ^{0}) ∪ (Z ⋆ γ^{1})

2. Λ_{n+1}(Z) = Λ_{n}(Z) ⋆ γ for n ⩾ 0

3. Λ(Z) := ⋃_{n⩾0} Λ_{n}(Z)

where γ^{0}, γ^{1} : Id ⇒ Cyl_{•} are the natural transformations associated with the cylinder Cyl_{•} : CSTS_{•} → CSTS_{•} and γ = γ^{0} ⊔ γ^{1} (see Table 4 page 1140) and where Z is a set of maps of CSTS_{•}.

10.3. Proposition. Every map of Λ(I_{•}) is bijective on actions.

Proof. Let f : (A, ∗) → (B, ∗) be a map of star-shaped transition systems. Using Lemma 10.1, the map f ⋆ γ^{ϵ} gives rise to the composite set map

\underline{L}(A, ∗) ⊔_{\underline{L}(A,∗)} \underline{L}(B, ∗) ↠ \underline{L} (Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗)) ⟶ \underline{L}(B, ∗)

which is bijective. Thus, the left-hand map is injective and then bijective. This implies that the right-hand map is bijective and that f ⋆ γ^{ϵ} is bijective on actions. Suppose now that f is bijective on actions. By Lemma 10.1, the map f ⋆ γ gives rise to the composite set map

\underline{L}(Cyl_{•}(A, ∗)) ⊔_{\underline{L}((A,∗)⊔(A,∗))} \underline{L}((B, ∗) ⊔ (B, ∗)) ↠ \underline{L} (Cyl_{•}(A, ∗) ⊔_{(A,∗)⊔(A,∗)} ((B, ∗) ⊔ (B, ∗))) ⟶ \underline{L}(Cyl_{•}(B, ∗))

which is bijective. Thus, the left-hand map is injective and then bijective. This implies that the right-hand map is bijective and that f ⋆ γ is bijective on actions.

10.4. Proposition. Let (X, ∗) be a star-shaped transition system. Then we have the equalities \underline{I}(Cyl_{•}(X, ∗)) = \underline{I}(X, ∗) × \{0\} and \underline{E}(Cyl_{•}(X, ∗)) = \underline{E}(X, ∗) × \{0, 1\}.

Proof. The natural map γ_{X}^{0} : (X, ∗) → Cyl_{•}(X, ∗) induces a one-to-one set map

\underline{S}(γ_{X}^{0}) : \underline{I}(X, ∗) ⊔ \underline{E}(X, ∗) ⟶ \underline{I}(X, ∗) × \{0\} ⊔ \underline{E}(X, ∗) × \{0, 1\}.

We deduce the set inclusion

\underline{I}(γ_{X}^{0}) : \underline{I}(X, ∗) ≅ \underline{I}(X, ∗) × \{0\} ⊂ \underline{I}(Cyl_{•}(X, ∗)).

Let (α, ϵ) ∈ \underline{I}(Cyl_{•}(X, ∗)). By Proposition 5.6, there exists a 2-transition

((μ_{0}, ϵ_{0}), u_{1}, u_{2}, (μ_{1}, ϵ_{1}))

of Cyl_{•}(X, ∗) such that the tuples ((μ_{0}, ϵ_{0}), u_{1}, (α, ϵ)) and ((α, ϵ), u_{2}, (μ_{1}, ϵ_{1})) are two transitions of Cyl_{•}(X, ∗). Using Table 4, we deduce that the tuples (μ_{0}, u_{1}, u_{2}, μ_{1}), (μ_{0}, u_{1}, α) and (α, u_{2}, μ_{1}) are transitions of (X, ∗). This implies that α is an internal state of (X, ∗) and that ϵ = 0. We deduce the set inclusion

\underline{I}(Cyl_{•}(X, ∗)) ⊂ \underline{I}(X, ∗) × \{0\}.

We obtain the equality

\underline{I}(Cyl_{•}(X, ∗)) = \underline{I}(X, ∗) × \{0\}

and, by taking the complement, the equality

\underline{E}(Cyl_{•}(X, ∗)) = \underline{E}(X, ∗) × \{0, 1\}.

10.5. Definition. A map f : (A, ∗) → (B, ∗) of pointed transition systems is proper if the set map \underline{I}(f) : \underline{I}(A, ∗) → \underline{I}(B, ∗) is bijective and if f induces a one-to-one set map f(\underline{E}(A, ∗)) ⊂ \underline{E}(B, ∗) on external states. In particular, a proper map is one-to-one on states. A map f : (A, ∗) → (B, ∗) of pointed transition systems is strongly proper if it is proper and bijective on states (which means that not only it is bijective on internal states, but also on external states).

10.6. Proposition. Let f : (A, ∗) → (B, ∗) be a (strongly resp.) proper map of pointed transition systems. Then for any g ∈ Mor(CSTS_{•}), the map f ⊘ g is (strongly resp.) proper.

Proof. Let f ⊘ g : (Â, ∗) → (B̂, ∗). The star-shaped transition system (Â, ∗) is obtained from (A, ∗) by doing for each state α of (A, ∗) different from the base state one of the following operations (cf. the proof of Theorem 8.9): 1) either identifying α with ∗, 2) or attaching a finite sequence of 1-transitions with initial state ∗ and final state α. When α is internal in (A, ∗), it remains internal in (Â, ∗). When it is external in (A, ∗), it becomes internal (case 1) and actually equal to ∗, or it remains external (case 2). In case 2, all intermediate states of the finite sequence of 1-transitions are external. The star-shaped transition system (B̂, ∗) is obtained from (B, ∗) by doing for each state α of (B, ∗) different from the base state one of the following operations (cf. the proof of Theorem 8.9): 1) nothing for a state of f(\underline{S}(A)), 2) one of the two operations above on the states of \underline{S}(B)\f(\underline{S}(A)). Thus, f ⊘ g is proper.

10.7. Notation. Let Σ^{+} = ⋃_{n⩾1} Σ^{n} denote the set of nonempty words over Σ.

10.8. Corollary. Every map of I_{•} is proper. Every map of I_{•}\{(∅ → (P (w), 0)) | w ∈ Σ^{+}} is strongly proper (where ∅ = ({∗}, ∗) is the initial object of CSTS_{•}).

Proof. For any set S, we have \underline{I}(S) = ∅, \underline{E}(S) = S. For any n-cube C_{n}[x_{1}, …, x_{n}] with n ⩾ 1 and x_{1}, …, x_{n} ∈ Σ, we have \underline{E}(C_{n}[x_{1}, …, x_{n}]) = \{0_{n}, 1_{n}\} and \underline{I}(C_{n}[x_{1}, …, x_{n}]) = {0, 1}^{n}\{0_{n}, 1_{n}}. Thus, every map of ρ^{∗}(I^{CTS}) is proper and every map of ρ^{∗}(I^{CTS}\{∅ ⊂ {0}}) is strongly proper. The proof of the first statement is complete using Proposition 10.6. We have

{ρ^{∗}(∅ ⊂ {0}) ⊘ g | g ∈ Mor(CSTS_{•})} = {(∅ → (P (w), 0)) | w ∈ Σ^{+}}.

Then the proof of the last part is complete using Proposition 10.6.

10.9. Proposition. Let f : (A, ∗) → (B, ∗) be a (strongly resp.) proper map of starshaped transition systems. Then the map f ⋆ γ^{ϵ} for ϵ = 0, 1 is (strongly resp.) proper.

Proof. We write the proof for ϵ = 0. We have

\underline{S}(Cyl_{•}(A, ∗)) ⊔_{\underline{S}(A,∗)} \underline{S}(B, ∗) ≅ (\underline{I}(A, ∗) × \{0\} ⊔ \underline{E}(A, ∗) × \{0, 1\}) ⊔_{\underline{I}(A,∗)×\{0\}⊔\underline{E}(A,∗)×\{0\}} (\underline{I}(B, ∗) × \{0\} ⊔ \underline{E}(B, ∗) × \{0\}) ≅ \underline{I}(B, ∗) × \{0\} ⊔ \underline{E}(B, ∗) × \{0\} ⊔ \underline{E}(A, ∗) × \{1\}.

The map f ⋆ γ^{0} gives rise by Lemma 10.1 to the composite set map

\underline{I}(B, ∗) × \{0\} ⊔ \underline{E}(B, ∗) × \{0\} ⊔ \underline{E}(A, ∗) × \{1\} ↠ \underline{S} (Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗)) ⟶ \underline{I}(B, ∗) × \{0\} ⊔ \underline{E}(B, ∗) × \{0, 1\}

which is one-to-one. Thus, the left-hand map is one-to-one, and then bijective. We deduce the bijection of sets

\underline{S} (Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗)) ≅ \underline{I}(B, ∗) × \{0\} ⊔ \underline{E}(B, ∗) × \{0\} ⊔ \underline{E}(A, ∗) × \{1\}

and therefore, that f ⋆ γ^{0} is one-to-one on states. The map of star-shaped transition systems

ι_{2} : (B, ∗) → Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗)

induces on internal states the set map

\underline{I}(ι_{2}) : \underline{I}(B, ∗) ⟶ \underline{I}(Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗)).

The latter yields the inclusion of sets

\underline{I}(B, ∗) × \{0\} ⊂ \underline{I}(Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗)).

The map f ⋆ γ^{0} : Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗) → Cyl_{•}(B, ∗) induces a set inclusion between the sets of internal states

\underline{I} (Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗)) ⊂ \underline{I}(Cyl_{•}(B, ∗)).

By Proposition 10.4, we have \underline{I}(Cyl_{•}(B, ∗)) = \underline{I}(B, ∗) × \{0\}. We obtain the set inclusion

\underline{I} (Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗)) ⊂ \underline{I}(B, ∗) × \{0\}.

Thus, we obtain the equality

\underline{I}(Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗)) = \underline{I}(B, ∗) × \{0\}

and, by taking the complement, the equality

\underline{E}(Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗)) = \underline{E}(A, ∗) × \{1\} ⊔ \underline{E}(B, ∗) × \{0\}.

The proof is complete thanks to Proposition 10.4.

10.10. Proposition. Let f : (A, ∗) → (B, ∗) be a proper map. The map f ⋆γ is strongly proper.

Proof. We have

\underline{S}(Cyl_{•}(A, ∗)) ⊔_{\underline{S}((A,∗)⊔(A,∗))} \underline{S}((B, ∗) ⊔ (B, ∗))
≅ (\underline{I}(A, ∗) × \{0\} ⊔ \underline{E}(A, ∗) × \{0, 1\})
⊔_{\underline{I}(A,∗)×\{0,1\}⊔\underline{E}(A,∗)×\{0,1\}} (\underline{I}(B, ∗) × \{0, 1\} ⊔ \underline{E}(B, ∗) × \{0, 1\})
≅ \underline{I}(A, ∗) × \{0\} ⊔ \underline{E}(B, ∗) × \{0, 1\}.

Thus the map f ⋆ γ gives rise by Lemma 10.1 to the composite set map

\underline{I}(A, ∗) × \{0\} ⊔ \underline{E}(B, ∗) × \{0, 1\} ↠ \underline{S}(Cyl_{•}(A, ∗) ⊔_{(A,∗)⊔(A,∗)} ((B, ∗) ⊔ (B, ∗))) ⟶ \underline{I}(B, ∗) × \{0\} ⊔ \underline{E}(B, ∗) × \{0, 1\}.

Since this composite is bijective, the left-hand map is injective and then bijective. We obtain

\underline{S}(Cyl_{•}(A, ∗) ⊔_{(A,∗)⊔(A,∗)} ((B, ∗) ⊔ (B, ∗))) = \underline{I}(A, ∗) × \{0\} ⊔ \underline{E}(B, ∗) × \{0, 1\}

and f ⋆ γ is bijective on states. The states of \underline{E}(B, ∗) × \{0, 1\} are external in Cyl_{•}(B, ∗) by Proposition 10.4. Thus, the states \underline{E}(B, ∗) × \{0, 1\} cannot be internal states of Cyl_{•}(A, ∗) ⊔_{(A,∗)⊔(A,∗)} ((B, ∗) ⊔ (B, ∗)). We have proved the inclusion

\underline{I}(Cyl_{•}(A, ∗) ⊔_{(A,∗)⊔(A,∗)} ((B, ∗) ⊔ (B, ∗))) ⊂ \underline{I}(B, ∗) × \{0\}.

The map Cyl_{•}(A, ∗) → Cyl_{•}(A, ∗) ⊔_{(A,∗)⊔(A,∗)} ((B, ∗) ⊔ (B, ∗)) induces a set map

\underline{I}(Cyl_{•}(A, ∗)) → \underline{I}(Cyl_{•}(A, ∗) ⊔_{(A,∗)⊔(A,∗)} ((B, ∗) ⊔ (B, ∗))).

By Proposition 10.4, we have \underline{I}(Cyl_{•}(A, ∗)) = \underline{I}(A, ∗) × \{0\} ≅ \underline{I}(B, ∗) × \{0\}. We deduce the inclusion of sets

\underline{I}(B, ∗) × \{0\} ⊂ \underline{I}(Cyl_{•}(A, ∗) ⊔_{(A,∗)⊔(A,∗)} ((B, ∗) ⊔ (B, ∗))).

The proof is complete thanks to Proposition 10.4.

10.11. Corollary. Every map of Λ(I_{•})\Λ_{0}({∅ → (P (w), 0) | w ∈ Σ^{+}}) is strongly proper, and in particular, bijective on states.

Proof. Table 5 summarizes the situation.

I^{CTS}  ∅ ⊂ {0}  I^{CTS}\{∅ ⊂ {0}}
I_{•} = {ρ^{∗}(f) ⊘ g | f ∈ I^{CTS} {∅ → (P (w), 0) | w ∈ Σ^{+}} I_{•}\{∅ → (P (w), 0) | w ∈ Σ^{+}}
and g ∈ Mor(CSTS_{•})}  proper (10.8)  strongly proper (10.8)
Λ_{0}  proper (10.9)  strongly proper (10.9)
Λ_{n} with n ⩾ 1  strongly proper (10.10)  strongly proper(10.10)

Table 5: Properness of the maps of Λ(I_{•})

10.12. Theorem. Let (X, ∗) be a star-shaped transition system. Then (X, ∗) is fibrant if and only if its set of transitions is closed under past-similarity.

Proof. The “only if” part is Proposition 9.5. Let (X, ∗) be a star-shaped transition system such that the set of transition is closed under past-similarity. We have to prove that (X, ∗) is injective with respect to any map of Λ(I_{•}).

Let us prove first that (X, ∗) is injective with respect to the maps of Λ_{0}({∅ → (P (w), 0) | w ∈ Σ^{+}}). Let i : ∅ → (P (w), 0) with w ∈ Σ^{+}. By symmetry, it suffices to prove the injectivity with respect to i ⋆ γ^{0}. Consider the diagram of solid arrows of

CSTS_{•}
\xymatrix{(P (w), 0) \ar[r]^{ϕ} \ar[d]_{i⋆γ^{0}} & (X, ∗) \\ Cyl_{•}(P (w), 0) \ar@{-->}[ur]^{ℓ}}

The map i ⋆ γ^{0} : (P (w), 0) → Cyl_{•}(P (w), 0) has the retraction σ : Cyl_{•}(P (w), 0) → (P (w), 0). Thus, ℓ = ϕσ is a solution. So far, we have not used the fact that the set of transitions of (X, ∗) is closed under past-similarity.

Let us prove now that (X, ∗) is injective with respect to any map of Λ_{0}(I_{•}\{∅ ⊂ (P (w), 0) | w ∈ Σ^{+}}). By symmetry, it suffices to prove the injectivity with respect to

{i ⋆ γ^{0} | i ∈ I_{•}\{∅ ⊂ (P (w), 0) | w ∈ Σ^{+}}}.

The map i ⋆ γ^{0} is of the form Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗) → Cyl_{•}(B, ∗) with i : (A, ∗) → (B, ∗) ∈ I_{•}\{∅ ⊂ (P (w), 0) | w ∈ Σ^{+}} where the map from (A, ∗) to Cyl_{•}(A, ∗) is γ_{(A,∗)}^{0}.

Consider the diagram of solid arrows of CSTS_{•}

\xymatrix{Cyl_{•}(A, ∗) ⊔_{(A,∗)} (B, ∗) \ar[r] \ar[d]_{i⋆γ^{0}} & (X, ∗) \\ Cyl_{•}(B, ∗). \ar@{-->}[ur]^{ℓ}}

By adjunction, the lift ℓ in the diagram above exists if and only the lift ℓ′ in the commutative diagram of solid arrows of CSTS_{•}

\xymatrix{(A, ∗) \ar[r]^{ϕ′} \ar[d]_{i} & Path_{•}(X, ∗) \ar[d]_{π^{0}} \\ (B, ∗) \ar[r]^{ψ′} \ar@{-->}[ur]^{ℓ′} & (X, ∗)}

exists. By Table 5, the map i is bijective on states. By Table 4, the map π^{0} is bijective on actions. There is therefore one and exactly one way to define ℓ′ on states and on actions. Let (α, u_{1}, …, u_{n}, β) be a transition of B. Then the tuple (ψ′(α), ψ′(u_{1}), …, ψ′(u_{n}), ψ′(β)) is a transition of (X, ∗). By Table 4, we obtain the equality of tuples

ℓ′(α, u_{1}, …, u_{n}, β) = ((ψ′(α), α′), ψ′(u_{1}), …, ψ′(u_{n}), (ψ′(β), β′))

with α′ ≃_{past} ψ′(α) and β′ ≃_{past} ψ′(β). Since the set of transitions of (X, ∗) is closed under past-similarity, the three tuples

(ψ′(α), ψ′(u_{1}), …, ψ′(u_{n}), β′)), (α′, ψ′(u_{1}), …, ψ′(u_{n}), ψ′(β)), (α′, ψ′(u_{1}), …, ψ′(u_{n}), β′)

are transitions of X. Thus, by Table 4, the tuple ℓ′(α, u_{1}, …, u_{n}, β) is a transition of Path_{•}(X, ∗) and ℓ′ is a well-defined map of CSTS_{•}.

Let us prove now that (X, ∗) is injective with respect to the maps f ⋆γ of Λ_{1}(I_{•}\{(∅ → (P (w), 0)) | w ∈ Σ^{+}}) and of Λ_{n}(I_{•}) for n ⩾ 2. Then we have

f ∈ Λ_{0}(I_{•}\{(∅ → (P (w), 0)) | w ∈ Σ^{+}}) ∪ Λ_{n−1}(I_{•}).

By Table 5, the map f : (A, ∗) → (B, ∗) is bijective on states. And by Proposition 10.3, it is bijective on actions. By adjunction, we then have to prove that for any commutative diagram of solid arrows of CSTS_{•}

\xymatrix{(A, ∗) \ar[r]^{ϕ} \ar[d]_{f} & Path_{•}(X, ∗) \ar[d]_{π} \\ (B, ∗) \ar@{-->}[ur]^{ℓ} \ar[r]^{ψ=(ψ_{1},ψ_{2})} & (X, ∗) × (X, ∗),}

the lift ℓ exists. Since f is bijective on actions, we have ψ_{1}(u) = ψ_{2}(u) for any action u of (B, ∗) because π is the diagonal on actions. Since f is bijective on states, ψ(α) is a state of Path_{•}(X, ∗) for any state α of (B, ∗). Let ℓ(α) = ψ(α) for a state α of (B, ∗) and ℓ(u) = ψ_{1}(u) = ψ_{2}(u). We have to prove that ℓ takes a transition of (B, ∗) to a transition of Path_{•}(X, ∗). Let (α, u_{1}, …, u_{n}, β) be a transition of (B, ∗). Since the map ψ_{1} : (B, ∗) → (X, ∗) × (X, ∗) → (X, ∗) is a map of star-shaped transition systems, the tuple (ψ_{1}(α), ψ_{1}(u_{1}), …, ψ_{1}(u_{n}), ψ_{1}(β)) is a transition of X. Since the map ψ_{2} : (B, ∗) → (X, ∗) × (X, ∗) → (X, ∗) is a map of star-shaped transition systems, the tuple (ψ_{2}(α), ψ_{2}(u_{1}), …, ψ_{2}(u_{n}), ψ_{2}(β)) is a transition of X as well. Since ψ(α) is a state of Path_{•}(X, ∗), we have ψ_{1}(α) ≃_{past} ψ_{2}(α) by Table 4. For the same reason, we have ψ_{1}(β) ≃_{past} ψ_{2}(β). Since the set of transitions of (X, ∗) is closed under past-similarity, we deduce that the tuples (ψ_{2}(α), ψ_{1}(u_{1}), …, ψ_{1}(u_{n}), ψ_{1}(β)) and (ψ_{1}(α), ψ_{1}(u_{1}), …, ψ_{1}(u_{n}), ψ_{2}(β)) are transitions of (X, ∗). Therefore, the tuple

(ℓ(α), ℓ(u_{1}), …, ℓ(u_{n}), ℓ(β)) = (ψ(α), ψ_{1}(u_{1}), …, ψ_{1}(u_{n}), ψ(β))

is a transition of Path_{•}(X, ∗) by Table 4.

It remains to prove that (X, ∗) is injective with respect to the maps of Λ_{1}({(∅ → (P (w), 0)) | w ∈ Σ^{+}})) to complete the proof. A map of Λ_{1}({(∅ → (P (w), 0)) | w ∈ Σ^{+}}) is of the form f ⋆ γ where f : (P (w), 0) → Cyl_{•}(P (w), 0) is the map f = γ_{(P (w),0)}^{ϵ} for w ∈ Σ^{n} and n ⩾ 1. Assume that ϵ = 0 without loss of generality. By adjunction, we have then to prove that for any commutative diagram of solid arrows of CSTS_{•}

\xymatrix{(P (w), 0) \ar[r]^{ϕ} \ar[d]_{f=γ_{(P (w),0)}^{0}} & Path_{•}(X, ∗) \ar[d]_{π} \\ Cyl_{•}(P (w), 0) \ar@{-->}[ur]^{ℓ} \ar[r]^{ψ=(ψ_{1},ψ_{2})} & (X, ∗) × (X, ∗),}

the lift ℓ exists. Since f is bijective on actions, and since π is the diagonal map on actions, we have ψ_{1}(u) = ψ_{2}(u) for any action u of (B, ∗). The only possible definition on actions is ℓ(u) = ψ_{1}(u) = ψ_{2}(u). Let ℓ(α) = ψ(α). For any 0 ⩽ j ⩽ n, we have (j, 0) ≃_{past} (j, 1) in Cyl_{•}(P (w), 0). Consequently, we have ψ_{1}(j, 0) ≃_{past} ψ_{1}(j, 1) and ψ_{2}(j, 0) ≃_{past} ψ_{2}(j, 1) in (X, ∗). Since the diagram is commutative, the pair (ψ_{1}(j, 0), ψ_{2}(j, 0)) is a state of Path_{•}(X, ∗). By Table 4, we deduce that ψ_{1}(j, 0) ≃_{past} ψ_{2}(j, 0). By Proposition 9.7, past-similarity is transitive on (X, ∗). We deduce that ψ_{1}(j, 1) ≃_{past} ψ_{2}(j, 1). We have proved that for any state α of Cyl_{•}(P (w), 0), ψ(α) is a state of Path_{•}(X, ∗) (remember that π is one-to-one on states). It remains to prove that ℓ takes a transition of Cyl_{•}(P (w), 0) to a transition of Path_{•}(X, ∗) to complete the proof. Let (α, u_{1}, …, u_{n}, β) be a transition of Cyl_{•}(P (w), 0). Then both (ψ_{1}(α), ψ_{1}(u_{1}), …, ψ_{1}(u_{n}), ψ_{1}(β)) and (ψ_{2}(α), ψ_{2}(u_{2}), …, ψ_{2}(u_{n}), ψ_{2}(β)) are transitions of X. Since the set of transitions of (X, ∗) is closed under past-similarity, the tuples (ψ_{1}(α), ψ_{1}(u_{1}), …, ψ_{1}(u_{n}), ψ_{2}(β)) and (ψ_{1}(α), ψ_{2}(u_{2}), …, ψ_{2}(u_{n}), ψ_{2}(β)) are also transitions of X. The proof is complete using Table 4.

11. Characterization in the star-shaped case

11.1. Definition. A star-shaped transition system is reduced when two states are pastsimilar if and only if they are equal.

All reduced star-shaped transition systems are fibrant by Theorem 10.12.

11.2. Proposition. The full subcategory \overline{CSTS_{•}} of reduced star-shaped transition systems is a small-orthogonality class of CSTS_{•}.

Proof. Let w = x_{1} … x_{n} ∈ Σ^{n} with n ⩾ 1. Let (C(w), ∗) be the ω-final lift of the map

ω(Cyl_{•}(P (w), 0)) → (\underline{S}(Cyl_{•}(P (w), 0))/((n, 1) = (n, 2)), \{(x_{1}, 1), …, (x_{n}, n)\}).

It can be depicted as follows:

\xymatrix{ & (1, 0) \ar[r]^{(x_{2},2)} \ar[ddr]_{(x_{2},2)} & (2, 0) \ar[r]^{(x_{3},3)} \ar[ddr]_{(x_{3},3)} & . . . . . . \ar[dr]_{(x_{n},n)} \\ ∗ = (0, 0) = (0, 1) \ar@{-->}[ur]^{(x_{1},1)} \ar[dr]_{(x_{1},1)} &  &  &  & (n, 0) = (n, 1) \\  & (1, 1) \ar[r]^{(x_{2},2)} \ar[uur]^{(x_{2},2)} & (2, 1) \ar[r]^{(x_{3},3)} \ar[uur]^{(x_{3},3)} & _{. . . . . .} \ar[ur]^{(x_{n},n)}}

A star-shaped transition system is reduced if and only if it is injective with respect to the maps Cyl_{•}(P (w), 0) → (C(w), ∗) with w ∈ Σ^{+}. Since these maps are onto on states and on actions, they are epic. Thus, injectivity is equivalent to orthogonality in this case.

Let \underline{R} = \{Cyl_{•}(P (w), 0) → (C(w), ∗) | w ∈ Σ^{+}\}. For any star-shaped transition system (X, ∗), the canonical map (X, ∗) → 1 factors as a composite (X, ∗) → R_{•}^{⊥}(X, ∗) → 1 with the left-hand map belonging to cell_{CSTS_{•}}(\underline{R}) and the right-hand map belonging to inj_{CSTS_{•}}(\underline{R}). By Theorem 4.5 and Corollary 4.6, every map of cell_{CSTS_{•}}(\underline{R}) is onto on states, on actions and on transitions. We deduce that every map of cell_{CSTS_{•}}(\underline{R}) is epic in CSTS_{•}. Thus, by [Gaucher, 2015a, Proposition A.1], this factorization is unique up to isomorphism. And for the same reason as for CSA1, this construction provides the left adjoint to the inclusion functor \overline{CSTS_{•}} ⊂ CSTS_{•}. By [Adámek and Rosický, 1994, Theorem 1.39], the category \overline{CSTS_{•}} is locally presentable.

11.3. Notation. Let us denote by Ψ_{(X,∗)} : (X, ∗) → R_{•}^{⊥}(X, ∗) the unit map.

11.4. Notation. Let X be a weak transition system. Let u and v be two actions of X. Denote by u ≃_{CSA_{1}} v if μ(u) = μ(v) and if there exist two states α and β of X such that the triples (α, u, β) and (α, v, β) are transitions of X.

11.5. Proposition. Let (X, ∗) be a star-shaped cubical transition system. Let \underline{r}(X) be the ω-final lift of the map ω(X) ⟶ (\underline{S}(X)/≃_{past}, \underline{L}(X)/≃_{CSA_{1}}) of Set^{\{s\}∪Σ}. Let ∗ be the image by X → \underline{r}(X) of ∗ ∈ X. Then the pointed weak transition system (\underline{r}(X), ∗) is a star-shaped cubical transition system.

Proof. The weak transition system X is cubical by hypothesis. Since the set map \underline{L}(X) → \underline{L}(X)/≃_{CSA_{1}} is onto, the weak transition system \underline{r}(X) is cubical by Theorem 2.4. The map X → \underline{r}(X) is onto on states. Thus, every state of \underline{r}(X) is reachable.

11.6. Proposition. Let (X, ∗) be a star-shaped transition system. Let X_{0} = X. Suppose the weak transition system X_{ξ} constructed for an ordinal ξ ⩾ 0. Let X_{ξ+1} = \underline{r}(X_{ξ}). For a limit ordinal ξ, let X_{ξ} = \underrightarrow{lim}_{β<ξ}^{WTS} X_{β}, the colimit being taken in WTS. Then

1. For all ordinals ξ, the weak transition system X_{ξ} is cubical and the pointed cubical transition system (X_{ξ}, ∗) is star-shaped.

2. There exists an ordinal η such that X_{ξ} = X_{η} for all ξ ⩾ η.

3. There is the isomorphism R_{•}^{⊥}(X, ∗) = (X_{η}, ∗).

Proof. The proof is in five steps.

1) For a limit ordinal ξ, the weak transition system \underrightarrow{lim}_{ζ<ξ}^{WTS} X_{ζ} is cubical if all X_{ζ} for ζ < ξ are cubical since CTS is a coreflective subcategory of WTS. We have proved the first assertion using Proposition 11.5.

2) The second assertion holds for cardinality reasons.

3) For any action u and v of (X_{η}, ∗), we have u ≃_{CSA_{1}} v ⇒ u = v since X_{η} = X_{η+1}. This means that (X_{η}, ∗) satisfies CSA1.

4) Let (α, u_{1}, u_{2}, β), (α, u_{1}, ν_{1}), (α, u_{1}, ν_{2}), (ν_{1}, u_{2}, β) and (ν_{2}, u_{2}, β) be five transitions of (X_{η}, ∗). Thus, the triple ((α, α), u_{1}, (ν_{1}, ν_{2})) is a transition of Path_{∗}(X_{η}, ∗) by Table 2. Since α ≃_{past} α, we deduce that (α, α) is a reachable state of Path_{∗}(X_{η}, ∗), and then that (ν_{1}, ν_{2}) is a reachable state of Path_{∗}(X_{η}, ∗), and therefore that ν_{1} ≃_{past} ν_{2}. Thus, we obtain ν_{1} = ν_{2} since X_{η} = \underline{r}(X_{η}). Let

(α, u_{1}, …, u_{n}, β), (α, u_{1}, …, u_{p}, ν_{1}), (α, u_{1}, …, u_{p}, ν_{2}), (ν_{1}, u_{p+1}, …, u_{n}, β), (ν_{2}, u_{p+1}, …, u_{n}, β)

be five transitions of (X_{η}, ∗) with n ⩾ p + 1 and p ⩾ 2. Since (X_{η}, ∗) is cubical, there exists a state ν_{3} such that the tuples (α, u_{1}, …, u_{p−1}, ν_{3}) and (ν_{3}, u_{p}, …, u_{n}, β) are two transitions of (X_{η}, ∗). By the patching axiom, the triples (ν_{3}, u_{p}, ν_{1}) and (ν_{3}, u_{p}, ν_{2}) are two transitions of (X_{η}, ∗). Since ν_{3} ≃_{past} ν_{3}, we deduce that (ν_{3}, ν_{3}) is a reachable state of Path_{∗}(X_{η}, ∗), and then that (ν_{1}, ν_{2}) is a reachable state of Path_{∗}(X_{η}, ∗), and therefore that ν_{1} ≃_{past} ν_{2}. Thus, we obtain ν_{1} = ν_{2} since X_{η} = \underline{r}(X_{η}). Therefore, (X_{η}, ∗) satisfies CSA2.

5) We deduce that (X_{η}, ∗) is a star-shaped Cattani-Sassone transition system. By construction, the star-shaped transition system (X_{η}, ∗) is reduced. Let us prove by induction on the ordinal ξ that the map (X, ∗) → R_{•}^{⊥}(X, ∗) factors as a composite

(X, ∗) → (X_{ξ}, ∗) →^{ϕ_{ξ}} R_{•}^{⊥}(X, ∗). The case ξ = 0 is trivial. If the map (X, ∗) → R_{•}^{⊥}(X, ∗) factors as a composite (X, ∗) → (X_{ξ}, ∗) → R_{•}^{⊥}(X, ∗), then for any pair of past-similar states (α, β) of X_{ξ}, we have ϕ_{ξ}(α) ≃_{past} ϕ_{ξ}(β) in R_{•}^{⊥}(X, ∗). Thus, we obtain ϕ_{ξ}(α) = ϕ_{ξ}(β) since R_{•}^{⊥}(X, ∗) is reduced. And for any pair of actions (u, v) of X_{ξ} with u ≃_{CSA_{1}} v, we have ϕ_{ξ}(u) ≃_{CSA_{1}} ϕ_{ξ}(v) in R_{•}^{⊥}(X, ∗). Thus, we obtain ϕ_{ξ}(u) = ϕ_{ξ}(v) since R_{•}^{⊥}(X, ∗) satisfies CSA1. We deduce that the map ω(ϕ_{ξ}) : ω(X_{ξ}) → ω(ω^{∗}(R_{•}^{⊥}(X, ∗))) of Set^{{s}∪Σ} factors uniquely as a composite ω(X_{ξ}) → ω(X_{ξ+1}) → ω(ω^{∗}(R_{•}^{⊥}(X, ∗))). We obtain the factorization ϕ_{ξ} : (X_{ξ}, ∗) → (X_{ξ+1}, ∗) → R_{•}^{⊥}(X, ∗). By passing to the colimit, we then obtain the

factorization X ⟶ X_{η} ⟶^{ϕ_{η}} R_{•}^{⊥}(X, ∗). By the universal property of the adjunction, we deduce the isomorphism X_{η} ≅ R_{•}^{⊥}(X, ∗).

11.7. Proposition. Let f : (X, ∗) → (Z, ∗) be a map of star-shaped cubical transition systems with (Z, ∗) fibrant in CSTS_{•}. Let Y = \underline{r}(X). Then (Y, ∗) is a star-shaped cubical transition system. There exists a map g : (Y, ∗) → (Z, ∗) of star-shaped cubical transition systems such that for any state \overline{α} of X, we have gw(\overline{α}) ≃_{past} f(\overline{α}) and for any action \overline{u} of X, we have gw(\overline{u}) = f(\overline{u}) where w : (X, ∗) → (Y, ∗) is the canonical map.

Proof. Let w : (X, ∗) → (Y, ∗) be the canonical map. By Proposition 11.5, (Y, ∗) is a star-shaped cubical transition system. By construction, the map ω(w) has a section s. Let g(α) = fs(α) for a state α of Y and g(u) = fs(u) for an action u of Y. Let \overline{α} ∈ \underline{S}(X). Since wsw(\overline{α}) = w(\overline{α}) in \underline{S}(X)/ ≃_{past}, the pair of states (sw(\overline{α}), \overline{α}) is in the transitive closure of the binary relation ≃_{past} of (X, ∗). Thus, the pair of states (fsw(\overline{α}), f(\overline{α})) is in the transitive closure of the binary relation ≃_{past} of (Z, ∗). But (Z, ∗) is fibrant by hypothesis. By Proposition 9.7, we deduce that fsw(\overline{α}) ≃_{past} f(\overline{α}). We have gw(\overline{α}) = fsw(\overline{α}) by definition of g. We obtain gw(\overline{α}) ≃_{past} f(\overline{α}) for any state \overline{α} of X. Let \overline{u} be an action of X. By a similar argument, we prove that the pair of actions (gw(\overline{u}), f(\overline{u})) is in the transitive closure of the binary relation ≃_{CSA_{1}} of (Z, ∗). Since Z satisfies CSA1, we deduce that gw(\overline{u}) = f(\overline{u}) for any action \overline{u} of X. It remains to prove that g maps a transition of (Y, ∗) to a transition of (Z, ∗). The weak transition system Y is defined as the ω-final lift of the map ω(X) → (\underline{S}(X)/≃_{past}, \underline{L}(X)/≃_{CSA_{1}}). That is to say, it is equipped with the final structure. By [Gaucher, 2010a, Proposition 3.5], this final structure is obtained by considering the set G_{0} of transitions which are in the image of the map (X, ∗) → (Y, ∗), then by applying the patching axiom on the transitions of G_{0} to obtain a set G_{1} ⊇ G_{0}, and by transfinitely iterating the process. The set of transitions ⋃_{ξ⩾0} G_{ξ} is the final structure ^{1}. We are going to prove by transfinite induction on ξ ⩾ 0 that for any transition (α, u_{1}, …, u_{n}, β) of G_{ξ}, the tuple (g(α), g(u_{1}), …, g(u_{n}), g(β)) is a transition of (Z, ∗). First of all, let (α, u_{1}, …, u_{n}, β) ∈ G_{0}. By definition of G_{0}, there exists a transition (\overline{α}, \overline{u_{1}}, …, \overline{u_{n}}, \overline{β}) of (X, ∗) such that (w(\overline{α}), w(\overline{u_{1}}), …, w(\overline{u_{n}}), w(\overline{β})) = (α, u_{1}, …, u_{n}, β).

1[Gaucher, 2010a, Proposition 3.5] also claims that the multiset axiom is automatically satisfied. This is due to the internal symmetry of the patching axiom and to the fact that G_{0} satisfies the multiset axiom.

We have w(\overline{α}) = α = ws(α) since s is a section of w on states. Thus, the pair of states (\overline{α}, s(α)) is in the transitive closure of the binary relation ≃_{past} in (X, ∗). We obtain f(\overline{α}) ≃_{past} fs(α) = g(α) since ≃_{past} is transitive in (Z, ∗) by Proposition 9.7. For the same reason, we obtain f(\overline{β}) ≃_{past} fs(β) = g(β). The tuple (f(\overline{α}), f(\overline{u_{1}}), …, f(\overline{u_{n}}), f(\overline{β})) is a transition of (Z, ∗) since f is a map of transition systems. By Theorem 10.12, and since (Z, ∗) is fibrant by hypothesis, the tuple (g(α), f(\overline{u_{1}}), …, f(\overline{u_{n}}), g(β)) is then a transition of (Z, ∗). We have w(\overline{u_{i}}) = u_{i} = ws(u_{i}) for all 1 ⩽ i ⩽ n. Thus, the pair of actions (\overline{u_{i}}, s(u_{i})) for any 1 ⩽ i ⩽ n is in the transitive closure of the binary relation ≃_{CSA_{1}} in (X, ∗). We obtain f(\overline{u_{i}}) = fs(u_{i}) = g(u_{i}) for all 1 ⩽ i ⩽ n since Z satisfies CSA1. Therefore, the tuple (g(α), g(u_{1}), …, g(u_{n}), g(β)) is a transition of (Z, ∗). The step ξ = 0 of the transfinite induction is proved. The case ξ limit ordinal is trivial. It remains to prove that if all transitions of G_{ξ} are mapped by g to transitions of (Z, ∗), then the same fact holds for G_{ξ+1}. Consider the five tuples

(α, u_{1}, …, u_{n}, β), (α, u_{1}, …, u_{p}, ν_{1}), (ν_{1}, u_{p+1}, …, u_{n}, β), (α, u_{1}, …, u_{p+q}, ν_{2}), (ν_{2}, u_{p+q+1}, …, u_{n}, β)

of G_{ξ} with n ⩾ 3, p, q ⩾ 1 and p + q < n. By definition, the tuple (ν_{1}, u_{p+1}, …, u_{p+q}, ν_{2}) belongs to G_{ξ+1}. By induction hypothesis, the five tuples

(g(α), g(u_{1}), …, g(u_{n}), g(β)), (g(α), g(u_{1}), …, g(u_{p}), g(ν_{1})), (g(ν_{1}),

g(u_{p+1}), …, g(u_{n}), g(β)), (g(α), g(u_{1}), …, g(u_{p+q}), g(ν_{2})), (g(ν_{2}), g(u_{p+q+1}), …, g(u_{n}), g(β))

are transitions of (Z, ∗). By applying the patching axiom in (Z, ∗), we obtain that the tuple (g(ν_{1}), g(u_{p+1}), …, g(u_{p+q}), g(ν_{2})) is a transition of (Z, ∗). The proof is complete.

11.8. Theorem. For any star-shaped transition system (X, ∗), the map Ψ_{(X,∗)} : (X, ∗) → R_{•}^{⊥}(X, ∗) is a weak equivalence of CSTS_{•}.

Proof. Let f : (X, ∗) → (Y, ∗) be a map of star-shaped transition systems. By Proposition 11.6 and Proposition 11.7, there exists a map of star-shaped transition system g : R_{•}^{⊥}(X, ∗) → (Y, ∗) such that for any state α of (X, ∗), we have gΨ_{(X,∗)}(α) ≃_{past} f(α) and for any action u of (X, ∗), we have gΨ_{(X,∗)}(u) = f(u). By Theorem 9.8, we deduce that gΨ_{(X,∗)} and f are homotopy equivalent maps. Thus, the set map

π_{CSTS_{•}}(R_{•}^{⊥}(X, ∗), (Y, ∗)) → π_{CSTS_{•}}((X, ∗), (Y, ∗))

induced by the precomposition with Ψ_{(X,∗)} : (X, ∗) → R_{•}^{⊥}(X, ∗) is onto. Let f, g : R_{•}^{⊥}(X, ∗) → (Z, ∗) be two maps of CSTS_{•} such that fΨ_{(X,∗)} is homotopy equivalent to gΨ_{(X,∗)}. Then fΨ_{(X,∗)} and gΨ_{(X,∗)} coincide on actions by Theorem 9.8 and for any state α of X, the states f(Ψ_{(X,∗)}(α)) and g(Ψ_{(X,∗)}(α)) are past-similar. For any state β of Y, there exists a state α of X such that Ψ_{(X,∗)}(α) = β. Thus, for any state β of Y, the states f(β) and g(β) are past-similar. Since Ψ_{(X,∗)} is onto on actions as well, f and g coincide on actions. We deduce that f and g are homotopy equivalent by Theorem 9.8. We deduce that the set map

π_{CSTS_{•}}(R_{•}^{⊥}(X, ∗), (Z, ∗)) → π_{CSTS_{•}}((X, ∗), (Z, ∗))

induced by the precomposition with Ψ_{(X,∗)} is one-to-one.

11.9. Theorem. The left adjoint R_{•}^{⊥} : CSTS_{•} → \overline{CSTS_{•}} induces a Quillen equivalence between the model category CSTS_{•} and the category \overline{CSTS_{•}} equipped with the discrete model category structure.

Proof. For any reduced star-shaped transition system (X, ∗), we have by Proposition 9.2 and by Table 2 the equality Path_{•}(X, ∗) = (X, ∗). Let α be a state of X. Since (X, ∗) is star-shaped, there exists w ∈ Σ^{n} with n ⩾ 0 and a map f : (P (w), 0) → (X, ∗) such that f(n) = α. By functoriality, we obtain a map Cyl_{•}(f) : Cyl_{•}(P (w), 0) → Cyl_{•}(X, ∗). Thus, we have (α, 0) ≃_{past} (α, 1) in Cyl_{•}(X, ∗). This implies that R_{•}^{⊥}(Cyl(X, ∗)) = (X, ∗) for any reduced star-shaped transition system (X, ∗). Using [Gaucher, 2015c, Theorem 3.1], we obtain a left determined Olschok model structure on \overline{CSTS_{•}} such that the cylinder and path functors are the identity functor. Therefore, we have the equalities

π\overline{CSTS_{•}}((X, ∗), (Y, ∗)) = πl ; \overline{CSTS_{•}}((X, ∗), (Y, ∗))

= πr ; \overline{CSTS_{•}}((X, ∗), (Y, ∗)) = \overline{CSTS_{•}}((X, ∗), (Y, ∗))

for any reduced Cattani-Sassone transition system (X, ∗) and (Y, ∗). This means that the weak equivalences of \overline{CSTS_{•}} are the isomorphisms. Thus, the left adjoint R_{•}^{⊥} : CSTS_{•} → \overline{CSTS_{•}} induces a homotopically surjective left Quillen adjoint from CSTS_{•} to \overline{CSTS_{•}} equipped with the discrete model structure. By Theorem 11.8, this left Quillen adjoint is a left Quillen equivalence.

The following corollary proves that a map of star-shaped transition systems is a weak equivalence if and only if it becomes an isomorphism after the identification of all pastsimilar states.

11.10. Corollary. A map f of CSTS_{•} is a weak equivalence if and only if R_{•}^{⊥}(f) is an isomorphism.

Proof. Since all objects of CSTS_{•} are cofibrant, a weak equivalence f is mapped to a weak equivalence R_{•}^{⊥}(f) of \overline{CSTS_{•}}, i.e. an isomorphism. Conversely, if R_{•}^{⊥}(f) is an isomorphism, then by Theorem 11.8 and the two-out-of-three property, f is a weak equivalence.

12. Causality and homotopy

This concluding section is written to interpret Theorem 11.9. All left determined model categories constructed so far on higher dimensional transition systems, including the ones of [Gaucher, 2011] and [Gaucher, 2015b] where R : {0, 1} → {0} is a generating cofibration, are Quillen equivalent to discrete model categories. Similar left determined model categories on flows [Gaucher, 2003] and multipointed d-spaces [Gaucher, 2009] do not have such a behavior. This phenomenon could be related to the absence of thin objects in higher dimension in the formalism of higher dimensional transition systems which categorically behave like labelled symmetric precubical sets [Gaucher, 2010a, Theorem 11.6].

To be more specific in the sequel, we will be using the 1-dimensional paths (P (w), 0) with w ∈ Σ^{∗} (where Σ^{∗} = ⋃_{n⩾0} Σ^{n} is the set of words over Σ). The arguments developed here could be adapted to more complicated notions of paths, in particular higher dimensional ones like in [Fahrenberg and Legay, 2013]. Let

P = {(P (w), 0) → (P (ww′), 0) | w, w′ ∈ Σ^{∗}}

be the set of extensions of paths. The semantics of [Gaucher, 2010a] is used in this section. The reader does not actually need to read the latter paper to understand the sequel. Indeed, except for Proposition 12.2 whose proof is just sketched, the only facts to know are that:

1. All P-cell complexes are realizations of process algebras.

2. All realizations of process algebras are colimits of cubes.

12.1. Definition. After [Joyal, Nielsen, and Winskel, 1996], two star-shaped transition systems (X, ∗) and (Y, ∗) are P-bisimilar if they are related by a span of P-injective maps (X, ∗) ← (Z, ∗) → (Y, ∗).

Since the class of P-injective maps is closed under pullback and composition, two starshaped transition systems (X, ∗) and (Y, ∗) are P-bisimilar if and and only if they are related by a zig-zag of P-injective maps. Note that a P-injective map between star-shaped transition systems is always onto on states, on actions and on 1-dimensional transitions.

12.2. Proposition. Any two weakly equivalent star-shaped transition systems of the left determined Olschok model category CSTS_{•} realizing process algebras are isomorphic, and hence P-bisimilar. There exist two P-bisimilar P-cell complexes which are not weakly equivalent.

Proof. (sketch) A star-shaped transition system realizing a process algebra is reduced: the proof is by induction on the syntactic description of the process algebra. Thus, if two of them are weakly equivalent, they are isomorphic by Corollary 11.10. The two P-cell complexes (P (u), 0) ⊔ (P (u), 0) and (P (u), 0) are P-bisimilar since the unique map (P (u), 0) ⊔ (P (u), 0) → (P (u), 0) is P-injective. They can be depicted as follows with μ(u_{1}) = μ(u_{2}) = u:

\xymatrix{ &  & • \\ (P (u), 0) ⊔ (P (u), 0) = & 0 \ar@{-->}[ur]^{u_{1}} \ar[dr]_{u_{2}} &  & (P (u), 0) = & 0 \ar[r]^{u_{1}} & • \\  &  & •}

However, they are reduced and not isomorphic. Thus, they are not weakly equivalent by Corollary 11.10.

12.3. Definition. A model structure on CSTS_{•} is P-causal (with respect to the semantics of [Gaucher, 2010a]) if any two star-shaped transition systems realizing process algebras are weakly equivalent if and only if they are P-bisimilar.

12.4. Theorem. Consider a model structure of CSTS_{•} such that all P-cell complexes are cofibrant and such that all P-injective maps are weak equivalences. Then there exist two homotopy equivalent P-cell complexes which are not P-bisimilar. In particular, this model structure is not P-causal.

Proof. Consider the two P-cell complexes (M_{0}, 0) = (P (uv), 0)⊔(P (u), 0) and (M_{1}, 0) = (P (uv), 0). The star-shaped transition systems (M_{0}, 0) and (M_{1}, 0) look as follows (with μ(u_{1}) = μ(u_{2}) = u and μ(v_{1}) = v):

\xymatrix{ &  & • \ar[r]^{v_{1}} & • \\ (M_{0}, 0) = & 0 \ar@{-->}[ur]^{u_{1}} \ar[dr]_{u_{2}} &  &  & (M_{1}, 0) = & 0 \ar[r]^{u_{1}} & • \ar[r]^{v_{1}} & • \\  &  & •}

They are not P-bisimilar since the path 0 →^{u_{2}} • of (M_{0}, 0) cannot be extended. Let f : (M_{0}, 0) → (M_{1}, 0) be the unique map defined on actions by the mappings u_{1}, u_{2} ↦ u_{1} and v_{1} ↦ v_{1}. Let g : (M_{1}, 0) → (M_{0}, 0) be the unique map defined on actions by the mappings u_{1} ↦ u_{1} and v_{1} ↦ v_{1}. Consider a commutative diagram of solid arrows of

CSTS_{•}
\xymatrix{(P (w), 0) \ar[r]^{ϕ} \ar[d] & (M_{0}, 0) ⊔ (M_{0}, 0) \ar[d] \\ (P (ww′), 0) \ar[r] \ar@{-->}[ur]^{ℓ} & (M_{0}, 0)}

where w, w′ ∈ Σ^{∗}. The only possibilities for w, ww′ ∈ Σ^{∗} are w, ww′ ∈ {∅, u, uv}. Consequently, the map ϕ factors as a composite

(P (w), 0) ⟶ (M_{0}, 0) ⟶ (M_{0}, 0) ⊔ (M_{0}, 0).

Thus, the lift ℓ exists. We deduce that the codiagonal map (M_{0}, 0) ⊔ (M_{0}, 0) → (M_{0}, 0) factors as a composite

\xymatrix{(M_{0}, 0) ⊔ (M_{0}, 0) \ar[r]^{≅} & (M_{0}, 0) ⊔ (M_{0}, 0) \ar[r]^{∈inj_{_{CSTS}_{•}}(P)} & (M_{0}, 0)}

where the left-hand map is a cofibration and the right-hand map is P-injective, i.e. by hypothesis a weak equivalence. Consequently, (M_{0}, 0) ⊔ (M_{0}, 0) is a good cylinder of (M_{0}, 0) for this model structure. We deduce that the maps Id_{(M_{0},0)}, gf : (M_{0}, 0) ⇉ (M_{0}, 0) are left homotopic maps. By [Hirschhorn, 2003, Proposition 7.4.8], and since (M_{0}, 0) is cofibrant by hypothesis, Id_{(M_{0},0)} and gf are right homotopic, and then homotopic. For the same reason, the maps Id_{(M_{1},0)} and fg are homotopic. Therefore, the star-shaped transition systems (M_{0}, 0) and (M_{1}, 0) are homotopy equivalent in this model structure.

Theorem 12.4 and its proof tell us that localizing with respect to the whole class of P-injective maps is a very bad idea. Theorem 12.4 also tells us that the most obvious candidate, the left determined model structure with respect to P, whose existence is a consequence of Vopěnka’s principle by [Rosický and Tholen, 2003, Theorem 2.2], is not P-causal either.

Theorem 12.4 also holds by replacing the category of star-shaped transition systems by any category of labelled precubical sets of [Gaucher, 2008] or [Gaucher, 2010b]. Indeed, the origin of the problem is that the map (X, ∗) ⊔ (X, ∗) → (X, ∗) is P-injective for any star-shaped transition system (X, ∗) not containing any cycle passing by the base state ∗, which means in this case that a good cylinder of (X, ∗) is (X, ∗) ⊔ (X, ∗) in such a model structure.

It turns out that there exist star-shaped transition systems which are not colimits of cubes, e.g. the star-shaped transition systems of Figure 2 and Figure 3. It is actually the main technical difference with any category of labelled precubical sets of [Gaucher, 2008] or [Gaucher, 2010b]. To overcome the problem arising from Theorem 12.4, the idea is to localize with respect to a class of P-injective maps between star-shaped transition systems which are P-optimized in the sense that they use a minimal set of actions. For example, with (X, ∗) = (P (uv), ∗), the star-shaped transition system (X, ∗) ⊔ (X, ∗) looks as follows (with μ(u_{1}) = μ(u_{2}) = u and μ(v_{1}) = μ(v_{2}) = v):

\xymatrix{ &  & • \ar[r]^{v_{1}} & • \\ (X, ∗) ⊔ (X, ∗) = & ∗ \ar[ur]^{u_{1}} \ar[dr]_{u_{2}} \\  &  & • \ar[r]_{v_{2}} & •}

and its P-optimized version is:

\xymatrix{ &  & • \ar[r]^{v} & • \\ (Y, ∗) = & ∗ \ar[ur]^{u} \ar[dr]_{u} \\  &  & • \ar[r]_{v} & •}

The star-shaped transition system of (Y, ∗) is exactly the one of Figure 2. The star-shaped transition systems (X, ∗) ⊔ (X, ∗) and (Y, ∗) are P-bisimilar and (Y, ∗) uses as few actions as possible. Note that (X, ∗) ⊔ (X, ∗) is never P-optimized unless X = {∗}.

The pushout diagram of Figure 5 highlights another problem which seems to indicate that left properness could be an obstacle. All star-shaped transition systems of Figure 5 are P-optimized. The left vertical map is P-injective. The right vertical map is not P-injective since the bottom path of the domain ∗ →^{u} • →^{v} • cannot be extended. It turns out that the right vertical map identifies two states having the same past and not the same future. There are two ways of overcoming this situation: 1) noticing that the domain and the codomain of the bottom horizontal arrow are not the optimizations of

[figure: •; v; •; •; v; •; w; •; ∗; u; u; ∗; u; u; •; v; •; •; v; •; •; v; •; v; ∗; u; u; •; ∗; u; u; •; w; •; •; v; •; v]

Figure 5: A pushout of a P-injective map which is not P-injective

[figure: •^{β}; •^{α}; u; •^{γ}; ∩; •^{β}; •^{α}; u; •^{γ}; •^{α′}; u; •^{γ′}; ∩; •^{β}; •^{α}; u; u; •^{γ}]

Figure 6: Erratum

star-shaped transition systems coming from a process algebra; indeed the semantics of [Gaucher, 2010a] cannot create directed cycles; 2) colocalizing with respect to the set of paths; then the domain and the codomain of the bottom horizontal arrow are not cofibrant anymore.

After all these observations, we want to study localizations with respect to P-injective maps between P-optimized realizations of process algebras and also localizations of the colocalization with respect to the set of paths of CSTS_{•}. The colocalization is not left proper and entails the introduction of a new underlying category.

A. Erratum

[Gaucher, 2015a, Theorem A.2] is false. It is used in [Gaucher, 2015a, Proposition 2.7] and in [Gaucher, 2015a, Theorem 3.7]. [Gaucher, 2015a, Proposition 2.7] is still true.

[Gaucher, 2015a, Theorem 3.7] is not true. Indeed, the cofibration

[figure: •^{β}; •^{α}; u; •^{γ}; ∩; •^{β}; •^{α}; u; u; •^{γ}]

is not a transfinite composition of pushouts of maps of

I^{CTS} = {C : ∅ → {0}}

∪ {∂C_{n}[x_{1}, …, x_{n}] → C_{n}[x_{1}, …, x_{n}] | n ⩾ 1 and x_{1}, …, x_{n} ∈ Σ}

∪ {C_{1}[x] →↑x↑| x ∈ Σ}.

However, it belongs to cell_{CTS}(I^{CTS} ∪ {R : {0, 1} → {0}}) by the sequence of inclusions of Figure 6. The correct statement of [Gaucher, 2015a, Theorem 3.7] is obtained by replacing the maps C_{1}[x] →↑x↑ for x running over Σ by the maps C_{0}⊔C_{0}⊔C_{1}[x] →↑x↑ for x running over Σ which are defined to be bijective on states (see Notation 5.12 of this paper).

References

J. Adámek and J. Rosický. Locally presentable and accessible categories. Cambridge University Press, Cambridge, 1994. ISBN 0-521-42261-2.

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. ISSN 1201-561X. Reprint of the 1990 original [Wiley, New York; MR1051419].

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.

D. Dugger. Combinatorial model categories have presentations. Adv. Math., 164(1):177– 201, 2001. ISSN 0001-8708.

U. Fahrenberg and A. Legay. History-preserving bisimilarity for higher-dimensional automata via open maps. In Proceedings of the 29th conference on the mathematical foundations of programming semantics (MFPS XXIX), New Orleans, LA, USA, June 2013, pages 165–178. Amsterdam: Elsevier, 2013. doi: 10.1016/j.entcs.2013.09.012.

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

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

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

P. Gaucher. Directed algebraic topology and higher dimensional transition systems. New York J. Math., 16:409–461 (electronic), 2010a.

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

P. Gaucher. Towards a homotopy theory of higher dimensional transition systems. Theory Appl. Categ., 25:No. 25, 295–341 (electronic), 2011.

P. Gaucher. Erratum to ”Towards a homotopy theory of higher dimensional transition systems”. Theory Appl. Categ., 29:No. 2, 17–20 (electronic), 2014a.

P. Gaucher. Homotopy theory of labelled symmetric precubical sets. New York J. Math., 20:93–131 (electronic), 2014b.

P. Gaucher. The choice of cofibrations of higher dimensional transition systems. New York J. Math., 21:1117–1151 (electronic), 2015a.

P. Gaucher. The geometry of cubical and regular transition systems. Cah. Topol. Géom. Différ. Catég., LVI-4:242–300, 2015b.

P. Gaucher. Left determined model categories. New York J. Math., 21:1093–1115 (electronic), 2015c.

P. Hirschhorn. Overcategories and undercategories of model categories. arXiv:1507.01624, 2015.

P. S. Hirschhorn. Model categories and their localizations, volume 99 of Mathematical Surveys and Monographs. American Mathematical Society, Providence, RI, 2003. ISBN 0-8218-3279-4.

M. Hovey. Model categories. American Mathematical Society, Providence, RI, 1999. ISBN 0-8218-1359-5.

A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Inf. Comput., 127 (2):164–185, 1996. doi: 10.1006/inco.1996.0057.

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

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

M. Olschok. On constructions of left determined model structures. PhD thesis, Masaryk University, Faculty of Science, 2009b.

G. Raptis and J. Rosický. The accessibility rank of weak equivalences. Theory Appl. Categ., 30:No. 19, 687–703 (electronic), 2015.

J. Rosický. On combinatorial model categories. Appl. Categ. Structures, 17 (3):303–316, 2009. ISSN 0927-2852. doi: 10.1007/s10485-008-9171-2. URL

  http://dx.doi.org/10.1007/s10485-008-9171-2.

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

A. Salch. The Bousfield localizations and colocalizations of the discrete model structure. Topology Appl., 219:78–89, 2017. ISSN 0166-8641. doi: 10.1016/j.topol.2017.01.005.

  URL http://dx.doi.org/10.1016/j.topol.2017.01.005.

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.

Institut de Recherche en Informatique Fondamentale CNRS et Université Paris Diderot Case 7014 75205 PARIS Cedex 13 France

http://www.irif.fr/~gaucher

This article may be accessed at http://www.tac.mta.ca/tac/

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 from the journal’s server at http://www.tac.mta.ca/tac/. 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 is required. Articles in PDF format may 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 Valeria de Paiva: Nuance Communications Inc: valeria.depaiva@gmail.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne: kathryn.hess@epfl.ch Martin Hyland, University of Cambridge: M.Hyland@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 Edinburgh: Tom.Leinster@ed.ac.uk Ieke Moerdijk, Utrecht University: i.moerdijk@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 Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Alex Simpson, University of Ljubljana: Alex.Simpson@fmf.uni-lj.si James Stasheff, University of North Carolina: jds@math.upenn.edu Ross Street, Macquarie University: ross.street@mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Université du Québec à Montréal : tierney.myles4@gmail.com R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca