{'fraction_non_alphanumeric': 0.04253676404575081, 'fraction_numerical': 0.007954321009821701, 'mean_word_length': 3.9102183560114026, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 35, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Algebraic models of homotopy types and the homotopy hypothesis

We introduce and study a notion of cylinder coherator similar to the notion of Grothendieck coherator which define more flexible notion of weak infinity groupoids. We show that each such cylinder coherator produces a combinatorial semi-model category of weak infinity groupoids, whose objects are all fibrant and which is in a precise sense"freely generated by an object". We show that all those semi model categories are Quillen equivalent together and Quillen to the model category of spaces. A general procedure is given to produce such coherator, and several explicit examples are presented: one which is simplicial in nature and allows the comparison to the model category for spaces. A second example can be describe as the category of globular sets endowed with"all the operations that can be defined within a weak type theory". This second notion seem to provide a definition of weak infinity groupoids which can be defined internally within type theory and which is classically equivalent to homotopy types. Finally, the category of Grothendieck infinity groupoids for a fixed Grothendieck coherator would be an example of this formalism under a seemingly simple conjecture whose validity is shown to imply Grothendieck homotopy hypothesis. This conjecture seem to sum up what needs to be proved at a technical level to ensure that the theory of Grothendieck weak infinity groupoid is well behaved.


Motivations
In the unpublished manuscript [13], A.Grothendieck introduced a very natural (although quite ingenious) notion of "weak 1 ∞-groupoid", a presentation of this notion can be found in [18]. Grothendieck showed in particular that to any topological space one can associate such a "fundamental" weak ∞-groupoids, encoding paths, homotopy between path, homotopy between homotopy and so on, and he stated a precise conjecture asserting that this fundamental ∞groupoid construction induces an equivalence between the homotopy category of spaces and the homotopy category of his weak ∞-groupoids. This conjecture is known as Grothendieck Homotopy Hypothesis (conjecture 2.8 of [18]). It is well known that strict ∞-groupoids, while considerably easier to define, are not sufficient for this kind of results, for example it is proved in [24] that the fundamental 3-groupoids of the 2-sphere cannot be represented in a reasonable way by a strict 3-groupoids, and other obstruction results in this spirit where known long before.
Grothendieck's definition of weak ∞-groupoids has also been extended by G.Maltsiniotis (in [18]) to a definition of weak ∞-categories (often called Grothendieck-Maltsiniotis ∞-categories). A related definition of weak ∞-categories has been proposed independently by M.Batanin in [5] and improved by T.Leinster in [14]. These are called Batanin or Batanin-Leinster ∞-categories. The precise relationship between Grothendieck-Maltsiniotis and Batanin-Leinster ∞-category is explained in D.Ara p.h.d. thesis, [2]. All these approaches are "globular" in the sense that an ∞-category is represented by a globular set with operations, i.e. one has a set of objects, a set of morphisms between any two objects, a set of 2-morphisms between any two parallel morphisms, 3-morphisms between any pair of parallel 2-morphisms, etc. with all the compositions operations and coherence isomorphisms that one can expect in a ∞-categories.
Nowadays, it seems that, while the fact that weak ∞-groupoids and spaces up to weak homotopy equivalence are the same is considered as a very important and deep fact, Grothendieck homotopy hypothesis seem to be considered more as a marginal problem. Indeed it has generally been accepted that instead of trying to define what is a ∞-groupoid one should take the homotopy hypothesis as their definition. One can for example replace spaces by a more algebraic category which is known to be equivalent and define an ∞-groupoid to be a simplicial Kan complex. This has been taken as the starting point of higher category theory. From this definition of ∞-groupoid as the Kan complex, one have then been able to define (∞, 1)-categories , i.e. ∞-categories where all the 2-arrows and above are invertible, as simplicially enriched categories, complete Segal spaces or as quasi-categories, and those have been studied extensively. In fact large portion of ordinary category theory can be extended to those (∞, 1)-categories (see for examples [17] and [16]).
Moreover, the fact that the homotopy hypothesis has not been proved is not the only problem with the "globular" approaches to higher categories mentioned above: Their definition depends on certain choices (a coherator for Grothendieck-Maltsiniotis ∞-categories, and a weakly initial contractible globular operad for Batanin-Leinster ∞-categories), different choices produces different categories of ∞groupoids (and strict functors) and it is unknown if these choices are unimportant "up to homotopy". Also defining what are weak functors and weak natural transformations between ∞-categories is problematic, there has been approaches proposed (see for example [5, 8.8 and 8.9] ) but it is not always clear how to compose two such functors and natural transformation and in any case we do not know how to show that one can form an ∞-category of ∞-groupoids or of ∞-categories. We do not know either how to form an ∞-groupoids of functors between two ∞-groupoids, in fact we do not even know how to form the ∞-groupoid of arrows of a given ∞-groupoid 2 or slices of an ∞-category. All these problems prevent us to develop a nice theory of globular higher categories as it has been done for the simplicial approaches (for example in [17] and [16]).
This might sound very discouraging and a good reason to completely forget about globular approaches to higher category theory, but the recent development of homotopy type theory (see [27]) has given us very good reasons to be interested in these globular approaches again. Indeed, one thing that seem to be missing in present higher category theory is a good notion of internal logic of a (∞, 1)-category, and it is exactly what intentional type theory is supposed to be: intentional type theory with just identity type and Σ-type should be the internal logic of a (∞, 1)-category with finite projective limits. Strongest type theories ( with functions type, functional extensionality , Π-type, higher inductive type, univalence axiom etc... ) should corresponds to more structured higher categories (like locally cartesian closed or co-complete) and full homotopy type theory as presented in [27] should corresponds to the internal logic of an (∞, 1)-topos. This already gives us a first reason to be interested in Grothendieck ∞-groupoids and more generally in globular Higher categories: type theory is deeply globular, indeed, any naive notion of model of type theory produces globular sets and even globular higher groupoids (see [26], [15] and [8]). One could says that type theory should be in fact the internal logic of a certain type of globular (∞, 1)-categories. A second reason is that it is of prime importance for ordinary categorical logic to be able to discuss category theory itself "internally". One should hence expect that the internal logic of a Higher categories should be able to discuss higher category theory as well. It appears that intentional type theory has been unable at the present time to discuss simplicial or semi-simplicial sets, in the sense that we are not able to write down a definition of "simplicial types" making sense in type theory, hence there is no chance (at least at the present time) that we can use quasi-categories or simplicially enriched categories within type theory. Being able to discuss higher categories under one form or another is one of the most important open problem in homotopy type theory.
Surprisingly, it appears that it is not too difficult to define a globular type (it is generally done using co-induction) and it has been shown (see [10], [1]) that it is possible to define a notion of globular weak ∞-groupoid meaningful in type theory, and very close, if not equivalent, to Grothendieck's original definition.
Of course as we are not able to manipulate globular higher groupoids correctly in classical mathematics we do not know how to do it in type theory either so this does not told us how to discuss higher categories correctly within type theory.
This work started as an attempt to make the theory of globular higher categories work as well as the other approaches (for example simplicial) to higher categories at least in classical mathematics. We failed to completely solve any of the problems mentioned above for either the Gorthendieck-Maltsiniotis or the Batanin-Leinster approaches, but one has obtain some results in that direction, as well as ways to avoid those difficult problems.
completely For examples, one of the consequences of the following work is a new globular approach to weak ∞-groupoids based on type theory for which we can prove in classical mathematics the analogue of the homotopy hypothesis and which seems to be sufficient for the two motivations mentioned above: it should be definable within type theory and any type in intentional type theory caries the structure of such an ∞-groupoid.
Another problem is that the definitions of higher categorical structures that are classically used (like quasi-categories) seems to all be deeply "non-constructive". We think that the models we are producing here for ∞-groupoids will be more suited for studying higher categorical structures within constructive framework.
Although the long terms goal of this works is to obtain model of Higher categorical structures that will work within constructive mathematics and intentional type theory, the present paper focus on the non-constructive point of view: our main goal is to prove that our new definitions of higher groupoids are equivalent to more classical (and generally non-constructive) notion of higher groupoids (space or Kan complex). Also we will entirely focus on ∞-groupoids, but we hope that the methods developed in this paper might allows us to discuss more general higher structures in future work (like (∞, 1) and ∞-categories, monoidal (∞, 1)-categories, ∞operads etc...)

Introduction
At a more technical level, the main contribution of the present work can be described as a construction that allows to produce semi 3 -model categories whose objects are all fibrant and which are "freely generated by one object" among such category in a correct homotopy theoretical sense. We will also set up a formalism that will allow to discuss and study more general sort of "freely generated" semi-model categories that we hope might be of help to discuss more general higher categorical structures latter (like ∞-categories, ∞-operads, etc.).
1.2.1. This follows the idea that the (∞, 1)-category of ∞-groupoids is the co-complete (∞, 1)-category freely generated by one object and that (combinatorial) model categories are model for locally presentable (hence co-complete) (∞, 1)-categories. For this reasons those semi-model categories freely generated by one object will be thought of as semi-model categories of weak ∞-groupoids, and as they share a (homotopical) universal property they will automatically be all Quillen equivalent.
In order to perform this construction we will rely heavily on a notion weaker than model category: "categories with cylinder object" or in short "cylinder categories". They are the categorical opposite of the path categories introduced recently by B.Van der Berg and I.Moerdijk in [7], which in turn are a strengthening of K.Brown category of fibrant objects (introduced in [9]). See section 2.
If (combinatorial) model categories are supposed to model locally presentable (∞, 1)-categories, cylinder categories are supposed to model finitely co-complete (∞, 1)-categories. Our construction will be done in two step: first we construct a cylinder category "homotopically freely generated by one object" and then we "complete" it into a semi-model category.
The first step will be achieved by constructing (in section 4) a sort of weak model category whose fibrant objects are the cylinder categories. This allows us to perform all sort of free construction by first considering a genuine algebraic free construction and then take a fibrant replacement, hence producing a cylinder category which satisfies a homotopy theoretic version of the universal property of an actual freely generated object. The second step is more rigid and not homotopy theoretical in nature: the functor from the category of semi-model categories with fibrant object and left Quillen functors to the category of cylinder categories, which send a semi-model categories to its category of cofibrant object have (up to standard size problems) a left adjoint studied in subsection 2.4.
Combining the two steps one obtains semi-model categories whose objects are all fibrant which satisfies a weak universal property saying that it is freely generated by one object among semi-model category whose objects are all fibrant with left Quillen functors as morphisms.
1.2.2. The first step should be thought of an analogue of the construction of a Grothendieck coherator and the cylinder category obtained this way will be called a cylinder coherator (see 5.1) for this reason. The analogy is made very precise in subsection 5.1 where we prove that under a technical conjecture a Gorthendieck coherator actually produces a cylinder coherator which defines the same notion of weak ∞-groupoids.
The second step will be thought of as looking at the category of groupoids with respect to this cylinder coherator.
In some sense the objects of the cylinder coherator are all the finite "generalized diagrams" that are meaningful for our notion of groupoids, the cofibrations between them are the inclusions of diagrams and the more general map are the various composition and coherence operations expected for our notion of weak ∞-groupoids.
While ideas from type theory have been extremely influential in this work, explicit mention of type theory will be kept to a minimum in the present paper. It will only reappears as an example in the last subsection 5.4. But in some sense, type theory is hidden in the notion of cylinder category, as it has been shown in [6] that path categories (the dual of cylinder categories) are in some sense the categorical semantics of a weak intentional type theory where the identity elimination principle has been replaced by a propositional equality instead of a definitional equality. In some sense a cylinder coherator can be thought of as the opposite of the syntactic category of a certain kind of intentional type theory "freely generated" by one type (this analogy will be made a little more precise in subsection 5.4).
In section 2, we will first recall 4 the notion of cylinder category and its basic properties. In 5.4 we introduced a notion of equivalence between cylinder categories called acyclic morphism. This notion is new but very similar results were already known for Brown category of fibrant objects and due to D-C.Cisinski (see theorem 3.19 of [11]). Finally in subsection 2.4 we construct the "completion" of a cylinder category into a semi-model category, we prove the universal property of this completion and show that acyclic morphisms of cylinder categories induce Quillen equivalences between the completions.
In section 3 we introduced the category of "pre-cylinder categories" and study its algebraic property. The underlying idea is that we have only kept the properties of cylinder categories that are "algebraic" in nature and forget the weak structures (existence of factorization of morphisms and of retractions of trivial cofibrations) of cylinder categories that were not preserved by morphisms of cylinder categories. Doing so have the effect of providing a category (of pre-cylinder categories) which is much more algebraic and admit all sort of categorical construction, in particular free constructions discussed in 3.2 and a symmetric closed monoidal structure discussed in 3.3.
In section 4 we construct our "weak model structure" on the category of precylinder categories whose fibrant object are the cylinder categories and whose weak equivalences between fibrant objects are the acyclic morphisms. A precise summary of the sense in which it is a weak model structure can be found in 4.3.5. In subsection 4.1 we introduce the two (partial) weak factorization systems of our model category structure, in subsection 4.2 we use our notion of fibration of pre-cylinder categories and the monoidal structure on the category pre-cylinder categories to give a new presentation of the construction of "Reedy type" cylinder categories (but much of the results here were already known and can be found in [11] or [22] with more down to earth proof), we then use this to construct some examples of fibrations and trivial fibrations of cylinder categories that will play the role of a path objects for cylinder categories and are a key component in the proof of the existence of our weak model structure.
In subsection 4.3 we finish the construction of the weak model structure. In subsection 4.4 we discuss a construction of a "homotopy slice" of a cylinder categories that produces new examples of fibrations of cylinder categories, this construction will be used in subsection 5.3.
In the final section (5) of the paper we introduce the notion of cylinder coherator. A cylinder coherator (definition 5.1.1) is a fibrant replacement of the free precylinder categories F * generated by one object (see 3.1.7), if C is a cylinder coherator a C-groupoids is an object of the semi-model categories C obtained using the completion procedure of subsection 2.4. The main result of the paper is theorem 5.1.2 which gives all the good properties of this notion of weak groupoids, at this point all those properties except the homotopy hypothesis follows trivially from the framework developed in the rest of the paper. In order to prove the analogue of the homotopy hypothesis for C-groupoid we just need to prove it for a single cylinder coherator C, which is done in the next subsection. The small object argument provides examples of cylinder coherator, but those tends not to be very convenient. The last three sub-sections are each devoted to deals with specific cylinder coherators which are simpler than those produced by a naive application of the small object argument: In subsection 5.2 we construct a cylinder coherator whose associated notion of weak ∞-groupoids are semi-simplicial Kan complex for which we are able to prove a comparison theorem with the homotopy category of spaces and hence proving the homotopy hypothesis for all cylinder coherator.
In subsection 5.3 we show that under a simple looking technical conjecture (5.3.3) the theory of Grothendieck ∞-groupoids fits into our framework and hence that conjecture 5.3.3 implies Grothendieck homotopy hypothesis. This conjecture is a very concrete statement about Grothendieck's definition which seem considerably weaker than the homotopy hypothesis. A failure of this conjecture would in some sense means that Grothendieck's definition is missing some operations that should be present for weak ∞-groupoids (for example, it would miss certain operations that are definable in intentional type theory). We also show (without any assumption) that any object in a path category (the opposite of a cylinder categories) caries the structure (on its iterated path objects) of a Grothendieck ∞-groupoid. Combining this with the result of [6] that syntactic categories of type theory with propositional identity types are path categories this allows to extend the result of [8] that type in intentional type theory are Grothendieck groupoids to the case of a type theory with propositional identity types (the strategy of [8] does not extend to this case). Finally in subsection 5.4 we show that the opposite of the syntactic category of type theory with just propositional identity type and one "free" type * is a cylinder coherator. This produces a globular and syntactical definition of weak ∞-groupoids which is very similar to the definition given in [10] and [1] but for which, contrary to Grothendieck's definition, one can prove the homotopy hypothesis, the existence of a semi-model structure of these weak ∞-groupoids and one has a definition of the ∞-groupoids of weak functors between two ∞groupoids. We are convinced that this notion of weak ∞-groupoids will make sense in intentional type theory, but we think that only a computer implementation would be a convincing proof of this. 3) a structure similar to Quillen model category but where the factorization of an arrow as a trivial cofibration followed by a fibration is only possible for arrow whose domain is cofibrant (all the other axioms being the same). A semi-model category is said to be combinatorial if the underlying category is locally presentable and if there is two sets of morphisms I and J (called the generating cofibration and generating trivial cofibration) such that fibrations are the arrow with the right lifting property with respect to J and trivial fibrations are the arrow with the right lifting property with respect to I. In this situation we will call "trivial cofibration" the map in the class generated by J, i.e. the map that have the left lifting property with respect to all fibration and "acyclic cofibrations" the map that are cofibration and weak equivalences, those two class agree for arrow whose domain is cofibrant but we cannot say anything for general arrows. Most of the notion and construction available for ordinary model category carries over easily to semi-model category, we just need to take cofibrant replacement a little more often to avoid the pathological behavior of trivial cofibration with a non-cofibrant domain. In particular, one still have the same description of the homotopy category in terms of fibrant/cofibrant objects, the notion of Quillen adjunction and Quillen equivalences are still the same and a Quillen equivalence still induces an equivalence between the homotopy categories.

Preliminaries
In diagrams, hooked arrow denoted (֒→) always denote cofibration (we will not use this notion for monomorphism) and the symbol ∼ on a arrow mean that is is a weak equivalence and fibrations are denoted by arrow of the form ։. 3. C has an initial object 0 and for all object X of C the unique map 0 → X is a cofibration.

Pushout of cofibrations exist and are cofibrations.
5. Pushout of trivial cofibrations are trivial cofibrations. 6. For every object X ∈ C there exists a fatorization of the codiagonal: Where the first map is a cofibration and the second is a weak equivalence.

Every trivial cofibration admit a retraction.
Cylinder categories are exactly the opposites of the "Path categories" introduced recently by I.Moerdijk and B.van den Berg in [7]. They are also closely related to Brown categories of co-fibrant objects [9].
2.1.2. An object IX in a factorization as a cofibration followed by a weak equivalence: is called a cylinder object for X. "IX" will always denotes such a cylinder object for X.
2.1.3. The 2-out-of-6 property easily implies the more usual 2-out-of-3 property saying that if any two of the arrows f, g and f • g are weak equivalences then the third also is. A discussion of the role of this stronger 2-out-of-6 property in comparison with the 2-out-of-3 property can be found in 2.2.11.
Here are some examples of cylinder categories: • If C is a semi-model category in which every object is fibrant, then the full subcategory of co-fibrant objects (with the induced notion of weak equivalences and cofibration) is a cylinder category.
• The category of CW -complexes with homotopy equivalences and the relative CW -map as cofibration is a cylinder category (It is almost a special case of the above).
• The category of finite CW -complexes (with the same weak equivalences and cofibratons) is again a cylinder category: indeed cylinder objects for finite CW -complex can be chosen to be finite and pushout along cofibrations between finite CW -complexes produces finite CW -complexes.

Definition :
A morphism F between cylinder categories is a functor F : C → C ′ such that: • F sends weak equivalences to weak equivalences.
• F preserve the initial object and the pushout along cofibrations.
Such morphisms are also called "exact functor" in the literature. Note that there is a terminal cylinder category: the terminal category where the unique arrow is a trivial cofibration, it will be denoted by 0.
We conclude this section by introducing the notion of class of generating cofibrations for a cylinder category. It appears that this notion only depends on a small part of the structure of cylinder category and that it will be extremely useful in the rest of the paper to explicit this structre. For this reason we introduce immediately the following notion: 2.1.5. Definition : A cofibration category is a category C together with a class Cof C of maps called cofibrations such that: • isomorphisms are cofibrations and cofibrations are stable under composition.
• C has a initial object 0 and for all object X ∈ C the map O → X is a cofibration.
• Pushout of cofibrations exists and are cofibrations.
A morphism of cofibrations categories is a functor that send cofibrations to cofibrations and preserves the initial object and the pushout along cofibrations.
Obviously any cylinder category is a cofibration category when forgetting the weak equivalences. The dual notion, "fibration category", have also been called "tribe" by A.Joyal.
2.1.6. Definition : • If F is some class of maps in a category C one call a iterated pushout of maps in F a map which is a (finite) compositions of maps that are pushout of maps in F .
• An object is said to be an iterated pushout of maps in F if the map 0 → X is such an iterated pushout.
• If C is a cofibration category one say that F is a class of generating cofibrations if the cofibrations of C are exactly the iterated pushout of maps in F .
• A transfinite composition of iterated pushout will be called a transfinite iterated pushout.
For example, in the category of finite CW -complexes the inclusion of the (n−1)sphere into the n-ball for all n 0 form a set of generating cofibrations.
2.1.7. Proposition : Let C be a cofibration category with a set of generating cofibrations, a functor F : C → D to another cofibration category is a morphism if and only if: it preserves the initial object, it sends the generating cofibrations to cofibrations and it preserves pushout along generating cofibrations.

Proof :
Such a functor automatically send any pushout of a generating cofibrations to a pushout of a cofibrations. As all cofibrations in C are composite of pushout of generating cofibrations, F sends all cofibrations to cofibrations. A pushout along a pushout of a generating cofibration is also a pushout along a generating cofibration, hence these pushout are preserved by F . A general pushout along a cofibration is obtained as a series of such pushout so they are also preserved by F and this concludes the proof.

Homotopy category and generality on cylinder categories
In this subsection, we review for completeness the basic theory of cylinder categories and the construction of the homotopy category. All the material here originally comes from [7] and [9] except for some proof that have been slightly improved.
2.2.1. Proposition : Any morphism in a cylinder category can be factored as a cofibration followed by a weak equivalence. More precisely, any morphism in a cylinder category can be factored as a cofibration followed by a retract of a trivial cofibration.
This results and the proof that follows are due to K.Brown [9].

Proof :
Let F : A → B be a morphism in C a cylinder category, we form the co-product P = IA A B for IA some cylinder object A. P can be alternatively written as the pushout: In particular, the map A B ֒→ P is a cofibration, and hence one has a cofibration A ֒→ P , the map B ֒→ P is a trivial cofibration because it is a pushout of A ֒→ IA. There is a map from P to B which is IA → A → B on IA, the identity on B, this map is a retract of the trivial cofibration B ֒→ O (hence a weak equivalence by 2-out-of-3), and this form the factorization A ֒→ P ∼ → B claimed in the proposition.

Corollary :
• Any weak equivalence factors as a trivial cofibration followed by a retract of a trivial cofibration.
• Any functor between cylinder categories that send trivial cofibrations to trivial cofibrations also send weak equivalences to weak equivalences.
• A pushout of a weak equivalence along a cofibration is again a weak equivalence.
Note that as pushout of cofibrations exist and are cofibrations, saying that "any pushout of a weak equivalence along a cofibration is a weak equivalence" also means that if f : A → B is a weak equivalence between two objects under an object C and f : C → C ′ is a cofibration then the map induced by f , Proof : If f is a weak equivalence, then as any map, it can be factored as a cofibration followed by a retract of a trivial cofibration, but, by 2-out-of-3 the first cofibration will be a trivial cofibration. Any functor that preserves trivial cofibrations will send this factorization to a factorization as a trivial cofibration followed by a retract of a trivial cofibration, hence to a factorization into two weak equivalences and hence to a weak equivalence. The same argument applies to pushout along cofibration: pushout of trivial cofibrations are again trivial cofibrations by the fifth axiom of cylinder categories and the pushout of a retract of a trivial cofibration is again a retract of a trivial cofibration.

2.2.3.
Corollary : Let C be a cylinder category. Let A be an object of C.
Then the category C(A) of cofibrations A ֒→ B (with commutative triangle as morphisms) is a cylinder category with weak equivalences (resp. cofibrations) being the arrow that are weak equivalences (resp. cofibrations) in C.

Proof :
All the axioms about pushout, 2-out-of-6, isomorphisms, stability under compositions, and the map 0 → X being cofibrations are trivial. The existence of retract for trivial cofibration follow from the fact that a retraction of a map under an object A is automatically also under A. The only non trivial axiom is the existence of cylinder object, but a cylinder object for A ֒→ B ∈ C(A) is obtained simply by taking a factorisation in C as a cofibration followed by a weak equivalence of the map B A B → B.

Definition : If
A ֒→ B is a cofibration in a cylinder category, a relative cylinder object for B (relative to A or under A) is an object I A B such that one has a cofibration/weak equivalence factorization: This is the same as a cylinder object for B in the cylinder category C(A).

If
A and B are two objects of a cylinder category C, and if v : A → B is any morphism in C, then one has a pushout functor: 2.2.6. Lemma : If in a cylinder category C one has a square: where the left vertical arrow is a cofibration and the right vertical arrow is a weak equivalence, then there exists a map B → C which makes the upper triangle:

commutes.
Proof : We form the pushout P := B A C, let k : P → D the natural map and we factors k as a cofibration followed by a weak equivalence: By 2-out-of-3 the cofibration C ֒→ X is a weak equivalence, hence a trivial cofibration and hence admit a retraction. Composing this retraction with the map from B to X produces the map whose existence is claimed in the lemma.

2.2.7.
Definition : • If f, g : X ⇒ Y are two parallel maps in a cylinder category, one says that f is homotopic to g and one writes f ∼ g if the map (f, g) : X X → Y can be extended to a map IX → Y from some cylinder object, such an extension is called an homotopy between f and g.
• If i : A ֒→ X is a cofibration, and f, g : X ⇒ Y are two parallel maps such that f • i = g • i one says that f is homotopic to g relative to A and one writes f ∼ A g if the map: (f, g) : X A X → Y can be extended to a map I A X → Y for some relative cylinder object, such an extension is called an homotopy between f and g relative to A.

Proposition :
1. The notion of (relative) homotopy between maps does not depends on the choice of the (relative) cylinder object.
2. Homotopy and relative homotopy are equivalence relations.
3. If A ֒→ B is a trivial cofibration, any two maps from B to X which agrees on A are homotopy equivalent relative to A.

Homotopy and relative homotopy are compatible with post-compositon in
the sense that if f ∼ (A) g then u • f ∼ (A) u • g for any u such that the composition exists.

The homotopy relation is compatible with pre-composition as well, the relative homotopy relation is compatible with pre-composition in the sense that:
if one has a square: v whose vertical arrows are cofibrations, two morphisms f, g : B ⇒ X which agree on A, and such that f Proof : 1. Let I A X and I ′ A X be two (relative) cylinder objects, then considering the square: One has by lemma 2.2.6 a map I ′ A X → I A X under X A X showing that the homotopy relation in the sense of I A X implies the homotopy relation in the sense of I ′ A X and (as it is symmetric) that they are equivalent. 2. The fact that the homotopy relation is reflexive follows from the fact that the codiagonal map can be extended to a map IX → X by definition of IX. The symmetry follows from the same argument as the point 1.
with I ′ A X being I A X with the two maps X ֒→ I A X exchanged. For the transitivity, if f ∼ A g ∼ A h then one has a map: I A X X I A X → Y attesting those two homotopy, but if one consider the diagram: where the first horizontal map corresponds to the two map X → I A X that are not used in the formation of the coproduct I A X X I A X, then the diagonal map composed with the map to Y produces an homotopy between f and h. 4. An homotopy between two maps is just a map I A B → X hence it can be post-composed with any map.

If
5. It is enough to prove the relative case, the other case follow by taking A = A ′ = 0.
One can then consider the diagram: any diagonal map making the upper triangle commutes composed with the map to X produces the desired homotopy.
2.2.9. Proposition : If in a cylinder category C one has a square: where the left vertical arrow is a cofibration and the right vertical arrow is a weak equivalence, then there exists a map B → C which makes the upper triangle commutes and the lower triangle commute up to homotopy relative to A.
This proposition is due to I.Moerdijk and B.Van den Berg, it can be found in [7] with a different proof.

Proof :
We use the same construction as in the proof of lemma, one gets a diagram: By 2-out-of-3 the cofibration c • j : C ֒→ X is a weak equivalence, hence a trivial cofibration and hence admit a retraction r. One has r • c • j = Id C and by proposition 2.2.8 (3.) one has: c • j • r ∼ C Id X . The map we are trying to construct is r • c • k : C → B, the fact that r • c • j = Id C gives the commutation of the upper triangle, and the fact that c•j •r ∼ C Id X together with proposition 2.2.8 (5.) and (4.) gives the commutation of the lower triangle up to homotopy relative to A.

2.2.10.
Proposition : If C is a cylinder category, then there is a category hC whose objects are the objects of C and whose arrows are the equivalence class of arrows in C for the homotopy relation. Moreover hC is the localization of C at weak equivalences, for the natural quotient functor C → hC.

Proof :
The fact that hC is well defined and form a category follows directly from proposition 2.2.8.
Trivial cofibrations in C are send to isomorphisms in hC: any trivial cofibration j : A ֒→ B admit a retraction r, hence one has r • j = Id A and j • r ∼ A Id B because of proposition 2.2.8 (3.), which implies that j • r ∼ B (it follows from 2.2.8 (5.)) hence in hC, r is an inverse for j. As any weak equivalence in C is the composite of a trivial cofibration followed by a retract of a trivial cofibration it implies that any weak equivalences in C is an isomorphism in hC.
If F : C → D is any functor which send weak equivalences to isomorphisms, then for any object X, the map IX → X is sent to an isomorphism, as the two maps X ⇒ IX are section of this map their images are equal in D, and hence any pair of maps that are homotopic in C have equal images in D, hence the functor from C to D can be factored (essentially uniquely) into hC and this concludes the proof.

Proposition : A morphism in C is a weak equivalence if and only if its image in hC is an isomorphisms.
Note that the proof of this proposition will be the first place were we use the 2-out-of-6 property (and not just the 2-out-of-3 property). If one starts with a category that satisfies all the axioms of a cylinder category except the 2-out-of-6 property which is replaced by the 2-out-of-3 property, then one can still construct the category hC without problems. But the present proposition become equivalent to the 2-out-of-6 property and if one call "homotopy equivalences" the maps that are invertible in hC then this endows C with a new structure of cylinder category (satisfying the 2-out-of-6 property) which is minimal for the 2-out-of-6 property and still defines the same homotopy relation and the same homotopy category. We learned this remarks from [22, section 7.2] and it is apparently due to D-C.Cisinski.

Proof :
A map f : X → Y in C is invertible in hC if and only if there exists a map g : Y → X together with homotopies f • g ∼ Id Y and g ∼ f ∼ Id X . A map homotopic to a weak equivalence is a weak equivalence: indeed if one has a homotopy a ∼ b : IX → Y with b a weak equivalence then as b is the composite X ∼ ֒→ IX → Y , the map IX → Y is a weak equivalence by the property 2-outof-3 and hence a is an equivalence as a composite of weak equivalences. Hence in our initial situation, f • g and g • f are weak equivalences, and hence f and g are also weak equivalences by the 2-out-of-6 property.
The following proposition is often called the gluing lemma or the cube lemma: 2.2.12. Proposition : In a cylinder category, if one has a diagram of the form: Then the comparison map: is also a weak equivalence.
This results is well known for model category. We learned that it is true in weaker context from [22, Lemma 1.4.1]. Our proof is slightly different from the one given in this reference.

Proof :
We first fact f into a cofiration followed by a weak equivalence: And we factor f ′ into the pushout D ′ := A ′ A D: The map D → D ′ is a weak equivalence because it is a pushout of a weak equivalence along a cofibration (corollary 2.2.2) and the map D ′ → C ′ is a weak equivalence by 2-out-of-3.
In particular one obtains a square: where the two horizontal arrows are weak equivalences because they are both pushout of a weak equivalence along a cofibration (2.2.2). Hence it is enough to prove that the left most arrow is a weak equivalence, but as D ′ = D A A ′ , this leftmost map is in fact isomorphic to the map: Hence the result follows from the fact that A ֒→ D is a cofibration and B → B ′ is a weak equivalence (by a third application of corollary 2.2.2).

Acyclic morphisms of cylinder categories
Results in this sub-section are new, but very similar results where already known for Brown categories of fibrant objects and are due to D-C.Cisinski in [11] (For example theorem 3.19).
2.3.1. Definition : A morphism F : C → D between cylinder categories is said to be: • Homotopy surjective if for every object D in D there exists an object C in C and a weak equivalence D → F (C) (or equivalently F (C) → D). Equivalently, F is homotopy surjective if F : hC → hD is essentially surjective.
• Homotopy fully faithful if for any cofibration i : A ֒→ B in C, for any arrow x : A → X and any triangle: Is exactly the same as finding a retraction to the cofibration: Moreover, an homotopy relative to A between two such dashed arrow is the same as a factorization: is a relative cylinder object for X ֒→ X A B hence this is exactly the same as a homotopy relative to X of the two retractions. Hence this proves the lemma.

Proof :
Unfolding the construction of hC(A) and hD(A) in the condition 2., show that it is equivalent to the definition 2.3.1 of "homotopy fully faithful" in the special case where the horizontal map A → X is a cofibration: Indeed, they both says that for all object B and X for C(A) if there is a map between them in hD then it is homotopy equivalent relative to F (A) to a map in C(A). But because of the lemma 2.3.2, it is enough to check the definition of homotopy fully faithful when A → X is the identity, hence in particular a cofibration. Hence conditions 1. and 2. are equivalent.
Using condition 2. one see that being homotopy fully faithful is stable under co-slice, hence these conditions are also equivalent to condition 3..
In order to prove that they are also equivalent to condition 4. we just need to prove that if F is homotopy fully faithful then hF is faithful, but this follow immediately from the definition of homotopy fully faithful applied to: Indeed, if v and v ′ (two maps in C) are homotopy equivalent in D (hence equal in hD), then there is such a dashed arrow in D, hence it can be lifted to D and hence v and v ′ are homotopy equivalent in C (hence equal in hC).

2.3.4.
Proposition : For a morphism F : C → D of cylinder categories, the following conditions are equivalent: 1. F is acyclic.
2. F detect weak equivalences 6 and for all object A of C the functor F A : C(A) → D(F (A)) is homotopy surjective.
3. The functor hF : hC → hD is an equivalence of category. 4. For all object A of C, the functor: hF A : hC(A) → hD(F (A)) is an equivalence of category.

Proof :
We start with 3. ⇒ 2. If hF is an equivalence of categories, it in particular detect isomorphisms, but as weak equivalences are exactly the isomorphisms of the homotopy category, this implies that F detect weak equivalences. So we need to prove that F A is homotopy surjective. Let F (A) ֒→ B be an object of D(F (A)). As hF is essentially surjective, there exists an object B ′ of C such that F (B ′ ) is weakly equivalent to B. One can form in hD a triangle: which hence is a triangle in D that commutes up to homotopy. Moreover, as hF is fully faithfull The map F (A) → F (B) can be freely assumed to be a map of the form F (v), and by replacing this v be a cofibration/weak equivalence factorization, one can moreover assume that v is a cofibration (by changing the object B ′ ). Rewriting this diagram, by explicitly writing the homotopy that makes it commute on gets: Then, forming the pushout P = B ′ A IA one gets a diagram: The map F (A) i1 ֒→ F (IA) → F (P ) is a cofibration of the form F ( ) and the map from F (P ) to B is a weak equivalence by 2-out-of-3, hence one has constructed an object A ֒→ P in C such that F (P ) is homotopy equivalent to B in D(A) which concludes the proof of this implication.
We now prove that 2. ⇒ 1.. We only need to proves that F is homotopy fully faithful. We will use the criterion in Lemma 2.3.2. Let i : A ֒→ B a cofibration in C and assume that it has a retraction r : F (B) → F (A) in D. We consider a cofibration/weak equivalences factorization of r in order to a get a factorization of the identity of F (A) as: As F B is homotopy surjective, there exists a cofibration j : B ֒→ C ′ such that one has a diagram: In particular F (j) • F (i) is a weak equivalence in D and, as F detect weak equivalences, j •i is a trivial cofibration, hence it admit a retraction r ′ : C ′ → A. This already produces a retraction r ′′ = r • j : B → A of i in C, in order to conclude one need to show that F (r ′′ ) is homotopy equivalent to r relative to A. But in D, F (j • i) already has a retraction r ′′′ obtained by composing (in the above diagram) the equivalence λ : Proof : We will use characterization 2. of proposition 2.3.4. For each object of C(A) there is a weak equivalence from X to v ♯ (X) given by the pushout defining v ♯ hence v ♯ detect weak equivalences. As functors of the form (v ♯ ) X corresponds to w ♯ for w the pushout of v along the cofibration A ֒→ X, it is enough to prove that v ♯ is homotopy full. For any object B ֒→ X of C(B), a factorization as cofibration followed by a weak equivalence of A → B ֒→ X produces an object of C(A) which will be sent to an object homotopy equivalent to X in C(B) hence this concludes the proof of the first implication.
Proof : This follows from characterization 3. in proposition 2.3.4 and the fact that equivalences of categories satisfies this condition.

Completion of cylinder category in semi-model categories
In this section we show how a small cylinder category can be naturally completed into a semi-Model category. In ∞-categorical therms, this construction corresponds to freely adding direct co-limit to a finitely co-complete small (∞, 1)-category in order to turn it into a co-complete (∞, 1)-category, and this is usually done by looking at the category of presheaves sending finite co-limit to finite projective limits.

2.4.1.
Definition : Let C be a small cofibration category, we denote by C the category of presheaves over C that send the initial object to the singleton and pushout along cofibrations to pullback of sets.
As C is small, C is locally presentable category, in particular it is complete and co-complete. In fact C can be described as the category of models of some finite limits sketches (as in [4, chapter 4]) which are equivalent to the "Partial Horn theory" or the "quasi-equational theory" of [21], i.e. it is algebraic in some sense. Moreover, limits and directed colimits in C are computed "objectwise" (i.e. as limits and directed colimits of presheaves), finite (non directed) colimits are considerably harder to compute. For any cofibration category C, the (covariant) Yoneda embeddings of C takes values in C and C will always be identified with its image though the Yoneda embeddings C →C.

Definition : If F : C → D is a morphism between two cofibrations categories, we denote by R F :D →C the functor of restriction along F and byF its left adjoint (the left Kan extension of F ).
F is always an extension of F when C is identified with the image of the Yoneda embeddings C → C.
Completion of small cofibrations categories comes with a notion of cofibration and even a weak factorization system:

2.4.2.
Definition : An arrow f in C will be called: • A trivial fibration if it has the right lifting property with respect to all cofibrations in C.
• A finite cellular map if it is a iterated pushout of cofibrations in C.
• A cellular map if it is a transfinite iterated pushout of cofibrations in C.
• A cofibration if it is a retract of a cellular map.
By the small object argument, and because C is assumed to be small, every arrow in C can be factored as a cellular map followed by a trivial fibration and cofibrations are exactly the maps which have the left lifting properties with respect to all trivial fibrations. Cofibrations and trivial fibrations form a weak factorization system. Moreover it is easy to see that an object X of C is in C if and only if the map 0 → X is a finite cellular map. Note that unless we require C to be Cauchy complete 8 and that cofibrations of C are stable under retract cofibrations in C might be different from cofibrations in C: cofibrations in C corresponds in C to finite cellular map between representable objects and they are in particular cofibrations in C.

2.4.3.
Lemma : Every cellular objects inC, i.e. objects X such that the map 0 → X is cellular, can be written as a directed co-limit of representable such that all the transition map are cofibrations in C (i.e. finite cellular maps).

Proof :
Let X be a cellular object, it means that X can be written as the colimit of a sequence of objects X α induced by an ordinal ρ such that for each limit ordinal α < ρ, X α is the colimit of the X β for β < α and for each successor ordinal α + , X α + is obtained from X α as a pushout: We will prove by induction on α that X α is a directed colimit as claimed in the lemma, and that moreover the map X α ′ → X α for α ′ < α corresponds to an enlargement of the category indexing this colimits. The case α = 0 is tautological (with X 0 = 0 ). If α is a limit ordinal then the result is also easy: one just need to take the increasing union of all the indexing categories of all the colimit of the X α ′ for α ′ < α. Assume the result holds for X α , i.e. X α = lim i∈I X i where I is a direct category, the X i are in C and the transition map between the X i are cofibrations in C. We will write X for X α and X + for X α + . As directed colimit inC are computed object wise, the map A → X defining X + = X A B factors into one of the X i . Let us consider the following diagram: it has two type of objects: the X i for i ∈ I and the Y a,i for i ∈ I and a : A → X i an arrow inducing the correct map from A to X. The object Y a,i will be sent to X i A B, morphisms from X i to X j stay the same as in the original diagram, there is no morphisms from Y i,a to X j , morphisms from X i to Y j,a are the morphisms from X i to X j in the original diagram and morphisms from Y i,a to Y j,a ′ are the morphisms from X i to X j in the original diagram that are compatible to the maps from A (in C) and hence induces a cofibration from It is a routine check to see that this is a directed diagram and that its colimit is indeed X + (for example by checking the universal property) and this concludes the proof.

Definition :
If C is a cylinder category, a morphism f : X → Y inC is called: • A fibration if it has the right lifting properties with respect to all trivial cofibrations in C.
• A trivial cofibration if it has the left lifting property with respect to all fibrations.
• A weak equivalence if if for every square: where i : A ֒→ B is a cofibration in C, there exists applications a : B → X and h : I A B → Y for some relative cylinder object I A B which extend the above square into the following commutative diagram: By the small object argument, every arrow can be factored as a trivial cofibration followed by a fibration, and trivial cofibrations are exactly the retract of transfinite iterated pushout of trivial cofibrations in C.
The filling condition in the definition of weak equivalence means that a is a diagonal filler: Where the upper triangle is commutative and the lower triangle commute up to the homotopy h relative to A. In particular, weak equivalences in C are weak equivalences in C by proposition 2.2.9. The converse is also true and will be proved in 2.4.12.

Lemma : The existence of a filling as in the definition of weak equivalences 2.4.4 does not depends on the choice of the relative cylinder object I A B.
Proof : It follows from the fact that any two cylinder objects I A B and I ′ A B are connected by maps compatible to the cofibrations from B A B.
2.4.6. Proposition : Trivial fibrations in C are exactly the fibrations that are also weak equivalences.

Proof :
A trivial fibration is obviously a fibration, and satisfies the lifting condition defining weak equivalences (2.4.4) striclty (not up to homotopy) hence is a weak equivalence. Conversely, if f is both a weak equivalence and a fibration, then for any square: one can first use that f is a weak equivalence to obtain the arrow a and h and then that f is a fibration and B ֒→ I A B is a trivial cofibration to obtain the arrow b in the following commutative diagram: In order to study properties of weak equivalences it will be convenient to introduce the following definition.

Definition : Let X be an object inC, i : A ֒→ B a cofibration in C and
x : A → X a morphism, then one defines: Where ∼ A is the homotopy relation 9 relative to A. A morphism f : X → X ′ induces a map: Lemma : The extension of ∼ A above is indeed an equivalence relation and does not depends on the choice of a relative cylinder object I A B.

Proof :
The proof is exactly the same as the proof given in 2.2.8 that in a cylinder category the relative homotopy relation is an equivalence relation and does not depend on the choice of the relative cylinder object.

Proposition :
For a morphism f : X → X ′ the following conditions are equivalent: 1. For all cofibrations A ֒→ B in C, and all x : A → X, the map: is bijective.
2. for all cofibration A ֒→ B in C, and all x : A → X, the map: is surjective.

f is a weak equivalence in the sense of definition 2.4.4.
Proof : the implication 1. ⇒ 2. is tautological. The equivalence between 2. an 3. is relatively easy: A square: gives an element v of π B/A (X ′ , f (x)) (and every element corresponds to such a square) and a filing as in definition of weak equivalences in 2.4.4 is exactly the data of map B → X that would make the upper triangle commutes and the lower triangle commutes up to an homotopy relative to A, i.e. an element of π B/A (X, x) whose image by f is v. Hence the claim that such a filling exists is exactly the claim that π B/A (f, x) is surjective. It remains to prove that 3. ⇒ 1.. Assume that f is a weak equivalence. We just need to prove that hence one has a square: Using that f is a weak equivalence one gets a commutative triangle: which proves that u = v in π B/A (X, x) and hence concludes the proof.
2.4.9. Proposition : is a contravariant functor from C(A) to Sets which send weak equivalences to isomorphisms, in particular it factor as a functor on hC(A).
is a bijection.
• If one has a commutative square: where either f and g are weak equivalences, or the map B A A ′ → B ′ is a weak equivalence, then for any x : A ′ → X in C one has a bijection: Moreover all the construction done here are functorial in X in the appropriate sense.
Proof : • The functoriality follows from the fact that the (extended) relative homotopy relation is stable under precomposition (same proof as in proposition 2.2.8) and the proof that weak equivalences induce bijections is essentially the same as the proof of the fact that weak equivalences in C are bijections in hC given in the proof of proposition 2.2.10. Functoriality in X is also immediate.
• A map from B ′ to X extending the map from A ′ to X is, because of the universal property of the pushout, the same as a map from B to X extending the map from A to X. Moreover as A ′ A I A B can be used as a relative cylinder object for A ′ ֒→ B ′ the homotopy relation is the same in the two descriptions, hence one has the bijection. Once again the functoriality in X is clear.
• If f and g are weak equivalences then the 2-out-of-3 property implies that the comparison map from the pushout to B ′ is a weak equivalence, the result follows then from the conjunction of the two points above.
2.4.10. Corollary : If x, x ′ : A ⇒ X are two arrows, and h : IA → X is an homotopy between x and x ′ then there is a bijection: Moreover, if f : X → Y is a morphism inC the square:

commutes.
In particular, in order to test whether a map f : X → X ′ is a weak equivalence, we only need to test that the maps π B/A (f, x) are surjective for one x in each homotopy class of map x : A → X.

Proof :
We choose a factorization as cofibration followed by a weak equivalence: IB is indeed a cylinder object for B and one has a diagram of cofibrations: Applying the construction of 2.4.9, if h is an homotopy between two morphism x, x ′ : A ⇒ X one gets two isomorphisms: There composite give us the transport map h * we are looking for. The compatibility with transport along a map f : X → X ′ follow from the compatibility of the construction explained in 2.4.9.
2.4.11. Corollary : Weak equivalences inC satisfies the 2-out-of-3 condition. Proof : → Z be two composable arrows inC. if f and g are weak equivalences or if g • f and g are weak equivalences, then the third map also is because of the characterizations 1. of weak equivalences in proposition 2.4.8. The last case need a little more care: if g • f and f are weak equivalences, then, by the same argument, one can conclude that for all A ֒→ B and for all Hence, by 2.4.10 this proves that g is a weak equivalence and concludes the proof.

Proof :
We already saw that a weak equivalence in C is a weak equivalence in C (this is basically proposition 2.2.9). For the converse, using the cofibration/weak equivalence factorization in C and the 2-out-of-3 property for weak equivalences in C it is enough to prove the result for cofibrations in C. Let i : A ֒→ B be a cofibration in C which is a weak equivalence in C, then using that π B/A (i, Id A ) is surjective one can find a retraction p : B → A such that i • p is homotopy equivalent to Id B relative to A, but an inverse of i on hC hence by proposition 2.2.11 this proves that i is a weak equivalence and concludes the proof.

Proposition : If f : X → Y is an arrow inC with a cofibrant domain then f is a trivial cofibration if and only if it is a cofibration and a weak equivalence.
Proof : Let X be a cofibrant object, and let x : C → X be an arrow with C ∈ C, and C ∼ ֒→ D be a trivial cofibration in C. Let X + be the pushout X C D. We will first prove that the natural map X → X + is a weak equivalence. Consider a square: By assumption X is retract of a cellular object X ′ which is a directed co-limit of representable objects X i (with cofibrant transition map), the map from C → X lifts to a map C → X ′ and one defines X ′+ = X ′ C D, and X + is easily seen to be a retract of X ′+ , in particular, one can lift all the above square to X ′ and X ′+ X + 0 can then be represented by a colimits of X i C D restricted to the X i with a map from C compatible to the map to X 0 , and hence using again that directed colimit are computed objectwise, there exists a representable X i with a map X i → X such that the above square is lifted to: But as the map X i → X i C D is a trivial cofibration in C one has the lifting we are looking for directly in the first square by proposition 2.2.9. Moreover, because of the characterization of weak equivalence in terms of the π-sets (2.4.8) and the fact that the π-sets clearly commutes to directed colimits one directly see that a transfinite composition of weak equivalences is a weak equivalences and that a retract of a weak equivalence is a weak equivalence. Hence this show that every trivial cofibration of cofibrant domain is a weak equivalences.
Conversely, let f : X → Y be a cofibration with a cofibrant domain which is a weak equivalence. One can factor f as a trivial cofibration followed by a fibration, but the trivial cofibration part will be a weak equivalences by the above result and hence by the 2-out-of-3 property the fibration part will be a weak equivalence, hence a trivial fibration. Using the left lifting property of f (a cofibration) against this trivial fibration exhibit f as a retract of a trivial cofibration which concludes the proof.

Any left Quillen functorC → V is obtained this way.
Proof : The fact that one gets an adjunction which extend F , and the fact that any such functor is obtained this way is basic Kan extension theory (it only require V to be co-complete). Moreover, any suchF send the generating (trivial) cofibrations inC to (trivial) cofibrations in V by definition hence is a left Quillen functor.
2.4.16. Proposition : Let F : C → D be a morphism of cylinder categories Then: 1. For every object Y ofD, every cofibration A ֒→ B in C and every y : induced by the adjunction is a bijection.
2. If F is homotopy fully faithful then, for every cofibrant object X ofC, for every A ֒→ B a cofibration in C, and for every x : A → X, the natural map: induced by applyingF is a bijection.

If F is acyclic, then the Quillen pair (F , R F ) is a Quillen equivalence.
Proof : is the same as a homotopy F (I A B) → Y so the first point follows immediately.
2. The map is clearly well defined: any homotopy I A B → X will produces a homotopy F (I A B) →F (X) by applyingF .
Fix x : A → X and let v : F (B) →F (X) be any morphism inD which represents an element of π F (B)/F (A) (F (X),F (x)) . Being cofibrant, X can be written as (a retract of) a directed colimit of representable, andF commutes to colimit, so there exists a representable object X i → X such that v can be factored as: Applying the fact that F is homotopy fully faithful, one can find a re- This proves the surjectivity of this comparison map.
The exact same argument applied to B A B ֒→ I A B instead of A ֒→ B proves the injectivity.
3. Let X be a cofibrant object inC and Y be any object in D, let v : X → R F (Y ) with adjoint transpose: w :F (X) → Y . We need to prove that v is a weak equivalence if and only if w is. From the previous two points it is easy to see that v is a weak equivalence if and only if for every A ֒→ B, for every x : A → X the application: is a bijection. We need to show that this is enough to conclude that w is a weak equivalence.
First applying the second point to 0 ֒→ A one can see that any arrow F (A) →F (X) is homotopy equivalent to an arrow of the formF (x) so by 2.4.10 this shows that the above map is again a bijection whenF (x) is replaced with any map from F (A) toF (X), and finally, using that F is acyclic, one can construct for any cofibration i : A ′ ֒→ B ′ in D a square of the form: where the horizontal arrows are weak equivalences and using 2.4.9, this concludes the proof.
2.4.17. Let us mention an example: If C is the category of finite CW -complexes then C can be difficult to describe explicitly. But the full subcategory of cellular objects is equivalent to the category of CW -complexes: indeed, this follows from lemma 2.4.3 and the fact that a map from a finite CW -complex to an arbitrary CW -complex always factor into a finite sub-CW -complex by a compactness argument. As the general cofibrant objects are the retract of cellular objects, the full subcategory of cofibrant objects is equivalent to the category of retract of CW -complexes, i.e. of topological spaces which are cofibrant from the model structure on the category of spaces. Moreover it is immediate that the weak equivalences, cofibrations and fibrations between them are the same as in the category of spaces. It follows from that that the Quillen adjunction C ⇄ Spaces induced by the inclusion of C in Spaces is a Quillen equivalence: it induces a categorical equivalence between the categories of fibrant-cofibrant objects which preserves weak equivalences, fibrations and cofibrations.
In particular, one has that: 2.4.18. Proposition : If C is a cylinder category with an acyclic morphism to the cylinder category of finite CW -complexes, then the induced adjunction between C and the model category of spaces is a Quillen equivalence.
Finally, in the case where the category C comes with a class of generating cofibrations, one can use it to obtains smaller set of generating cofibrations and trivial cofibrations in C.

2.4.19.
Proposition : Let C be a cylinder category with a set A ֒→ B of generating cofibrations. Then for a map f : X → Y in C: • f is a trivial fibration if and only it has the right lifting property with respect to the generating cofibrations.
• f is a weak equivalence if and only if all A ֒→ B a generating cofibration, the maps π B/A (f, where A ֒→ B is a generating cofibration can be filled into: Proof : • The first claim is relatively immediate: Any cofibration in C is a composite of pushout of the generating cofibrations, so something that has the right lifting property with respect to generating cofibrations has the right lifting property with respect to all cofibrations.
• First take a cofibrant replacement X of the domain of X the map X → X satisfies the same condition as f because the map X → X preserves all π-sets. Hence one can freely assume that X is cofibrant. Then consider a trivial cofibration/fibration factorization of f , as the domain of f is cofibrant, the trivial cofibration part of the factorization is an equivalence hence by the exact same argument as in the proof of 2.4.11, the fibration part satisfies the same condition as f . But this is enough to make the proof of 2.4.6 shows that this fibration has the right lifting property with respect to all generating cofibrations hence is a trivial fibration, hence a weak equivalence and this concludes the proof.
• Let f be a trivial cofibration with cofibrant domain. Using the small object argument, one can factor f as p • i where i is in the class generated by maps of the form B ֒→ I A B and p has the right lifting property against those maps. Both f and i are weak equivalences, hence p is also a weak equivalence. Under those conditions, the proof of 2.4.6 shows that p is a trivial fibration. By the usual arguement on weak factorization systems, this suffices to prove that f is a retract of i and hence that the lifting property of fibrations can be tested against only the maps that we have used in the construction of i, i.e. o the form B ֒→ I A B.
One can also gives a longer proof (but more informative) of the last point by proving that any trivial cofibration C ֒→ D in C is a retract of D ֒→ I C D and if a cofibration C ֒→ D is obtained as n pushout of generatng cofibration A i ֒→ B i , the trivial cofibration D ֒→ I C D can be obtained as n pushout of of the trivial cofibrations B i ֒→ I Ai B i .

Pre-cylinder categories and their algebraic properties
We will now define and studies pre-cylinder categories, this notion corresponds roughly to the algebraic structure underlying the notion of cylinder categories, i.e. the part of the structure that is preserve by morphisms and subject to free constructions. In the next section we will construct a sort of weak model structure on the category of pre-cylinder categories such that the cylinder categories are exactly the fibrant objects. Of course we will call "trivial cofibrations" the maps that both cofibrations and weak equivalences.

Definition and generalities
The idea behind this definition is to isolate the "algebraic part" in the notion of cylinder category. In fact, up to some problem related to the fact that those are not ordinary category but a 2-category, the category of pre-cylinder categories and the category of cofibrations categories would be category of models of a quasi-equational theory or partial Horn theory as in [21] (for a correct 2categorical version of this) and hence should have all limits, all co-limits and all the free constructions that we might want. Those free constructions will be discussed more precisely in the next subsection 3.2.
Note that the "cube lemma" immediately implies some properties the we have for cylinder categories: 3.1.2. Proposition : In a pre-cylinder category, a pushout of a trivial cofibration is a trivial cofibration, a pushout of a weak equivalence along a cofibration is a weak equivalence.
Proof : The proposition is rather immediate to check: those trivially satisfies the cube axiom and the 2-out-of-6 property, and they do have the correct universal property to define adjoint functors. This proposition has a very interesting consequences: Computing limits, co-limit or free construction in the category of pre-cylinder category or in the category of cofibrations category would be essentially the same: the forgetful functor will preserve all sort of limits and co-limits, so when one wants to compute this kind of categorical constructions in the category of pre-cylinder category one can do it by first computing it in the category of cofibration categories and then constructing the class of weak equivalences as the smallest or largest class (depending if one perform an inductive or projective construction) satisfying some conditions.
We will now give basic example of limits, co-limits and free construction before moving in the next subsection to a more general theory of free constructions (including colimits) in the category of pre-cylinder category.

Proposition :
The product of two pre-cylinder categories (or of two cofibration categories) exists and is their categorical product with the cofibrations (resp. the weak equivalences) being the maps whose two components are cofibrations (resp. weak equivalences). This extend to infinite products.

Proof :
It is easy to see that it is indeed a pre-cylinder category (or a cofibration category) and that it indeed satisfies the universal property.
3.1.5. Lemma : The functor 0 is always a morphism between any two precylinder categories (or cofibration categories). If F, G : C ⇒ D are two morphisms between pre-cyinder categories (or cofibrations category) then: is also a morphism.
Those two claims are immediate to check (the fact that the co-product preserve weak equivalences is a special case of the cube lemma).
3.1.6. Proposition : The co-product of two pre-cylinder categories (or cofibration categories) C and D is isomorphic to their product C ×D. The co-projections are the maps X → (X, 0) and X → (0, X). If f : C → X and g : D → X are two morphisms, then the corresponding morphism (f, g) : D × C → X is: This extend to finite co-product.
One could also form infinite co-products: it will be the full subcategory of the infinite product of objects which are initial on all component except a finite number, but this would follow from the more general theory developed in the next subsection.

Proof :
It is not very hard to check directly. It also follows from the lemma above by the exact same categorical argument as the fact that the co-product (if it exists) is always isomorphic to the product in an additive category (with the addition being replaced by the co-product).
3.1.7. Proposition : The free pre-cylinder category F * on one object * is (equivalent to) the category of finite sets, with the monomorphisms as cofibrations and the isomorphisms as weak equivalences. The object * being the singleton.

Proof :
It is easy to check that it is indeed a cylinder category. Moreover if C is any pre-cylinder category and X is an object of C, then one can form for S a finite set the iterated co-product of X: This defines a functor from finite sets to C, isomorphisms are sent to isomorphisms hence weak equivalences, injections are sent to the structural maps of a coproduct: X (S1) → X (S1) (S2) = X (S1) X (S2) hence a cofibration, and pushout along cofibration are preserved by this functor. Hence it is a morphism from F * to C which send the singleton to X and such a morphism is obviously unique (up to unique isomorphism)

Completion and computation of free pre-cylinder categories
The goal of this sub-section is to develop a general procedure to compute all co-limits and free constructions within the category of pre-cylnder categories and the category of cofibrations categories.
As observed in 3.1.3, the important part is to understand free constructions and colimits of cofibration categories. The case of pre-cylinder categories is then easily deduced from that by first making the construction at the level of cofibration categories and then just taking the smallest class of weak equivalences that makes the cofibration category obtained a pre-cylinder category and the structural morphisms, morphisms of pre-cylinder category.
The first step would be to precisely introduce the type of free constructions that one want to consider.
3.2.1. Definition : A system of generators for a cofibrations category is the data of: 1. A set of cofibrations categories (C i ) i∈I .

2.
A set J of indices for objects (X j ) j∈J .

A set
A of indices for arrows, to each indices for arrow is attached a "domain" and a "co-domain" which are formal co-product of a finite family of objects of the C i and/or of some of the X j . 4. A subset C of the arrows are "cofibrations".

A set of relations between the arrows.
A system of generators for a pre-cylinder category is the same except that: 1. The points 4. (4 ′ .) and 5. need to be clarified: we mean by a subset of arrows (W or C) a subset of the set of all arrow that can be constructed out the arrows of the category C i , the objects X j for j ∈ J and the arrows in A between finite coproducts of these objects. Similarly a relation between arrows is an equality between two such parallel arrows.
A reader which find this last paragraph unclear or not formal enough can follow a more precise approach: one first consider systems of generators with only the axioms 1, 1 ′ , 2, 3 and one defines the cofibration categories/pre-cylinder categories freely generated by such a system of generators (in the sense of the next definition). One can then return to the more general definition of system of generators: the point 4. asks for a subset of the sets of arrows of the category freely generated by the previous structure (points 1, 1 ′ , 2, 3), the set W is the same things, and the point 5 is a set of pairs of parallel arrows in this freely generated category.
Moreover, one can iterate this procedures in order to also ask some properties or relations between arrows that are constructed using pushout along maps that are cofibrations because they are forced to be by the the choice made in point 4.. But this does not need to be done at this level, it will be automatically covered by iterating free construction and everything that is discussed below will also apply to this situation.

Definition :
A representation of a system of generator for a cofibration category in a cofibration category D, is the data of: 2. an object X j ∈ D for each j ∈ J, 3. for each a ∈ A an arrow in D between the corresponding co-product, 4. the arrow in C are cofibrations, 5. the relations are satisfied.
A morphism between two representations is the data of natural transformations between the morphisms specified in point 1. and of morphisms between the object specified in point 2., such that it satisfies the naturality conditions with respect to all the arrows specified in points 3..
A cofibrations category freely generated by a system of generators is a cofibrations category C such that for any other cofibrations category D the category of morphisms from C to D is equivalent, functorially in D, to the category of representations in D of the system of generator.
One defines the same notions for pre-cylinder category, the only change is that in 1. one asks for morphisms of pre-cylinder categories and in 4. on also asks that the maps in W are weak equivalences in D.

3.2.3.
Proposition : For every system of generators, there is a essentially unique small cofibrations category/ pre-cylinder category generated by it.

Proof :
The uniqueness property is clear. The existence would basically follow from a 2-categorical version of theorem 29 of [21], as we do not know any reference developing this sort of result into a 2-categorical context we will use some trick to deduce it from the 1-categorical version. The proof for cofibrations categories and cylinder categories are exactly the same, we will only write it for cofibration categories.
Let us temporarily call a strict cofibration category to be a (small) cofibration category with a specified initial object and in which for every diagram of the form C ← A ֒→ B one has chosen a specific pushout C A B. A morphism between strict cofibration category is called strict if it preserves the marked initial object and the chosen pushout.
The (1-)category of strict cofibration categories and strict morphism is the category of models of quasi-equational theory (in the temrinology of [21]), which would have one sort for objects, one sort for morphisms, one predicate for "cofibrations". Hence, because of theorem 29 of [21] one can have models freely generated by a system of generator in the sense that one will have a strict cofibration category C such that strict morphisms from C to D are the same as representation of the system of generators in D.
We will now show that this C satisfies the correct universal property. The first observation is that for any (strict) cofibration category D, there is a (strict) cofibration category D mor whose objects are pair of objects of D together with a morphism between them (cofibrations are the object wise cofibrations) and a morphism from C to D mor is the same as a pair of morphisms from C to D together with a natural transformation between them. Hence morphism between two (strict) functors from C to D can be described as (strict) morphisms from C to D mor hence as representations of the system of generator in D mor and those are exactly the morphisms of representations as defined above. Hence the category of strict morphism from C to D and natural transformation between them is indeed what we want. Any morphism (possibly non strict) form C to D can be made strict by eventually replacing D by a equivalent cofibration category, so this concludes the proof.
The argument above is extremely inexplicit, and the rest of this subsection is devoted to present a more efficient construction to produce those free categories. As mentioned above it is enough to deal with the case of cofibration categories, one can then deal with weak equivalences separately. The key observation is the following: Proposition : Let Set op be the opposite of the category of sets, with every map being a cofibration. Then Set op is a cofibration category and for every cofibration category C, there is a natural equivalence: Proof : This is relatively immediate: Set op has all colimits because the category of sets has all limits, a morphism from C to Set op is hence exactly a contravariant functor from C to sets which takes the initial object to the singleton and a pushout along cofibration to pullback of sets, hence an object of C. The natural transformations between such morphisms corresponds to morphism of pre-sheaf in the opposite direction.
3.2.4. This proposition allow to very easily obtain a simple description of the completion D of the cofibration category D freely generated by a system of generators: it corresponds to a representation of the system of generator in Set op . More precesely: 1. For each i ∈ I, an object D i of C i .
2. for each j ∈ J a set D j .
3. For each arrow in A, an arrow in the other direction between the corresponding finite product.
4. Asking for some arrows to be a cofibrations (or a weak equivalence) does not have any influence at this level as every map in Set op is a cofibration.
5. All the relations between the arrows should be satisfied.
Morphisms being the obvious notion. Next, one needs to compute what are the functors C i → D and what are the objects of D corresponding to the X j . There is no formula for this, but they satisfy a universal property: • For any i ∈ I and for any c ∈ C i then there is an object f i (c) ∈ D such that functorially in D ∈ D one has: • For any j ∈ J there is an object X j in D such that functorially in D ∈ D: Hom(X j , D) ≃ D j Such objects always exist but there is in general no easy procedure to construct them and one need to find those objects "by hand" in each specific case. Although it appears that it is often easy and we will see some of examples in the rest of the article.
Using the universal property of these objects, one easily extend this into a functor f i : C i → D which send coproducts along cofibrations to coproducts, and all for all arrows in A one can construct a corresponding arrow between coproducts of the f i (c) and the X j . One can then say that maps in D is a generating cofibration, if it is: either coming from a (generating) cofibration in C i though the construction above, or from an arrow in C from the construction above, or it is the arrow 0 → X j for a j ∈ J. One then has: Proposition : • D is the full sub-category of D of objects which can be obtained from 0 as an iterated pushout of generating cofibrations.
• Cofibrations in D are the arrows that are iterated pushout of the generating cofibrations (i.e. the generating cofibrations are indeed generating cofibrations of D).

Proof :
Let us first observe that if we define D ′ to be the full subcategory of object which can be obtained as iterated pushout of generating cofibration and the cofibrations between objects of D ′ being the iterated pushout of generating cofibration, then D ′ is a cofibraton category: isomorphisms are cofibration, and cofibrations are stable under composition, pushout along cofibrations exists (and are computed in D). Moreover, any cofibrations in D ′ is also a cofibration in D (in the sense of definition 2.4.2). D ′ contains all the structure that generated D: the image of the f i the object f j and all the maps defined between them, moreover the maps f i : C i → D ′ are morphisms of cofibration categories and the maps in the set C are cofibration in C (because they are generating cofibration). Hence there is a morphism from D to D ′ preserving all these structure. But if one look at the composition of this morphism with the inclusion D ′ → D we obtain the Yoneda embeddings: indeed all the generators of D are send to their Yoneda embeddings and this is a morphism from D to the cofibration category of cofibrant object of D hence it is the Yoneda embeddings by the uniqueness in the universal property of D. This proves that D and D ′ are equivalent as category. Moreover, Their cofibrations are the same: any map which is a cofibration in D is also a cofibration inD ′ because the functor D → D ′ is a morphism of cofibration category, and any morphism which is a cofibration in D ′ is a cofibration in D because it is an iterated pushout of generating cofibrations and generating cofibration are cofibration in D.
We finish with a simple example of the construction above: 3.2.5. Proposition : The pre-cylinder category freely generated by a cofibration A ֒→ B between two objects is the category F ֒→ such that: • objects are pair of finites sets X A , X B with a map: • Morphisms are morphisms of diagrams.
Moreover, if A ֒→ B is a cofibration in a pre-cylinder category C, the corresponding morphism from F ֒→ to C send X B → X A to the object constructed by first taking the co-product of X A copies of A and then gluing X B copies of B along the copies of A corresponding to the image in X A by X c .

Proof :
The completion of F ֒→ is the category of pair of sets with a map between them and morphisms are morphisms of diagram. Checking the universal property, the object A is ∅ → { * } and B is { * } → { * } and the generating cofibrations are 10 the map from the initial object to A and the map from A to B. Hence the finite cellular maps are the map that are obtained by iteratively: freely adding an element to X A or freely adding an element of X B whose image in X A is specified, i.e. they are exactly the object wise "co-finite" monomorphisms, it follows that the object of F ֒→ are just the pair of finite set with a map, cofibrations are the objectwise monomorphism, and as nothing in the system of generators impose that certain arrow are weak equivalences, the weak equivalences are just is isomorphisms.
The last claim just translate that the morphism will preserve co-product along cofibrations.

The monoidal closed structure on the category of precylinder categories
Both the category of pre-cylinder categories and of categories with cofibrations have a very natural structure of symmetric monoidal closed category. We will explain it only of pre-cylinder categories, but everything carries over easly to the case of cofibrations categories by just forgetting everything concerning the weak equivalences. We will start by describing the "Hom object".
3.3.1. Proposition : Let C and D be pre-cylinder category, there is a precylinder category [C, D] such that: • Objects are the morphisms from C to D.
• Morphisms are the natural transformations.
• Weak equivalences are the objectwise weak equivalences.
• Cofibrations are the natural transformations λ : F → G such that for any cofibration c : A ֒→ B in C, the arrow: induced by the naturality square (for λ and c) is a cofibration.
Proof : Remark first that cofibrations are in particular objectwise cofibrations : this can be seen by considering the case of the cofibration 0 ֒→ A in C, which gives that F (A) ֒→ G(A) is a cofibration for all A.
Let i : A ֒→ B and f : A → C be a cofibration and an arrow in [C, D], as i is in particular an objectwise cofibration one can form the objectwise pushout out D = B A C which is a functor from C to D. We will first prove that it is a morphism of pre-cylinder categories: • D preserves cofibrations: let i : X ֒→ Y be a cofibration in C. Then: Is a cofibration because C(X) → C(Y ) is a cofibration.
The square: Is a pushout (this is easily observed by examining the universal properties) and the left map is a cofibration by assumption (because i is a cofibration) hence the right map is also a cofibration and this shows that D(i) is a cofibration.
• D preserves pushout along cofibrations because colimits commute to colimits (or by examining the universal property of all the pushout involved). By assumption, one has a cofibration: One can push it forward to a cofibration: and then compose it to the cofibration: and this concludes the proof.
Even when D is a cylinder category, it is relatively rare that [C, D] is a cylinder category. This makes this hom object a little more difficult to use in a correct homotopy theoretic fashion and will not study in the present paper the precise relationship between the monoidal structure and the weak model structure on the category of pre-cylinder category, but it is not hard too see that it is not a monoidal model structure. This being said, conditions on C under which [C, D] is a cylinder category when D is will be studied in subsection 4.2.

Proposition : A morphism λ : F → G in [C, D] is a cofibration if and only if for a class of generating cofibrations
induced by the naturality square is a cofibration.

Proof :
We will prove by induction on the number of gluing generating cofibrations that under the assumption of the theorem if i : C ֒→ D is a cofibration then the map: is a cofibration. It holds if i is an isomorphism. Assume it hold for a cofibration i : C ֒→ D then we have to prove that it also holds for C ֒→ D + = D Ai B i for some map Hence we have a cofibration: which is a pushout of G(C) F (C) F (D) ֒→ G(D). and a cofibration: along the map G(A i ) → G(D). The composite of the two cofibrations with the isomorphism above is our map G(C) F (C) F (D + ) ֒→ G(D + ) hence this concludes the proof.

Proposition :
Let C, C ′ and D be three pre-cylinder categories. A morphism from C ′ to [C, D] is the same as a functor F : C ′ × C → D such that: • For each object c ∈ C, F c : x → F (x, c) is a morphism from C ′ to D.
• For each object c ′ ∈ C, F c ′ : x → F (c ′ , x) is a morphism from C to D.
• If i : a ֒→ b is a cofibration in C and i : a ′ ֒→ b ′ is a cofibration in C ′ then the natural map induced by i and i ′ : is a cofibration.
The proof is a routine check. Such a functor F : C ′ × C → D will be called a bi-morphism.

Proposition :
For any two pre-cylinder categories C and C ′ , there is a essentially unique pre-cylinder category C ⊗ C ′ endowed with a bi-morphism ⊗ : C × C ′ → C ⊗ C ′ such that for any other pre-cylinder category D morphisms from C ⊗ C ′ to D are the same as bi-morphism C × C ′ → D.

Proof :
One can consider the pre-cylinder category C ⊗ C ′ "freely generated by a bimorphism from C × C ′ ". Indeed such a bi-morphism can be described as a choice of: • An object c ⊗ c ′ for each pair of objects c ∈ C and c ′ ∈ C.
• A morphisms: for all pair of arrow f ∈ C and f ′ ∈ C.
• relation between these morphisms translating composition in C and in C ′ .
• Some of the maps are imposed to be cofibrations/weak equivalence to translate the fact that c⊗ and ⊗c should preserve weak equivalences and cofibration as well as the last conditions in the definition of bi-morphism.
• The natural maps 0 → 0 ⊗ c and 0 → c ⊗ 0 are forced to be isomorphisms.
• Certain comparison maps from a pushout to a cone should be forced to be isomorphisms in order to impose that c ⊗ and ⊗ c preserve pushout along cofibrations. and this fits in the framework of 3.2. The corresponding free pre-cylinder category C ⊗ C ′ satisfies the universal property mentioned in the proposition.
Note that in particular, the underlying cofibrations category of C ⊗ C ′ corresponds to the tensor product of the underlying cofibrations category of C and C ′ . This follow from the fact that the underlying cofibration category of the free pre-cylinder category C ⊗ C ′ is obtained by just forgeting everything about weak equivalences in the system of generators and this corresponds exactly to the notion of a bi-morphism of cofibration categories from C × C ′ .

If i :
A ֒→ B and i ′ : A ′ ֒→ B ′ are respectively cofibrations in C and C ′ then one denote by i ′ i ′ the cofibrations: 3.3.6. Proposition : If C and C ′ are two pre-cylinder categories with classes of generating cofibrations I and I ′ then the i i ′ for i ∈ I and i ′ ∈ I ′ are a class of generating cofibrations for C ⊗ C ′ .

Proof :
We will first show that if j : A ֒→ B and j ′ : A ′ ֒→ B ′ are respectively cofibrations in C and C ′ then j j ′ is a iterated pushout of the i i ′ . Let B + = B C D where i : C ֒→ D is one of the generating cofibration of C and C → B is any map, let j + be the composite cofibration A ֒→ B + . Then in the following diagram the two square are pushouts and the total vertical arrow is j + j ′ : Hence j + j ′ is an iterated pushout of j j ′ and i j ′ , moreover if either j and j ′ is an isomorphism then j j ′ is an isomorphism, hence one can proceeds by induction on gluing of generating cofibrations, we first show that if j ′ is a generating cofibration and j is any cofibration then j j ′ is an iterated pushout of the i j ′ for i a generating cofibration and then reversing the role of j and j ′ that for any pair of cofibrations j and j ′ the cofibrations j j ′ is an iterated pushout of the generating cofibrations i i ′ . From the construction of C ⊗ C ′ as a free pre-cylinder categories given in 3.3.4 and the general discussion of 3.2.4, the generating cofibrations of C ⊗ C ′ are the cofibrations of the form i i ′ together with the cofibration in C tensored by an object of C ′ and conversely, but those are special case of j j ′ when one of the two cofibrations j and j ′ is of the form 0 ֒→ c hence this shows that all the generating cofibrations of C ⊗ C ′ are iterated pushout of the i i ′ and hence that the i i ′ form a system of generating cofibrations for C ⊗ C ′ .

Proposition :
A morphism from C ⊗ (C ′ ⊗ C ′′ ) to D (with C, C ′ , C ′′ andD four pre-cylinder categories) is the same as a functor F : C × C ′ × C ′′ → D such that: • If one fixes any two of the variables one gets a morphism of pre-cylinder category in the third variables.
The only point of this proposition is that this description is completely symmetric in the three variables, hence proving that the tensor product is associative (up to canonical coherence isomorphisms) hence making the category of precylinder categories (as well as the category of cofibrations categories) into a symmetric monoidal 2-category. The unit object of the tensor product is the free pre-cylinder category on one object F * because a morphism from F * ⊗ C to D is the same as a morphism from F * to [C, D] is an object of [C, D], i.e. a morphism from C to D, hence F * ⊗ C is isomorphic to C.
Objects of [C ′ ⊗ C ′′ , D] are bi-morphisms C × C ′ → D and morphisms between them are the natural transformations.
Cofibrations in [C ′ ⊗ C ′′ , D] can be described using proposition 3.3.2 and proposition 3.3.6 together, as the natural transformations λ : F → G such that for each i : B 0 ֒→ B 1 and j : C 0 ֒→ C 1 cofibrations in C ′ and C ′′ the comparison map between the pushout of the first three object to the last one in the diagram: is a cofibrations. From this one immediately deduces that the second condition in the proposition above exactly says that cofibrations in C are sent to cofibrations in [C ′ ⊗ C ′′ , D]. The rest of the verifications are a long but easy routine check.
At this point, the following theorem becomes evident: 3.3.8. Theorem : The objects constructed in this sections endows the category of pre-cylinder categories with the structure of a symmetric closed monoidal 2-category.

A weak model structure on the category of pre-cylinder categories
In this section we will construct some sort of weak model structure on the category of pre-cylinder categories. It is not a real model structure but it will be more than enough to construct the homotopically free objects that we need. We will call acyclic (co)fibration the maps that are both (co)fibrations and weak equivalences. They might be different from trivial (co)fibrations which are the maps satisfying some lifting properties (although some comparison results between those classes will be proved showing that they are often the same). • If λ : A → B is a morphism in C and:

Fibrations and Cofibrations of pre-cylinder categories
is a factorization of F (λ) into a cofibration followed by a weak equivalence then there is a factorization of λ as a cofibration i ′ followed by a weak equivalence w ′ such that w = F (w ′ ) and i = F (i ′ ).

4.1.2.
A pre-cylinder category C is a cylinder category if and only the map C → * is a pre-fibration, indeed the pre-cylinder category * has all the retraction and all cofibration/weak equivalence factorisations.

Definition :
• A pre-cylinder category C will be said to be fibrant if the map C → * is a pre-fibration, i.e. if C is a cylinder category.
• A trivial cofibration is a morphism which has the left lifting property with respect to all pre-fibrations between fibrant objects.
• A cofibration is a morphism which has the left lifting property with respect to all acyclic pre-fibrations between fibrant objects.
• A fibration is a morphism which has the right lifting property with respect to all trivial cofibrations.
• A trivial fibration is a morphism which has the right lifting property with respect to all cofibrations.
• An anodyne morphism is a morphism which has the left lifting property with respect to all pre-fibrations.
Here are some immediate (and very easy) consequences of these definitions:

Proposition :
1. Anodyne morphisms and pre-fibrations form a weak factorization system.

Anodyne maps are in particular trivial cofibrations.
3. Fibrations are in particular pre-fibrations.

Any morphism with fibrant co-domain can be factored as a trivial cofibration followed by a fibration.
Proof : 1. The key observation here is that being a pre-fibration can be expressed as having the right lifting property with respect to two specific morphisms between free pre-cylinder category: the morphism from the pre-cylinder category freely generated by a trivial cofibration to the pre-cylinder category freely generated by a trivial cofibration with a retraction, and the morphism from the pre-cylinder category freely generated by a morphism λ : A → B to the pre-cylinder category freely generated by a diagram: Hence the result follow directly from the small object argument.
2. Anodyne maps have the left lifting property with respect to all prefibrations, in particular with respect to the pre-fibrations between fibrant objects and hence are trivial cofibrations.
4. Let f : A → B be a pre-fibration with fibrant domain, hence A is fibrant as well, hence f has the right lifting properties against all trivial cofibrations by definition of trivial cofibrations and hence it is a fibration. The converse is the previous point.

5.
Factor it has an anodyne map followed by a pre-fibration, the anodyne map is a trivial cofibration and the pre-fibration has a fibrant co-domain hence it is a fibration.

Definition : A full subcategory C ⊂ C ′ of a pre-cylinder category is said to be h-saturated if it is stable under pushout by cofibrations and if any object in C ′ which is weakly equivalent to an object in C is in C.
The following proposition is immediate:

Proposition : If C ⊂ C ′ is h-saturated then C is a pre-cylinder category for the induced structure and the inclusion functor is a pre-fibration.
In particular, if C ′ is a cylinder category then C is also a cylinder category.

If:
A X B f i h Is a diagram in C, and assume that there is another map h 2 which makes the diagram: 1. Such a diagonal filler is the same as a retraction of the trivial cofibration X ֒→ X A B, hence this follows from the fact that pre-fibrations lift retraction of trivial cofibrations.

2.
A relative cylinder object is a special case of cofibration/weak equivalence factorization and those are lifted by pre-fibrations.
3. Let us first chose a relative cylinder object I A B in C that lifts the one in D used to define the homotopy F (h) ∼ F (A) h 2 , we also fix such an homotopy The situation can then be presented as follow, one has a solid diagram in C: with a dashed arrow in D given by the map h 2 together with the homotopy F (h) ∼ F (A) h 2 as the vertical map is a trivial cofibration this can be lifted to C producing a map h ′ over h 2 and an homotopy h ∼ A h ′ over the homotopy between F (h) and h 2 .
4.1.8. Proposition : Let F : C → D be a fibration of pre-cylinder categories.
Assume that one has a square in C (with a cofibration and a weak equivalence): And assume that its image by F can be extended in D into: Where I A B is a relative cylinder object of i in D, then the extension can be lifted to C.

Proof :
This can be expressed as the fact that all fibrations have the right lifting property with respect to a certain morphism between freely generated pre-cylinder categories (freely generated by the diagram above and by a relative cylinder object). Hence the proposition boils down to saying that this map is a trivial cofibration, and hence it is enough to check the lifting property when C and D are both cylinder categories. The fact that the relative cylinder object can be lifted has been proved in proposition 4.1.7. We proved in 2.2.9 that such filing always exists in a cylinder category, so there is such a filing in C, using the lifted relative cylinder object. We call f ′ and h ′ the map obtain in C this way. We need to prove that one can replace f ′ and h ′ by maps that are send to f and h and this will be done mostly by using the last point of proposition 4.1.7. Let us call v the equivalence X → Y , then F (v) • F (f ′ ) and F (v) • f are both homotopic relative to A to the map F (k) : F (B) → F (Y ) corresponding to the bottom arrow of the square, the homotopy being respectively given by h and F (h ′ ), in particular they are homotopic relative to A by composing these two homotopies, but as F (v) is a weak equivalence it shows that F (f ′ ) and f are homotopic relative to F (A), we will call h f this homotopy, chosen such that and h. Applying the last point of proposition 4.1.7 one can lift f and h f to maps in C, which we will also call f and h f (the maps in D formerly known as f and h f are now F (f ) and F (h f ). It remains to show that the homotopy h between F (v • f ) and F (k) can also be lifted to a homotopy in C, but one already has a homotopy between v • f and k in C: it can be obtained as the composite of the homotopy h f between f and f ′ composed with v and the homotopy h ′ between k and v • f ′ , moreover it is not very hard to see (manipulating composition of homotopies and inverse of homotopies which satisfies the usual groupoids axiom up to higher homotopy) that the image of this homotopy in D is homotopy equivalent, relative to F (B) F (A) F (B), to h hence proving (applying the last point of proposition 4.1.7 one more time) that h can be lifted to C which concludes the proof.
In order to obtain a similar (partial) weak factorization system for cofibrations and trivial fibrations one needs to observe that acylic fibrations between fibrant objects can also be detected by the right lifting property with respect to a set of maps. This is achieved by the following proposition:

Proposition : A morphism F : C → D of pre-cylinder category with fibrant co-domain is an acyclic fibration if and only if it satisfies the following condition:
• It detects weak equivalences.
• If X is an object in C and i : F (X) ֒→ Y is a cofibration in D then there is a cofibration i ′ : X ֒→ Y ′ such that F (i ′ ) = i.
• If one has a diagram in C of the form: A X B f i with i a cofibration, such that it admits a filling in D:

Moreover, if the domain of F is also fibrant the first conditions can be omitted.
Note that the first condition is also a right lifting property: it corresponds to the right lifting property against the map from the free pre-cylinder category on one arrow to the free pre-cylinder category on one weak equivalence.

Proof :
We first assume that F satisfies the lifting property of the proposition. If we know that the domain is fibrant, then those conditions imply that F is acyclic: it is homotopy surjective because of the first lifting property and homotopy fully faithful because of the second condition. This in particular implies that F detect weak equivalences (because hF is an equivalence of category and hence detect isomorphisms) hence in this case the first conditions can indeed be omitted.
In the general case, if F (A) ֒→ P ∼ → F (B) is a factorization as a cofibration followed by a weak equivalence in D of a map in C, then one can lift P and the cofibration F (A) ֒→ P using the second lifting property, then one can use the third lifting property to lift the map P → F (B), and finally as F detect weak equivalences this implies that the lifting is a weak equivalence. Finally, the lifting conditions immediately implies the lifting of retractions of trivial cofibrations (it is a special case of the second lifting property). So this proves that a map satisfying those lifting conditions is a fibration. In particular the domain is fibrant hence it is acyclic.
Conversely, let F : C → D be an acyclic fibration between cylinder categories. As F is acyclic it detect weak equivalences and it satisfies the weak form of the two lifting conditions that we need to prove. The fact that it is a fibration will allow to make then strict. More precisely: If A ∈ C and F (A) ֒→ B is a cofibration then as F A : hC(A) → hD(A) is essentially surjective, there is an object B ′ of C with a cofibration A ֒→ B ′ such that F (B ′ ) is equivalent to B as objects of D(A). One can hence see Proof : This is exactly the same as proposition 4.1.4 but replacing pre-fibration with the class of map satisfying the lifting properties of 4.1.9. We will call those maps "trivial pre-fibration" 11 . Trivial pre-fibrations are characterized by the right lifting property with a set of morphism: the one from the free pre-cylinder category on one arrow to the free pre-cylinder category on one weak equivalences, and the two free constructions corresponding to the two other lifting properties of proposition 4.1.9. Applying the small object argument any map f can be factored in a map that satisfies the left lifting property with respect to trivial pre-fibration followed by a trivial pre-fibration. The first map is in particular a cofibration: it has the left lifting property with respect to all acyclic fibration with fibrant co-domain because they are trivial pre-fibrations, and if the map f has a fibrant co-domain then the trivial pre-fibration will be an acylic fibration by proposition 4.1.9.

Reedy type categories
4.2.1. Definition : A morphism f : C → C ′ of pre-cylinder category is said to be a Reedy extension if for any fibration F : D → D ′ between cylinder categories, the morphism:

is a pre-fibration. A pre-cylinder category is said to be of Reedy type if ∅ → C is a Reedy extension.
The point of this notion is that if C is a Reedy type pre-cylinder category then for all cylinder category D, the functor category [C, D] is a cylinder category, and for all fibrations between cylinder category D → D ′ , the morphism [C, D] → [C, D ′ ] is a fibration. We will think of Reedy type pre-cylinder categories as being "sketches" for some sort of theory whose category of models in a cylinder category will be a cylinder category.

Proof :
Manipulating the adjunction between internal hom objects of pre-cylinder categories and the tensor product of pre-cylinder categories constructed in subsection 3.3, one can see that for morphisms f : C → C ′ , F : D → D ′ , and i : A → A ′ saying that the map induced by f and F has the right lifting property against i is the same as saying that the map induced by i and F has the right lifting property with respect to f . Hence f is a Reedy extension if and only it has the left lifting property with respect to all the map of the form: for F : D → D ′ a fibration and i : A → A ′ a anodyne morphism (or just one of the generating morphisms of the class of anodyne morphisms). In particular, the class of Reedy extension is stable under retract, pushout and transfinite composition simply because it is characterized by a left lifting property.
So we just have to give a few examples of Reedy extension, and then the proposition above will allows to produce plenty of examples by transfinite iterated pushout.

Proposition :
The following maps are Reedy extension: • The map from F * the free pre-cylinder category on one object to F ֒→ the free pre-cylinder category on one cofibration, which send the generating object to the source of the generating cofibrations is a Reedy extension.
• The map from the free pre-cylinder category on one arrow to the free precylinder category on one equivalences.
Note that 0 → F * is a pushout of the first example (along the unique morphism F * → 0) hence it is also a Reedy type pre-cylinder category.
Proof : • Let D be a cylinder category, [F * , D] is just D, and [F ֒→ , D] is the category that we will denote D ↓ whose objects are pairs A = (A 0 , A 1 ) of objects of D together with a cofibration A 0 ֒→ A 1 , morphisms are the diagram morphisms, weak equivalences are objectwise weak equivalences and cofibrations are the map f : A → B such that f 0 : A 0 → B 0 is a cofibration and the comparison map A 1 A0 B 0 → B 1 is a cofibration (this follows from proposition 3.3.2 and the description of the generating cofibrations of a free pre-cylinder categories given in 3.2.4).
Let now F : D → D ′ be a fibration between cylinder categories, we need to show that the morphism: is a prefibration.
Let v : X → Y be a morphism in D ↓ such that one has a cofibration/weak equivalence factorization: in D, such that its image by F can be extended into a cofibration/weak equivalences factorization of F (v) : F (X) → F (Y ) in D ′ ↓ , this means that one has in D ′ : lifting this cofibration/weak equivalence factorization to D (using that F is a fibration) produces exactly what we need to complete the factorization X 0 ֒→ Z 0 ∼ → Y 0 into a factorization in D ↓ . Hence H lifts cofibration/weak equivalence factorizations.
If one has a trivial cofibration i : X ֒→ Y in D ↓ with a retraction r 0 : Y 0 → X 0 of i 0 , then finding a retraction of i that extend r 0 is the same as finding a retraction to the trivial cofibration: Hence if one can find such a retraction in D ′ it can be lifted to D and this shows that H lift retract of trivial cofibrations.
• Let F → and F ∼ be the two free categories mentioned in the proposition.
[F → , C] is the category of arrows in C with objectwise weak equivalences and objectwise cofibrations, [F ∼ , C] is the full subcategory of weak equivalences.
If F : D → D ′ is a fibration then the map: Is the inclusion of the subcategory of equivalences in D into the subcategory of arrows in D whose image in D ′ are weak equivalences, hence it is a h-saturated subcategory this concludes the proof The second example show that adding new equivalences (while keeping the same underlying cofibration category) to a Reedy type category gives a Reedy category. The first examples in the proposition above is exactly what we need to produce all the "Reedy type structure" for directed category as they were defined in [11] or [22], which is what we will now explain:

Definition :
A locally finite directed category is a category I endowed with a "height" function h : I → N such that any non-identity arrow f : i → j in I is such that h(i) < h(j) and such that all the slice category I /x are finite.

Proposition : Let I be a locally finite directed category, then:
• The category I f of finite presheaves 12 over I, with monomorphisms as cofibration and isomorphisms as weak equivalence is a pre-cylinder category.
• I f is a Reedy type pre-cylinder category.
• The completion of I f is the category I of pre-sheaves over I.
• Morphisms from I f to any pre-cylinder category C are exactly the "Reedy cofibrant I-diagram" 13 in C. Moreover the functor corresponding to a diagram is its left Kan extension.
• If J ⊂ I is a full subcategory such that if i → j is an arrow in I and j ∈ J then i ∈ I, then inclusion morphism: is a Reedy extension. 12 We mean by that presheaves which are non empty on only a finite number of element of I and which are finite on those elements 13 This can be read as "certain functors from I to C with cofibrancy conditions that we will define in the proof", but it do corresponds to the usual and well known notion of Reedy cofibrant object.

Proof :
The first claim is immediate: taking monomorphisms between finite sheaves clearly produces a cofibration category and taking isomorphisms as the weak equivalences makes it into a pre-cylinder category. All the other results are obviously true for the case of I = ∅, or maybe more clearly for I = { * }. We will prove the other claims for any finite category I, by induction on the number of objects of I. Let x be a maximal object in I (either such that h(x) is maximal, or more generally such that there is no non-identity arrow in I whose domain is x), then J = I − {x} is a category satisfying the condition of the last point, which is also directed and with strictly less object than I. Let ∂x be the object of J f "represented by x". Let C be the pre-cylinder category freely generated from J by freely adding an object x endowed with a cofibration ∂x ֒→ x.
A morphism from C to any other pre-cylinder category is given by first a morphism F from J f , i.e. a Reedy cofibrant J -diagram, together with an object F x and a cofibration F (∂x) ֒→ F x . But as F is a left Kan extension, a map from F (∂x) to F x is the same as a compatible collection of map F (y) → F x for each f : y → x in I, which makes F into a functor from I with F (x) = F x , the condition "Reedy cofibrant" can be described as F is Reedy cofibrant when restricted to J and the map F (∂x) → F (x) is a cofibration. We then use the general procedure of 3.2 to compute free categories, the completion of C is the category of morphisms from C to Set op , but by the above observations these are just presheaves over I, C is then the full subcategory of iterated pushout of: monomorphisms between finite J -presheaves (which are identified with certain I-presheaves by taking F (x) = ∅ and by the cofibration δx → x which allow to add any finite number of elements we want to F (x), hence C is indeed I f . As J f → C = I f is a Reedy extension this concludes the proof for a finite category. Indeed, for the last claim if J is a subcategory satisfying this condition, then if J = I then the claim is immediate and if not one could have chosen x not in J and concludes by induction on the difference of cardinality between the cardinal of J of I. If I is not finite but locally finite then it can be written as an increasing union of finite full subcategory J satisfying the condition of the last claim, and I f appears as the colimit of the J f and hence is also a Reedy type category.
We will also need the following proposition, which unfortunately does not seem to follow from our framework: 4.2.6. Proposition : Let I be a locally finite directed category, F : I → C a functor to a cylinder category, then there is a Reedy cofibrant functorF : I → C endowed with a natural transformationF → F which is objectwise a weak equivalence.

Proof :
We will constructF gradually on objects of I following the same induction process as in the proof of proposition 4.2.5. Let J ⊂ I be a full subcategory such that if i → j with j ∈ J then i ∈ I, and let x an object of I − J such that all the (non identity) arrow with co-domain x have domain in J . Assume thatF has already been constructed on J . We just need to extendF to x. SeeingF as a morphism from J f to C, one can form the objectF (∂x) in C. Because of the natural transformationF → F , F (X) is endowed with a compatible family of mapsF (y) for all arrow y → x in I, hence there is a map F (∂x) → x, taking a cofibration/weak equivalence factorization of this maps exactly gives what we need forF (x) and this concludes the proof.

4.2.7.
Proposition : Let f : T → T ′ be a Reedy extension of Reedy type categories which is also a trivial cofibration. Then for any cylinder category C, the map: is a trivial fibration.

Proof :
We already know that this map is a fibration between fibrant objects, so we just need to show that it is acyclic. Let A → B be an other Reedy extension of Reedy type pre-cylinder category category, and consider a diagram of the form: the two horizontal arrow can be turned into arrow T ′ → [A, C] and T → [B, C] and the commutativity of the above diagram is equivalent to the commutativity of: f but in this square the left arrow is a trivial cofibration and the right arrow is a fibration, hence there is a diagonal filler: T ′ → [B, C], which can be reinterpreted as a diagonal filler B → [T ′ , C] in the first square. This proves that our map has the right lifting property with respect to all Reedy extensions between Reedy type category. We will prove that F = [f, C] is acyclic using the second characterization of proposition 2.3.4. The case of the map F * → F ֒→ of 4.2.3 show that for all object A, F A is homotopy surjective. The case of the morphism from F ֒→ to the free category on a trivial cofibration shows that F detect trivial cofibrations among cofibrations. Using the cofibration/weak equivalence factorization this is enough to deduce that F detect weak equivalences and hence this concludes the proof.
We finish this section by introducing some Reedy type categories and Reedy extension which will be very useful in the next section.
4.2.8. We now consider the following directed categories: The category C eq corresponding to the diagram: l r c The category C I corresponds to the "co-equalizer" diagram: We let R eq and R I be the Reedy type category of finite presheaves over those directed categories in which we force all the arrow of the two diagrams to be weak equivalences. Finally if C is a cylinder category we define: C eq := [R eq , C] and C I := [R I , C]. C eq is the category of triple of objects X = (X l , X l , X c ) endowed with a cofibration X r X l ֒→ X c whose two components are weak equivalences. C I is a category of triple of objects X 0 , X I , X 1 endowed with cofibrations: such that the two legs X 0 → X I and the map X I → X 1 are weak equivalences.
One has morphisms C eq → C × C which send X to (X r , X l ) it corresponds to the inclusion of the two minimal objects in C eq , hence it is a fibration. Moreover one easily see that the morphism F * → R eq corresponding to any of the minimal element is a trivial cofibration, hence the legs C eq → C of the above map are trivial fibrations.
The inclusion of the minimal object in C I induces a Reedy extension F * → R I , which is easily seen to be a trivial cofibration. Hence the morphism b : C I → C which send X to X 0 is a trivial fibration. Finally the functor which send C eq → C I sending r and l to 0 and c to I induces a morphism C I → C eq which send (X 0 , X I , X 1 ) to (X 0 , X 0 , X I ), hence the composite with the two morphisms C eq → C are equal to b. The morphism C I → C eq is in particular acyclic by 2-out-of-3.
The intuitive idea behind those construction is that we want to construct a sort of "path object" for the cylinder category C. To do that we want to construct a category whose objects are pair of objects "with a weak equivalence" between them. This will not produce a cylinder category as such, our solution is to use instead this object X c to represent an equivalence between the two objects X r and X l . The new problem is that if one want a "identity map" from C to C eq on will need a functorial cylinder object, which in general is not available. The solution to this problem is the category C I which is in some sense the category of "cylinder object". Specifying the two maps X → IX is not enough to define a cylinder object, one also need the map IX → X, adding the maps would take us outside of the realm of Reedy category, hence we replace it by this map X I → X 1 for X 1 an object equivalent to X. One hence obtain a category C I over C which is equivalent to C and which have a map C I → C eq playing the role of this ''ìdentity map" we were trying to construct. These constructions will be key in the construction of the rest of the model structure in the next section: they will allows us to show that two fibrant replacement of a same cofibrant pre-cylinder categories are equivalents.

4.3
The weak model structure on pre-cylinder categories 4.3.1. Proposition : Let C be cofibrant pre-cylinder category, for any morphism f : C → D to a cylinder category, there is a morphism C → D eq whose composition with the two maps D eq → D are equal to f .

Proof :
As C is cofibrant and D I → D is a trivial fibration (see 4.2.8), the map f to D can be lifted to D I , one can then compose to D I → D eq to obtain the desired map.

4.3.2.
Proposition : Let C be a cofibrant pre-cylinder category, then any two fibrant replacement of C, i.e. a cylinder category C endowed with a trivial cofibration C → C are equivalent under C, in the sense that there is an acyclic map between them compatible to the map from C.

Proof :
If C 1 and C 2 are two fibrant replacements of C then using the lifting of trivial cofibrations against fibrant object, one obtain two maps f, g under C between C 1 and C 2 , we will show that g • f and f • g are equivalence, which, because of the 2-out-of-6 property, implies that f and g are weak equivalences between C 1 and C 2 So we need to prove that any endormorphisms f : C 1 → C 1 under C is a weak equivalence. Consider the (commutative) square: where the upper map is the map produced by proposition 4.3.1 using that C is cofibrant. A lifting in this square produces a map C 1 → C eq 1 which can be thought of as "a homotopy between f and the identity". The map C 1 → C eq 1 is it self acyclic (because when composed to the projection to first componenent one get the identity,and the projection C eq 1 → C is acyclic, and hence the map f (which is the composite of this map to C eq 1 with the second projection C eq 1 is an equivalence. )

Definition : A morphism between fibrant or cofibrant pre-cylinder categories is said to be acyclic if its lifting to fibrant replacements of the cofibrant pre-cylinder categories involved is acyclic.
Those definitions are consistant: they do not depends on the choice of the fibrant replacements because of proposition 4.3.2 above, and if an object is both fibrant and cofibrant then it can be used as its own fibrant replacement. Moreover any trivial cofibration from a cofibrant object is a weak equivalence as a fibrant replacement of the co-domain will also be a fibrant replacement of the domain. Also this extended notion of acyclic morphisms still satisfies 2-out-of-6 because any chain of morphisms can be lifted to a chain of morphism between some fibrant replacements (not changing the fibrant objects) and the 2-out-of-6 property for the replacement implies the 2-out-of-6 property for the original maps.
As far as we know, there is no reason for trivial cofibrations with fibrant domains to be weak equivalences (assuming their target is fibrant or cofibrant so this has a meaning) in particular one should be careful to not use fibrant replacement of an already fibrant but non cofibrant pre-cylinder category in this definition.

Proposition : A cofibration of cofibrant domain is acyclic if and only it is a trivial cofibration.
Proof : One direction is already known, so consider an acyclic cofibration with cofibrant domain. Assume first that the co-domain is fibrant. Then one can factor our map as a trivial cofibration followed by a fibration. By 2-out-of-3, the fibration part is a trivial fibration and then the lifting of cofibrations against trivial fibration gives that our cofibration is a retract of the trivial cofibration part of its factorization, hence it is a trivial cofibration. In the general case one post compose our acyclic cofibration with a trivial cofibration whose target is fibrant. The composite is an acyclic cofibration with fibrant target hence it is a trivial cofibration. But because trivial cofibration are charaterized by the left lifting property with respect to map between fibrant object this is enough to conclude that the map is a trivial cofibration, indeed if i and i • u are trivial cofibration then for any solid square where the right arrow is a fibration between fibrant objects: One can construct the dashed arrow l 1 because Y is fibrant and i is a trivial cofibration. Once this is done, one can construct the dashed arrow l 2 using the fact that the composite i • u is a trivial cofibration, and this shows that u has the lifting property and hence that it is a trivial fibration.

4.3.5.
We now sum up the properties of this weak model structure: • One knows what are weak equivalences (acyclic morphisms) only between objects that are either fibrant or cofibrant (by definition 4.3.3).
• We have four class of maps: fibration, cofibrations, trivial fibration, trivial cofibration, which are all characterized by the lifting property they are supposed to have, for examples, fibrations are exactly the maps that have the right lifting properties with respect to all trivial cofibrations and cofibrations are the map which have the left lifting property with respect to all trivial fibrations (see subsection 4.1 and in addition one defines trivial fibrations as the maps having the right lifting properties with respect to cofibrations).
• For maps with fibrant co-domain, being a trivial fibration is the same as being an acyclic fibration. (because of proposition 4.1.9) • For maps with cofibrant domain, being a trivial cofibration or an acyclic cofibration is the same (this is proposition 4.3.4).
• Any morphism with a fibrant co-domain can be factored as a trivial cofibration followed by a fibration (proposition 4.1.4) or as a cofibration followed by a trivial fibration (corollary 4.1.10).

Homotopy slice of cylinder categories
Finally, we want to consider "slice cylinder category". In general, if C is a cylinder category, the ordinary slice category C /X has no reason to be a cylinder category, so will replace this with a "homotopy slice category" which we will denote C X .
Strictly speaking, this subsection has nothing to do with the weak model structure on pre-cylinder category, but it is very much in line with the technique used here (especially with the theory of Reedy extension) and it provides new examples of fibrations between cylinder categories.

4.4.1.
Proposition : Let C be a cylinder category and X ∈ C an object. There is a cylinder category C X such that: • Morphism are the obvious diagram morphism: couple such that the naturality square with A i and B i commutes.
• Weak equivalences are the morphisms v such that v 0 is a weak equvalence (v f is always a weak equivalence by 2-out-of-3).
• Cofibrations are the "Reedy cofibrations" Moreover the functor C X → C which send A to A 0 is a fibration of cylinder categories.
Proof : Let C ′ be the category with the same description as C X but without the requirement on objects that X ֒→ A a is a weak equivalence. Then C ′ can be described as C ↓ (0 ֒→ X) in particular it is a cylinder category and the morphism C ↓ (0 ֒→ X) → C(0) = C is a fibration by proposition 4.1.6.
As C X is h-saturated in C ′ this concludes the proof.
More generally:

Proposition :
If F : C → D is a fibration between cylinder categories and X is an object of C, the natural morphism: is a fibration.
Proof : F induces a morphism C ↓ → D ↓ which is a fibration because C ↓ = [F ֒→ , C] with F ֒→ a Reedy type pre-cylinder category. Hence by proposition 4.1.6, F induces a fibration: C X and D F (X) are h-saturated sub-categories of those two cylinder categories and this F send C X to D F (X) and hence it is a fibration.

Definition : An object X in a cylinder category C is said to be h-terminal if any solid diagram in C of the form:
A X B admit a dashed filling.
Note that this is equivalent to the fact that the map X → 1 is a weak equivalence in C. In particular, any object weakly equivalent to X is also h-contractible, and it is not necessary to test the definition of h-contractible on all cofibrations A ֒→ B and all maps A → X but only on what would be necessary to test equivalences in C (see subsection 2.4).

Proposition :
• The object (X, IX, X X ֒→ IX) of C X is h-terminal.
• The fibration C X → C is acyclic if and only if X is h-terminal in C.
Proof : • Let: The map A f ֒→ B f is a trivial cofibration (indeed they are both equivalent to X) so it amit a retraction r : B f ֒→ A f , and r clearly preserve the inclusion of X.
Composing this with the map u f : A f → IX and IX → X, one obtains a map B f → X which extend the map u 0 : A 0 → X. One defines v 0 : B 0 → X to be the restriction of B f → X to B 0 , one then has a commutative square: ∼ and a diagonal filler (making only the upper triangle commute) produces the map v f such that (v 0 , v f ) is the filler we are looking for.
• If f : C → D is a acyclic morphism then it takes h-terminal object to h-terminal object. Indeed any diagram D testing whether F (X) is hterminal can be replaced by an equivalent one where the cofibration is of the form F (c), then one an construct a filler in C using that X is h-terminal and its image is a filler in D.
We now assume that X is h-terminal. Consider a solid diagram of the form: in C X and assume that the dashed arrow v exists in C, i.e. that v 0 : B 0 → Y 0 exists. Then, as Y f is homotopy equivalent to X, it is also h-terminal, and hence one can find a dashed arrow in: That produces our desired arrow v and concludes the proof.

Cylinder coherators
We can now introduced the main concept of the present paper: 5.1.1. Definition : A cylinder coherator C is a fibrant replacement of the free pre-cylinder category on one object F * . I.e it is a cylinder category with a marked object * , such that the morphism F * → C corresponding to this object is a trivial cofibration. If C is a cylinder coherator a C-groupoid is an object of the category C.
It follows 14 from the theory developed in the paper that: 5.1.2. Theorem : Let C be a cylinder coherator, then: 1. The category of C-groupoids is "algebraic", i.e. it is a category of models of a quasi-equational theory (see [21]).
2. The category of C-groupoids is endowed with a semi-model structure.
3. For any two cylinder coherator C and D the category of C-groupoid and D-groupoid are connected by Quillen equivalences (in the two directions).
4. The Quillen equivalences mentioned above identifies the homotopy categories of C-groupoids and D-groupoids in a canonical way.
It is a right Quillen equivalence, the left adjoint is called the geometric realization. This functor is unique when considered as a functor on the homotopy categories.
5.2 Semi-simplicial Kan complex and the homotopy hypothesis for cylinder coherators 5.2.1. Let ∆ denotes the semi-simplcial category whose objects are the finite inhabited ordered sets and whose map ares the injective order preserving map. ∆ is a locally finite directed category. One denotes C ∆ 0 the Reedy type pre-cylinder category of finite presheaves in this locally finite directed category (following proposition 4.2.5) but in which all the arrows between the representable objects are forced to be weak equivalences.

5.2.2.
We now introduce some objects of importance in C ∆ 0 : • ∆ n which is the representable object corresponding to [n] = {0, . . . , n} • ∂∆ n which is equal to ∆ n in dimension < n and equal to ∅ in dimension n.
∈ ∆ such that f avoid at least one value.
• Λ n k which is defined by: such that f avoid at least one value which is not k.
One has tautological inclusions (hence cofibrations) : Λ n k ֒→ ∂∆ n ֒→ ∆ n The cofibration ∂∆ n ֒→ ∆ n are generating cofibrations because of the construction done in 4.2.5 of this sort of pre-cylinder categories and the description of the generating cofibrations of a free pre-cylinder categories given in 3.2.4.

Proof :
We will show instead that the map s k : ∆ 0 → Λ n k is a trivial cofibration, as the map s k ∆ 0 ֒→ ∆ n is a weak equivalence by definition, this will concludes the proof. Moreover this will be done by induction on n. For n = 1, Λ 1 k is ∆ 0 hence the result is immediate. assume the results is proved for all j < n. We introduce: X 1 is ∆ 0 embedded by s k : ∆ 0 → ∆ n , the X i are increasing, and X n−1 is Λ n k . We will show that for all i the inclusion X i → X i+1 is a trivial cofibration. One start with X i , and let P be a subset of {0, . . . , n} which contains k and has cardinal i + 1, it corresponds to a cofibration ∆ i ֒→ ∆ n into which the maps s k : ∆ 0 ֒→ ∆ n factors. The intersection of P with X i (as sub-presheaves of ∆ n ) is isomorphic to Λ i j for some j (corresponding to the position of k in P ) and its inclusion to P is the natural map Λ i j → ∆ i taking the pushout: produces a sub-object of [n], where in comparison to X i , P and P − {k} have been added as possible images for f . One can iterate this for all such subset P , every times it corresponds to a pushout along Λ i j → ∆ i for some j and in the end one gets X i+1 . Hence X i → X i+1 is a trivial cofibration by induction, and this concludes the proof.

5.2.4.
Definition : Let C ∆ be the pre-cylinder category freely obtained from C ∆ 0 by freely adding one retraction to all the trivial cofibration Λ n k ֒→ ∆ n for n > 0.
The natural inclusion C ∆ 0 → C ∆ is a trivial cofibration as it is obtained by freely adding retractions to some trivial cofibrations. C ∆ can be described using the theory developed in subsection 3.2. Its completion is the category of semi-simplicial set X, endowed with maps X(Λ n k ) → X(∆ n ) which are sections of the natural restriction map X(∆ n ) → X(Λ n k ). They somehow are a semi-simplicial version of the category of "algebraic Kan complexes" introduced in [20]. The category C ∆ it self is the full subcategory of objects which can be obtained by freely adding cells gradually.
In order to prove the homotopy hypothesis, it will be convenient to consider a very specific (and very classical) geometric realisation morphism: C ∆ → finite CW-complex. 5.2.5. Definition : Let R be the geometric realization morphism defined first on C ∆ 0 be sending ∆ n to the ordinary n-simplex in the cyinder category of finite CW-complex and then extending it C ∆ by chosing any image of the freely added retraction of Λ n k ֒→ ∆ n .
5.2.6. Lemma : Let X be an object of C ∆ , one can forget its additional structure and consider it as a (no longer finite) semi-simplicial set, which we will denote by X ss . There is a natural comparison map from the geometric realization |X ss | of X as a semi-simplicial set to R(X) and it is a homotopy equivalence.
Proof : Any object X in C ∆ is obtained by a finite sequence of iterated pushout of ∂∆ n ֒→ ∆ n . We will prove the result by induction on this cell gluing process.
The case X = ∅ is trivial. Let X be any object, and assume that the map |X ss | → R(X) is constructed and is a homotopy equivalence. Let a : ∂∆ n → X and let: We need to understand better what is X + ss and its geometric realization in order to compare |X + ss | to R(X + ) = R(X) ∂∆n ∆ n , i.e. how the colimit describing X + is computed concretely. One can first compute the colimit Y = X ss ∂∆n ∆ n in the category of semisimplicial set. It boils down to simply add one n-dimensional cell to X ss . The geometric realization of Y as a semi-simplicial set is |X s s| ∂∆n ∆ n . As any colimit in a category of models of a quasi-equational theory, one then need to iteratively freely add all the missing structures, in this case it boils down to iteratively take pushout along Λ n k ֒→ ∆ n , in particular the geometric realization of the map of semi-simplicial set Y → X + is a trivial cofibration of CW-complexes. Moreover this map has a retraction, either simply because it is a trivial cofibration, but there is even a canonical (and functorial) such retraction using the fact that all the Λ n k ֒→ ∆ n have already a chosen retraction (fixed by the morphism R). Now R(X + ) is R(X) ∂∆n ∆ n and one has a commutative diagram: hence this concludes the proof.

5.2.7.
Lemma : Let X ∈ C ∆ , let a : ∂∆ n → X be a map in C ∆ and assume that there is commutative triangle: in the category of finite CW-complexes. Then f can be replaced by an arrow of the form R(x) for x an n-cell de X whose boundary is a and such that R(x) is homotopy equivalent to f relative to ∂∆ n .

Proof :
As R(X) and |X ss | are homtopy equivalent, one can replace R(X) by |X ss | in the above diagram: it will not change the existence or not of a diagonal filling nor the question of homotopy between two such filling. X ss is a semi-simplicial Kan complex, so by [23] it can be endowed with degeneracies making it into a simplicial set and hence a simplicial Kan complex (a more direct combinatorial proof of this can also be found in [19]), in particular, there exists a simplicial Kan complex Y such that X ss is equal to Y ss , i.e. the semi-simplicial set obtained by forgetting the face maps of Y . There is a natural homotopy equivalence from |X ss | to |Y | (because |X ss | is the so called fat geometric realization of Y ). Our map a ′ and f can be pushed forward to |Y | were it is well known that the map f will be represented (up to homotopy relative to |∂∆ n |) by a cell of Y (this follows from the Quillen equivalence between simplicial set and spaces and the fact that Y is a Kan complex, hence a fibrant object). This cell of Y is in particular a cell of X ss and a cell of X (they all have the same underlying semi-simplicial set), and as the map from |X ss | to |Y | is an homotopy equivalence, the homotopy between f and |x| in |Y | can be lifted to |X ss | and then pushed to R(X) and this concludes the proof.

Proposition :
The geometric realization from C ∆ to finite CW-complexes is homotopy fully faithful, more precisely: for every cofibration A ֒→ B in C ∆ for every map a : A → X in C ∆ and for every commutative triangle in the category of finite CW-complex: there exists a map f ′ : B → X making the triangle commutes in C ∆ and such that |f ′ | is homotopy equivalence to |f | relative to |A|.

Proof :
This is an immediate induction using the above lemma and the fact that any cofibration inf C ∆ is an iterated pushout of maps ∂∆ n → ∆ n .
5.2.9. Proposition : C ∆ is a cylinder category.

Proof :
We will first prove that it admit cylinder objects. Any object is obtained by iterated gluing of boundary inclusion: ∂∆ n ֒→ ∆ n , so we will work by induction on those gluing. The initial object always has a cylinder object (the initial object).
Assume that X ∈ C ∆ has a cylinder object IX. Let X + = X ∂∆n ∆ n for some integer n and some map a : ∂∆ n → ∆ n . Let: There is a cofibration X + X + → Y and a map Y → X + which send IX to X by the natural map and the X + to X + by the identity. Let also: where we only add a new cell to the second component. The natural map Z → Y is a cofibration and the map Z → X + is a weak equivalence (it is a pushout of the weak equivalence IX → X along ∂∆ n ֒→ ∆ n ). The map i 0 • a : ∂∆ n → Z, i.e. the one which has not been filled yet, actually already have a filling: indeed it has one when it is composed with the weak equivalence Z → X + , hence it has one at the level of geometric realization and hence it has one by proposition 5.2.8. Let b : ∆ n → Z be this map. Then one has a map ∆ n ∂∆n ∆ n → Y which send ∂∆ n to i 0 • a, the first ∆ n to the cell freely added in Y and the second ∆ n is send into Y though the map b defined above. Then let: IX + = Y ∆n ∂∆n ∆n I ∂∆n ∆ n = Z ∆n I ∂∆n ∆ n Z → IX + is a weak equivalence because it is a pushout of a tribial cofibration, and there is a natural map IX + → X + which is hence a weak equivalence by 2out-of-3. The map X + X + ֒→ Y ֒→ IX + is a cofibration hence this concludes the proof that X + admit a cylinder object and hence that every object admit a cylinder object. It remains to show that trivial cofibration admit retraction, but this follow from proposition 5.2.8 and the fact that trivial cofibration are cofibration and admit retraction on their geometric realization.

Theorem :
The geometric realization functor from C ∆ to finite CWcomplexes is acyclic.

Proof :
We have already shown that these two categories are cylinder category and that the functor is homotopy fully faithful, hence we only have to show that it is homotopy full i.e. that each finite CW -complexes is homotopy equivalent to something in the image of the geometric realization. This is immediately proved by cellular induction in the category of CW-complexes: it is obvious for the empty CW-complex. If a CW-complex X is homotopy equivalent to |Y |, and X + is obtained from X by gluing one extra cell then X + is homotopy equivalent to something of the form |Y | with one extra cell glued. This cell is glued along a map S n → |Y |, but S n can be seen as the geometric realization of ∂∆ n hence by proposition 5.2.8 this map is homotopy equivalent to the geometric realization of a map ∂∆ n → Y hence X + is homotopy equivalent to the geometric realization of Y + = Y ∂∆n ∆ n . 5.2.11. Proposition : The morphism F * → C ∆ and F * → C ∆ 0 corresponding to the object ∆ 0 are trivial cofibrations.

Proof :
It is enough to prove it for F * → C ∆ 0 , as the map C ∆ 0 → C ∆ is clearly a trivial cofibration. Let F : X → Y be a fibration between cylinder categories, let h : C ∆ 0 → Y and let h 0 be a lifting of ∆ 0 to X, one need to extend this to a lifting of h. As Y is a cylinder category, h can be extended to a functor from C ∆ to Y . Now using one can easily construct in C ∆ a maps c n : ∆ n → ∆ 0 whose restriction to the face are the map C k : ∆ k → ∆ 0 : this is done by induction on n by applying 5.2.8 to the cofibration ∂∆ n ֒→ ∆ n . In particular, ∂∆ n → ∆ n → ∆ 0 is a factorization as cofibration followed by a weak equivalence. Such a factorization can always be lifted trough a trivial fibration, hence one can lift h to X going though the induction procedure that construct the pre-cylinder category attached to a a locally finite directed category: for each n, we will be able to lift the cofibration ∂∆ n ֒→ ∆ n , hence producing a lifting of h at least as a morphism ∆ f → X. Moreover as at every step the lifting comes with a weak equivalence ∆ n ∼ → ∆ 0 it ensure that the newly lifted object ∆ n will indeed be homotopicaly equivalent to the previously lifted object and hence that it is indeed a morphism from C ∆ 0 .

Grothendieck weak ∞-grouppoids
We refer to [3] for the definition and all results about Grothendieck ∞-groupoid.
We fix a coherator C (see [3, 2.11]) and when we say ∞-groupoid is means ∞groupoid of type C.

5.3.1.
We denote by D n the free ∞-groupoid generated by one cell in dimension n and by S n the free ∞-groupoid generated by two parallel cell of dimension n. S −1 will be the initial object (the empty groupoid) ∅ by convention. What we call the natural map S n−1 → D n is the one that send the two generators of S n−1 to the source and the target of the generator of D n .

Definition :
One say that an ∞-groupoid is finitely cellular if it is obtained from the empty groupoid by freely adding cells, i.e. by iterated pushout of the maps S n−1 → D n for n 0.

5.3.3.
Conjecture : Let X be a finitely cellular ∞-groupoid, and let a be an n-cell of X. Consider X + the (finitely cellular) ∞-groupoid obtained by freely adding a cell a ′ parallel to a and a cell i between a and a ′ . i.e. X + is the pushout: Then X → X + is a weak equivalence.
In all the rest of the subsection we investigate consequences of this conjecture.

5.3.4.
Lemma : If conjecture 5.3.3 holds, then it also holds when X is a retract of an arbitrary cellular object, i.e. is a retract of an object obtained from ∅ as a transfinite composition of iterated pushout of S n → D n+1 .

Proof :
This follow easily from the fact that directed limits in the category of ∞groupoids are computed level wise, and that π-groups commute to those directed limits.

5.3.5.
Theorem : Under conjecture 5.3.3 there is a "canonical" semi-model structure on the category of ∞-groupoid such that: • Weak equivalences are the weak equivalences of [3, 4.17 and 4.18].
• Fibrations are the map with the right lifting property with respect to s : • Trivial fibrations are the maps with the right lifting property with respect to the natural maps S n → D n+1 .
Note that as the maps D n → D n+1 admit retraction, every object is fibrant.

Proof :
By the small object argument one has two factorization systems in cofibration/trivial fibration and trivial cofibration/fibration with the fibrations and trivial fibrations defined above. The characterization of [3, 4.18. (4)] of weak equivalences can be reformulated as the fact that every square of the form: f admit a filing of the form: hence the exact same proof as in proposition 2.4.6 show that trivial fibrations are exactly the fibrations that are weak equivalences. The conjecture, and its extension by the lemma above shows that transfinite iterated pushout of the D n → D n+1 out of a cofibrant objects are weak equivalences, hence by the small object argument any map out of a cofibrant object can be factored as "trivial cofibration" which is a weak equivalence followed by a fibration. As weak equivalences of ∞-groupoid satisfies 2-out-of-3 this concludes the proof.
5.3.6. Proposition : Assuming conjecture 5.3.3. The category Gpd f of finitely cellular ∞-groupoids is a cylinder category with the S n−1 ֒→ D n as generating cofibrations and the weak equivalences of ∞-groupoids as weak equivalences.

Proof :
The existence of retraction to trivial cofibrations follow from the fact that those will be trivial cofibrations in the canonical model structure on ∞-groupoids and hence will admit a retraction as every object is fibrant. The only non trivial things is the existence of cylinder object. One will need the following fact easily proved by induction: if X ֒→ Y is an iterated pushout of some finite set of cofibration A i ֒→ B i in a cylinder category then one can chose a relative cylinder object I X Y such that Y ֒→ I X Y is an iterated pushout of the trivial cofibrations B i ֒→ I Ai B i . As in the cylinder category of cofibrant ∞-groupoids the cofibration S n−1 ֒→ D n have relative cylinder object which are themselves finitely cellular (D n+1 ) this implies that any finitely cellular object admit a finitely cellular cylinder object. This concludes the proof.

Proof :
Consider the following free construction of pre-cylinder category. One start with the globular category: It is a directed locally finite category, hence one get a Reedy type pre-cylinder category of finite globular sets with monomorphism as cofibrations and we ask that the structural map between the D i are weak equivalence. This pre-cylinder category Glob f is endowed with a morphism F * → Glob f which is cofibrant, and the completion of Glob f is the category of globular set. The map "S n−1 → D n " (the free globular set respectively generated by two parallel n − 1 cells and one n-cell) are generating cofibrations. One then follow the construction of the coherator C we have fixed in the beginning, and for each lifting of a parallel pair that is freely added during the construction of C one free add the same arrow freely to our pre-cylinder category. The completion of the resulting category C is the category of ∞-groupoid and as we have not added any cofibration the pre-cylinder category we have generated is (at least as a cofibration category) Gpd f . The weak equivalences in C are generated by the D n ֒→ D n+1 (it is the smallest class that contains those maps and satisfies the axioms for pre-cylinder categories), in particular, weak equivalences in C are weak equivalences in Gpd f , but as Gpd f is a cylinder categories any trivial cofibrations in Gpd f is a retract of an iterated pushout of the D n ֒→ D n+1 (which are the legs of the relative cylinder object of the generating cofibrations) and hence C is the same as Gpd f . In particular F * → Gpd f is cofibrant. Moreover, the description given in proposition 2.4.19 of the semi-model structure on the completion in terms of the generating cofibrations shows that the model structure on the completion is exactly the one of proposition 5.3.5.
5.3.8. If we do not assume conjecture 5.3.3, the proof of the above proposition still construct a pre-cylinder category C that we will denote Gpd f which is defined by this free construction. It is still true that it is the category of finitely cellular ∞-groupoid and that the S n → D n+1 are generating cofibrations, but if we do not assume the conjecture it might not be a cylinder categories and its weak equivalences can be different from the ones defined in [3, 4.17 and 4.18], in fact any of these two facts would implies the conjecture. This will be our definition of Gpd f if we do not assume conjecture 5.3.3.

5.3.9.
Lemma : This lemma holds without assuming conjecture 5.3.3 as long as Gpd f is defined using the free construction in the proof of proposition 5.3.7 as explained in 5.3.8.

Proof :
We follow the "free" description of Gpd f given in the proof of proposition 5.3.7 to construct the lifting. The first step is to lift the co-globular object. In Gpd f one has a cofibration/weak equivalences: Lifting this factorization gradually produces a co-globular object in X whose zero object is o, which is a lifting of the one in Y and whose structural maps are all weak equivalences. We now need to gradually lift the map corresponding to the liftings of parallel pairs freely added in the construction of the coherator. Each such pair has the form S n → S where S is an ∞-groupoid obtained as a globular sum of the D n (see [3, 1.3]), and a lifting is an extension of S n ֒→ D n+1 → S. The map S n → G is already lifted to X and a lifting exists in Y , one need to find a lifting in X which is over the lifting in Y . One easily see that the objet S is weakly equivalent to o hence it is itself h-terminal hence such a lifting S n ֒→ D n+1 → S automatically exists in X, its image in Y might not be equal to the lifting already existing but it is going to be homotopy equivalent relative to S n because f (S) is also h-terminal. Hence one can apply the last point proposition 4.1.7 to find a lift in X which is sent to the correct lift in Y and this concludes the proof.
5.3.10. The lemma above is enough to show (even without assuming conjecture 5.3.3) that any object in any path category can be "endowed with a structure of Grothendieck ∞-groupoid", or more precisely, the globular object given by any iterated relative path object can be endowed with the operation making it into a Grothendieck ∞-groupoid. Indeed, dually it corresponds to the statement that for any object X in a cylinder categories C, there is a morphism Gpd f → C which send D 0 to X, and this is proved by applying the lemma the the fibration C X → 0. Indeed X is hcontractible in C X because of proposition 4.4.4 hence one can lift the unique morphism Gpd f → 0 to a morphism Gpd f → C X , composing with the fibration C X → C produces the desired morphisms.
We have not been able to extend this argument to prove that F * → Gpd f is a trivial cofibration without assuming conjecture 5.

Proof :
In the category of ∞-groupoid the map from D 0 to the terminal groupoid * is a trivial fibration. Hence D 0 is h-terminal in Gpd f , hence by proposition 4.4.4 the map Gpd f /D0 → Gpd f is a trivial cofibration, and as Gpd f is cofibrant one can construct a morphism Gpd f → Gpd f /D0 which send D 0 to the object (D 0 , D 1 ) and whose composite with the natural fibration Gpd f /D0 is the identity. Composing this to the natural map Gpd f /D0 → C /f (D0) gives us the desired lifting, and the image of D 0 is f (D 0 ), f (D 1 ) which is a h-terminal object. 5.3.12. Corollary : (assuming conjecture 5.3.3) The morphism F * → Gpd f corresponding to D 0 is a trivial cofibration, hence Gpd f is a cylinder coherator.
Proof : Consider a square: with f a fibration between fibrant object. h send D 0 to f (o), one can hence construct using lemma 5.3.11 a first factorization: As f is a fibration, this cylinder object can be lifted to X and one can hence extend this into a factorization:

Proof :
This follows from the fact that it is a cylinder coherator and theorem 5.1.2.

5.4
The opposite of the syntactic categories of (weak) intentional type theory The main goal of this last subsection is to reconnect to theory developed here with type theory. For a reader not interested in type theory, it still contains an interesting result: there exists a notion of weak globular ∞-groupoid (i.e. a globular set with certain "composition operations" defined between finite projective limit for the set of n-cells) which fits into our framework and hence which satisfies the homotopy hypothesis. If the reader is only interested in this results he can take the discussion of 5.4.12 as a definition of the cylinder coherator C(T * w.i.e. ) op as a free pre-cylinder category and avoid almost all mention of type theory.
Giving a precise and general enough definition of what is a type theory is a difficult task and subject to debate that we will not try to answer here. We will just give some examples of things that we will call "type theory" which defines a syntactical category and which are of the vague form described just below. 5.4.1. A type theory will be a formal system (i.e. a set of rules) for deriving statement of the form Γ ⊢ J Where J is a judgement and Γ is a context. A judgement can have one of the following form: A Type or x : A Which are supposed to be interpreted respectively as the fact that A is a well formed expression denoting a type and that x is a well formed expression denoting an inhabitant of the type A.

5.4.2.
Contrary to most reference (for example [6]), one does not need equality of types or of variables to be judgements. This is because all the computation rules of the type theory that we will consider will holds up to propositional equality (and not definitional equality), hence these types theory would have no rules proving definitional equality of types or variables aside from the obvious structural rules, and hence can only proves definitional equality when there is actually "syntactical" equality of the expression. For this reason it is considerably simpler to remove judgemental equality all together and only consider propositional equality and "syntactical equality". 5.4.3. A "context" is a device whose purpose is to make explicit the type of all the free variables that appears in a judgement J . More precisely it is a finite sequence: Such that the x i are free variables, no free variables appears in A 0 and the only free variables that appears in A i are x 0 , . . . , x i−1 . A context is said to be valid (with respect to a type theory) if the following judgement can be inferred from the rules of the type theory:

5.4.4.
A rules for a type theory will be of the form: Such a rule means that if all the Γ i ⊢ J i can be inferred from the type theory, one can apply this rules to deduces that Γ ⊢ J can also be inferred. There should be some of the rules (called axiom) for which n = 0, and one says that a judgement can be inferred from a type theory if it can be obtained this way by a finite number of applications of the rules (and axioms).

5.4.5.
We start by what we will call the "syntactical rules" which are the rules that in some sense ensure that the judgements and context behave in the way their intuitive interpretation suggest: (S1) -(Axiom): if a : A appears in the context Γ then: where T [a/x] mean that all the occurrence of the free variable x in T have been replaced by a.
Those rules does not allow to prove anything interesting by themselves, but they ensure a good behaviour of the type theory and allow to construct its "syntactic category". 5.4.6. If T is a type theory with at least the rules (S1), (S2) and (S3). And if Γ and ∆ are two valid context within a type theory T, then a context morphism t from Γ to ∆ with ∆ = (x 1 : A 1 , . . . , x n : A n ) is a collection of terms t 1 , . . . , t n such that: The following lemma show in particular that this definition is meaningful, i.e. that:

Proof :
By iterated application of the weakening axioms (S2) one has that Γ, ∆ ⊢ J then by iterated application of the substitution axiom one can gradually remove the variable x i (starting with x 1 and going up) for the context ∆ and replacing it every where by t i to obtain the result once they have all been replaced.
This lemma also allows to define composition of context morphisms f • g with f = (f 1 , . . . , f n ) as (f 1 [g], . . . , f n [g]). And one easily see that and that the composition is associative. This defines a category C(T) called the syntactic category of T whose object are the context and whose morphisms are the context morphisms.

Proposition :
If T is a type theory with at least the rules (S1), (S2) and (S3). Then its syntactic category C(T) is a fibration category (the opposite of a cofibration category) with fibrations (cofibration in the opposite category) being the map that are isomorphic to a morphism p : Γ, ∆ → Γ which is of the form (x 1 , . . . , x n ) for Γ = (x 1 : A 1 , . . . , x n : A n )

Proof :
Those morphisms clearly contains isomorphisms. We will first show that they are stable under pullback, for this it is enough to show that the "dependant projection", i.e. the map of the form p : Γ, ∆ → Γ are stable under pullback. Let f : Γ ′ → Γ be a context morphism, then because of the lemma 5.4.6 Γ ′ , ∆[f ] is a valid context which fits into a square: where the upper arrow if f on the component corresponding to Γ ′ and is "the identity" (at least syntactically) on the variable corresponding to ∆[f ]. If one has a morphism Γ ′′ → Γ ′ , ∆[f ] then the first componenents should be a morphism Γ ′′ → Γ ′ and the remaining component should be an extenion of the composition with f to Γ, ∆, hence Γ ′ , ∆[f ] is indeed the pullback we are looking for, this proves that pullback of a dependant projection exists and can be represented by dependant projection, hence pullback of fibrations exist and are fibrations. Another consequence of this "pullback stability" of dependant projections is that if p is a dependant projection and i is an isomorphism then p • i is equal to i ′ • p ′ for i ′ an isomorhisms and p ′ a dependant projection hence fibrations are closed under compositions. Finally, the empty context is a terminal object and all the map to the empty context are dependant projection, hence fibrations.
5.4.8. We now introduce the three examples of type theory we are concerned with: The theory T * Id has the three rules (S1), (S2), (S3) and in addition: (T1) (Free object) ⊢ * Type (T2) (Identity type) The first axioms is what makes all those type theory "freely generated on one object * ". A few things need to be clarified in this last two axioms about what are J and H syntactical. Our point is that we want to make those terms "as different as possible" from one others (i.e. minimalize the syntactical equality between J terms and H terms). They will both have free varibables: J has all the variables appearing in Γ, a : A, b : A, γ : Id(a, b), ∆ as free variables and H has all the variables appearing in Γ, a : A, ∆[a/b, r(a)/γ] as free variables. They also have a subscript to distinguishes them which contains all the assumption of the rules that produces them (one consider two such subscript equal if one can go from one set of assumption to another by just renaming the free variables). It is probable that those conventions can be modified to have more equality between J terms and H terms but one need to be very careful here as it can change the fact that the obtained syntactical category will or will not be a trivially cofibrant extension of F * . 5.4.9. The idea of having "weak identity type" as in our theory T * w.i.e where the computation rules is a propositional identity instead of a definitional identity comes from B. van den Berg in [6]. 5.4.10. Let us gives some examples of context that one can form in those different type theories. In T * Id (and hence also in all the other type theory mentioned) ∅ is a context, one has ∅ ⊢ * Type by the rule (T 1), hence (x : * ) is also a valid context. One can iterate this and (x : * ; y : * ) and (x : * , y : * , z : * ) and so one are all contexts.
In T * ref l and T * w.i.e. one can form additional terms, which in turn (because of rules (T 2)) allow to form new context by using Id(t 1 , t 2 ) for t 1 and t 2 terms involving r,J or H.
The convention we chose about equalities between J terms and H terms produces an essential difference between the rules (T 4) and (T 5) on one hand and the rules (T 2) and (T 3) on the other hand. Indeed, while (by convention) each application of the rules (T 4) and (T 5) produces syntactically different terms, different applications of the rules (T 3) and (T 2) can produces the same terms. For example if one has: Γ ⊢ Type A, a : A, b : A then by application of (T 2) one has Γ ⊢ Id A (a, b) Type, but one also has: Γ, x : A, y : A ⊢ Id A (x, y) and one can substitute x and y by a and b using the rules (S3) to obtain again Γ ⊢ Id A (a, b). In this example we obtained twice the same judgement by applying different rules, which shows that the syntactic category is not "Freely generated by the rules" which will make it considerably more complicated to use and suggest that the corresponding cylinder category that we will obtain might not be cofibrant. There is several solutions to solve this problem, the first would be to take the same conventions as we did for the rules (T 4) and (T 5), this solution would work but the resulting cylinder category would have considerably more object and its completion would not be formed of "globular groupoids" anymore. Instead we will modify the rules (T 2) and (T 3) in order to restrict them to a "minimal" set of applications.

Consider the following weakening of the rules (T 2) and (T 3):
Proposition : In the three theory above, the rules (T 2) can be replaced by the following infinite family of axioms: (T 2 ′ 1 ) s 0 : * , t 0 : * ⊢ Id 1 (s 0 , t 0 ) Type . . . Those new rules do not suffer from the problem with the rules (T 2) and (T 3) mentioned above: each rules produces a syntactically different object, and you can read from the syntax which rules has been used to produce it.

Proof :
All these rules are special case of (T 2) and (T 3) so we need to show that the general form of the rules (T 2) and (T 3) can be deduced from those specific cases and manipulation involving the structural rules (S1), (S2) and (S3). In the three theories above, there is no other rules allowing to form type than (T 1) and (T 2), hence any type is either of the form * or Id A for some other type A. In particular one can define by induction the "height" of a type: * has height 0 and Id A has height the height of A plus one. One define the height of a variable to be the height of its type. A variable x of height n > 0 has a "source" and a "target" of height n − 1: indeed x is of type Id A (a, b) for some a and b of type A of height n − 1 we call a the source of x and b the target of x. Specifying a variables of heights i definable in some context Γ is the same as specifying a context morphism: Γ → (s 0 : * , t 0 : * , s 1 : Id 1 (s 0 , t 0 ), . . . , v : Id i (s i−1 , t i−1 ) Where (at this point) Id i is a short cut for: Id 1 = Id * , Id 2 = Id Id(s0,t0) . . . Indeed such a morphism v will corresponds to some variable of height i and then all the s k and t k will be the iterated source and target of v. And similarly a pair of variables of a same type A of height (i − 1) is the same as a morphism: Γ → (s 0 : * , t 0 : * , s 1 : Id 1 (s 0 , t 0 ), . . . , s i−1 : Id i−1 (s i−2 , t i−2 ), t i−1 : Hence if Γ ⊢ A Type, Γ ⊢ a : A and Γ ⊢ b : A and if i denotes the height of A there such a morphism from Γ to the context above and Id A (a, b) can be defined as Id i (a, b). Hence any application of the rules (T 2) can be deduce as an application of a rule (T 2 ′ i ) and an application of the substitution rule. Similarly, if Γ ⊢ A type and Γ ⊢ a : A with A of height i, one has a unique morphism Γ → (s 0 : * , t 0 : * , s 1 : Id 1 (s 0 , t 0 ), . . . , v : Id i (s i−1 , t i−1 ) which send a and v and one can define r(a) as r(v) after substitution along this morphism and this concludes the proof.
We will now explain how to construct morphisms from a syntactical category as C(T * w.i.e. ) to another fibration category (or equivalently from C(T * w.i.e. ) op to a cofibration category), and how to detect if such morphisms are morphisms of (pre-)cylinder category/(pre-)path category. 5.4.12. If F : C(T) → F is a morphism of fibrations category whose domain is a syntactical category of a type theory T, then each judgement of T can be "interpreted" in F : • Each valid context Γ in T produce an object F (Γ) in F .
• Each type in context: Γ ⊢ A Type produce a fibration F (Γ, A) ։ F (Γ) which is the image of the fibration (Γ, x : A) → Γ.
• Each terms Γ ⊢ a : A produce a sections of the fibration F (Γ, A) ։ F (Γ) which corresponds to the map Γ → Γ, x : A which is the identity on all variables except the last ones, which substitute x for a.
In the special case where T is generated by "nice" rules, it is enough to interpret the rules. In order to construct inductively a morphism from the syntactical category of one of our type theory one just need to explain how each rules (T 1), (T 2 ′ i ), (T 3 ′ i ), (T 4), (T 5) is interpreted: (T1) One has a chosen object X in F .
(T 2 ′ ) 1 One has a chosen object Id X 1 in F endowed with a fibration Id X 1 ։ X × X (T 2 ′ ) i One has a chosen object Id X i endowed with a fibration p i : Id X i ։ Id X i−1 × Id X i−2 ×Id X i−2 Id X i−1 where the maps Id X i−1 → Id X i−2 × Id X i−2 involved in the fiber product are both p i−1 . (by convention Id X 0 = X and Id X −1 is the terminal object.) (T 3 ′ ) i One has a chosen map r i−1 : Id X i−1 → Id X i which factor the diagonal maps: (one has in particular for i = 0, r 0 : X → Id X 1 ) (T4) Assume one has judgements as in the premise of (T 4) which have already been interpreted. It means that one has a diagram of the form: We also need to a construct a "relative homotopy" between them: H : F (Γ, A, ∆[a/b, r(a)/γ]) → F (Γ, A, A, Id A , ∆, C, C, Id C )) Finally: Lemma : A morphism of fibration categories F : C(T * w.i.e. ) → C for C a prepath category 16 is a morphism of pre-path category if and only if all the maps in C: Produces by rules (T 3 ′ i ) above are weak equivalences.

Proof :
All those maps r are weak equivalences in C(T w.i.e. ) hence they should be sent to weak equivalences by any morphism of pre-cylinder categories. Conversely, if all these maps are sent to weak equivalences then any maps of the form r A : (Γ, A) → (Γ, A, A, Id A ) produced by rules (T 3) will also be a weak equivalence (because it is a pullback of one of the maps produced by (T 3 ′ i ) in a situation where the cube lemma applies). Finally, An arrow f : X → Y is a weak equivalence in C(T * w.i.e. ) if and only if it has a "homotopy inverse", i.e. a map g : Y → X such that f • g and g • f are "homotopic to the identity" where homotopic is defined using the path object constructed in [6, section 5 and 6] from the identity types. Hence it is enough to forces the identity type to be sent to relative path object to have that F preserve the equivalences.

Proof :
The fact that it is a cylinder category is the main result of [6]. So we just have to prove that the map F * → C(T * w.i.e. ) op corresponding to the marked object is a trivial cofibration, i.e. that it has the left lifting property with respect to all fibrations, but this follow immediately from the description of morphisms of pre-cylinder categories C(T * w.i.e. ) op → C given in 5.4.12: The rule (T 1) corresponds to the choice of an object, which corresponds to the arrow from F * hence does not need to be lifted. The rules (T 2 ′ i ) and (T 3 ′ i ) together corresponds to choosing a cofibration/weak equivalences factorization of a morphism (in fact a relative cylinder object) and such a choice can always be lifted along a (pre-)fibrations (definition 4.1.1) and finally axiom (T 4) and (T 5) together corresponds to the choice of a weak filing of the square (in the fibration category C(T * w.i.e. )): • The completion of C(T * w.i.e. ) op can be described as the category of globular sets (G n ) endowed with additional operation which are maps between finite projective limits of the G n cells satisfying certain relations, the precise definition of those maps being controlled by the type theory T * w.i.e. .

Proof :
In all case it is a direct application of the description of morphisms out of these syntactical category given in 5.4.12 to understand the completion as the category of morphisms to the pre-cylinder category Set op . In the first case, one just need to pick a set G 0 and then a series of set G n endowed with a map G n → G n−1 × Gn−2×Gn−2 G n−1 and this corresponds exactly to a globular set, in the second case one need to add the reflexivity map r : G n → G n+1 and this corresponds exactly to a reflexive globular set, and in the third case one need to add all the operations that can be produces using the reflexivity terms and the rules (T 4) and (T 5).

5.4.15.
Finally we would like to point out that for the cylinder coherator C = C(T * w.i.e. ) the notion of C-groupoid should be definable within intentional type theory using the same strategy of syntactic groupoid as G.Brunerie in [10], we just have to replace the type theory introduced in [10] by the more classical type theory T * w.i.e. introduced here.