Simon Forest

An extension of Batanin's approach to globular algebras *

In earlier work, Batanin has shown that an important class of definitions of higher categories could be apprehended together simply as monads over globular sets. This allowed him to generalize the notion of polygraph, initially introduced by Street and Burroni for strict categories, to all algebraic globular higher categories. In this work, we refine this perspective and introduce new constructions and properties for this class of higher categories. In particular, we define the notion of cellular extension and its associated free construction, from which we obtain another definition of polygraph and the adjunction between globular algebras and polygraphs. We moreover introduce two criteria allowing one to use most of the constructions of this article without having to describe explicitly the underlying globular monad.

Introduction

Over the last years, higher categories have emerged as a convenient tool to study problems in mathematics, physics and computer science [START_REF] Baez | Physics, topology, logic and computation: a Rosetta Stone[END_REF][START_REF] Leinster | Higher Operads, Higher Categories[END_REF]. The notion of "higher category" encompasses informally all the structures that have higher-dimensional cells which can be composed together with several operations. It admits a vast number of definitions, which can make it hard to apprehend.

In order to get a more global view and factor out several common constructions and properties across the different possible definitions higher categories, it is useful to consider a restriction of this general notion to a more formal class of theories. This was done by Batanin [START_REF] Michael | Computads for finitary monads on globular sets[END_REF], who introduced a unified formalism for algebraic globular higher categories. The latter are very common, since they include all the globular higher categories defined by a set of operations and equations between them. Moreover, the instances of such higher categories form locally finitely presentable categories and, as such, have very good properties, like being complete and cocomplete [START_REF] Adámek | Locally Presentable and Accessible Categories[END_REF]. The setting of Batanin then enables one to derive several common constructions for such higher categories. In particular, one can generalize to those the notion of polygraph, which can be thought as higher-dimensional signatures, originally defined by Street [START_REF] Street | Limits indexed by category-valued 2-functors[END_REF] for strict 2-categories and Burroni for strict ω-categories. Batanin moreover showed that there is an adjunction between n-polygraphs and n-categories, which is "most of the time" monadic (as proved by Street for 2-polygraphs of strict categories), allowing for presenting higher categories of this framework using polygraphs.

Although this is already valuable, it seems that the work of Batanin can be refined in several aspects. First, several constructions of interest for concrete applications are too implicit, if not absent of Batanin's treatment. For example, in the context of higher dimensional rewriting, one is usually interested in a notion intermediate to higher category and polygraph, called cellular extension, which is simply a higher category with a set of generators in the next dimension. One can then consider the free (n+1)-category obtained from an n-cellular extension by freely generating the (n+1)-cells from the set of generators. Thus, cellular extensions can be considered as a more flexible construction than the one on polygraphs, where each dimension has to be freely generated.

Second, in order to use the results of Batanin, one has to work directly with a monad and its Eilenberg-Moore category. However, one usually does not have direct access to the underlying monad of the considered theory of higher category, but only the operations of the theory together with the equations satisfied by the theory, from which one can derive a monad, but the description of the latter can be very tedious [START_REF] Penon | Approche polygraphique des ∞-catégories non strictes[END_REF]. Instead, one would prefer results that can work directly with the equational theory, the category of models of this theory, and the straight-forward functors that one can build from it. In particular, such a shortcut feels particularly desirable for showing the truncability of the monad, which is required for the constructions and properties of Batanin to work.

Third, it seems that deeper understanding about globular algebras can be gained by seeing them through the lenses of the formal theory of monads of Street [START_REF] Street | The formal theory of monads[END_REF]. Indeed, several natural constructions on globular algebras, like truncations functors and their right adjoints, are in fact projections, through the Eilenberg-Moore functor, of constructions happening in the category MND of monads and monad functors, whose compositions involve vertical composition of square-shaped natural transformation. Then, several computations on these functors can be nicely described using string diagrams, facilitating their readability and making them more intuitive.

In this work, we attempt to address these three points.

Outline In Section 1, we recall some elements of Street's formal theory of monads [START_REF] Street | The formal theory of monads[END_REF]. In particular, we define the category MND of monads over categories together with the Eilenberg-Moore construction, which produces a category of algebras from a monad. In Section 2, we recall Batanin's framework for globular higher categories, where theories of higher categories are simply studied as monads on globular sets, and extend it with new results and constructions. Among other, we prove two criterions (Theorem 2.5.2 and Theorem 2.7.4) which help bridge the gap between that framework and the usual definitions of higher categories as structures with operations satisfying equations. In Section 3, we recover the notion of polygraph through a different path than the one of Batanin using the intermediate and intuitive notion of cellular extensions. We also describe explicitly the free constructions associated to both notions. The adjunctions shown by Batanin between higher categories and polygraphs can then be recovered from an adjunction between cellular extensions and polygraphs (Theorem 3.4.1). Finally, in Section 4, we illustrate the use of our properties and constructions on the case of strict categories.

Acknowledgements I would like to thank all the people with whom I was able to discuss this work and who gave me useful feedback about it. In particular, I would like to thank Samuel Mimram, Tom Hirschowitz and Dominic Verity who took the time to read in depth an earlier version of this work under the form of the first chapter of my PhD thesis. The comments of Dominic were particularly valuable to this work, since he opened my eyes on some very naïve arguments I used in that earlier version, and indicated me some more natural ones. Most of the changes from the earlier version to this one can be attributed to him, so that I am grateful to him. Also, some additional thanks to Samuel Mimram for having developed satex1 that I have used to draw most of the string diagrams of this article.

Notations In this article, given n ∈ N, N n denotes the set {0, . . . , n} and N * n denotes the set {1, . . . , n}. We extend this notation to the infinity and put N ω = N and N * ω = N * . As a consequence of the above choices, we might write N n ∪{n} as a convenient abbreviation to denote either N n when n ∈ N, or N ∪ {ω} when n = ω.

1 Highlights of the formal theory of monads

In order to better manipulate globular algebras and constructions upon them, we use the formal theory of monads of Street [START_REF] Street | The formal theory of monads[END_REF], of which we recall briefly the salient points. We start by recalling the notion of algebra for a monad and the associated Eilenberg-Moore category in Section 1.1. Then, in Section 1.2, we recall that the construction of the Eilenberg-Moore category is part of an adjunction between the 2-categories MND, describing monads over categories, and CAT. Finally, in Section 1.3, we give several useful properties to build morphisms in MND from adjunctions in CAT.

In the following, we introduce monads either as (T, η, µ), where T is the endofunctor of the monad and (η, µ) is the unit-counit pair; or we introduce them as (C, T ), where C is the base category for which T is the endofunctor. When the latter notation is used, the unit and counit, when required, are introduced explicitly.

Algebras

Given a monad (T, η, µ) on a category C, a T -algebra is the data of an object X ∈ C together with a morphism h : T X → X such that

h • η X = id X and h • µ X = h • T (h).
A morphism between two algebras (X, h) and (X , h ) is given by a morphism f :

X → X of C satisfying f • h = h • T (f ).
We write C T for the category of T -algebras, also called Eilenberg-Moore category of T . There is a canonical forgetful functor U T : C T → C which maps the T -algebra (X, h) to X. This functor has a canonical left adjoint

F T : C → C T
which maps X ∈ C to the T -algebra (T X, µ X ), such that the unit of F T U T is η T = η, and the associated counit, denoted T , is such that T (X,h) = h for a given T -algebra (X, h). The monad induced by F T U T is then exactly (T, η, µ).

The category MND

Given two monads (S, γ, ν) and (T, η, µ) on two categories C and D respectively, a monad functor betweem (S, γ, ν) and (T, η, µ) is the data of a functor F : C → D together with a natural transformation α : T F ⇒ F S such that α • (ηF ) = F γ and α • (µF ) = (F ν) • (αS) • (Sα).

A monad functor transformation (often abbreviated truncable monads) between two monad functors (F, α), (G, β) : (C, S) → (D, T ) is a natural transformation m : F ⇒ G such that is mapped by EM to the natural transformation F α ⇒ G β whose component at an S-algebra (X, h) is m X . The component of the counit of the adjunction at a monad (C, T ) is given by (U T , U T T ). Moreover, the monad functor (T, µ) : (C, 1) → (C, T ) corresponds to the functor

(mS) • α = β • (T m).
F T : C → C T by the adjunction Inc EM.
There is also a forgetful functor

Und : MND → CAT
which maps a monad (C, T ) to C and whose action on monad functors and monad transformations is the expected one. We mention that this functor is left adjoint to Inc, even though this is not really useful for our purposes.

Morphisms of MND from adjunctions

We give several results that allows building morphisms of MND from adjunctions. First, we prove that every functor which is a right adjoint can be lifted canonically to MND: where T = (T, η T , µ T ) is the canonical monad with T = RSL and is the counit of L R.

Proof. The fact that we obtain a monad functor can readily be verified using string diagrams. For example, the equation (RS ) • (η T R) = Rη S asserts that the two diagrams

R S L R and R S
represents the same natural transformation, which is true by the zigzag equations for L R.

The other equation (RS )

• (µ T R) = (Rµ S ) • (RS S) • (T RS ) is verified similarly.
We are now left to prove the cocartesianness of (R, RS ). So let (D , T ) be a monad, U : C → D and Ū : D → D such that U = Ū R, and (U, α) : (C, S) → (D , T ) be a monad functor. We define ᾱ :

T Ū ⇒ Ū T by ᾱ = T Ū R L = U α U S = Ū R = Ū T
and verify that it defines a monad functor ( Ū , ᾱ) : (D, T ) → (D , T ). We start with the unit equation, i.e., ᾱ

• (η T Ū ) = Ū η T : Ū R L = T U α U S = Ū R = Ū T = Ū R L = U = S Ū R = Ū T = Ū R S L = Ū T = Ū Ū T .
The second equation, i.e., ᾱ • (µ T Ū ) = ( Ū µ S ) • (ᾱT ) • (T ᾱ), is proved in Figure 1. Thus, we conclude that ( Ū , ᾱ) is a monad functor. We verify that it is a factorization of (U, α) through (R, RS ):

T Ū R R L = U α U S = Ū R = T RS Ū R S = T Ū R R L = U α U S = Ū R S = T Ū R = U α U S = Ū R S .
Moreover, by the zigzag equations, we observe that the vertical pasting operation

D D D D T Ū ⇓ β T Ū → C D D C D D R S ⇓ RS T Ū ⇓ β T R Ū T T Ū R L = T U α U S = Ū R = Ū T = T T Ū R L = U α U S α U S = S Ū R = Ū T = T T Ū R L = U α U S = Ū R = U α U S = S Ū R = Ū T = T T Ū ᾱ Ū T = Ū R S L = U α U S = S Ū R = Ū T = T T Ū ᾱ Ū T R L = U α = U S R S L = Ū R S = Ū T = T T Ū ᾱ Ū T ᾱ Ū T Ū T Figure 1: Proof of ᾱ • (µ T Ū ) = ( Ū µ S ) • (ᾱT ) • (T ᾱ).
is a bijective operation between natural transformations of adequate types, whose inverse is β → (β L) • (T Ū η) where η is the unit of L R. Thus, we conclude that ( Ū , ᾱ) is the unique monad functor above Ū which factors (U, α) through (R, RS ). Thus, the latter is a cocartesian morphism for Und.

Remark 1.3.2. The morphism of Proposition 1.3.1 is even 2-cocartesian, meaning that given a monad transformation θ : (U, α) ⇒ (U , α ) : (D, T ) → (D , T ) and θ : Ū ⇒ Ū such that θR = θ, then θ uniquely lifts through Und to a monad modification θ : ( Ū , ᾱ) ⇒ ( Ū , ᾱ ) which factors θ seen as a monad modification through (R, RS ). The proof that θ induces a monad transformation is done by observing that the bijection introduced in the end of the proof of Proposition 1.3.1 generalizes to a bijection

D D D D T Ū ⇓ β T Ū → C D C D S U ⇓ β T U .
Then, the equation required for θ to be a monad transformation is given by the one of θ, through this bijection.

Given a situation as in the statement of Proposition 1.3.1, we might wonder whether the adjunction L R lifts to an adjunction in MND. In fact, we can ask this question in a more general setting: given (C, S) and (D, T ) two objects of MND and (R, ρ)

: (C, S) → (D, T ) ∈ MND such that R = Und(R, ρ) is part of an adjunction L
R, when does this adjunction lift to an adjunction in MND, i.e., there exists λ : SL ⇒ LT such that (L, λ) (R, ρ) in MND?

Given the situation just described, consider the natural transformation ρ * : LT ⇒ SL, also called the mate [START_REF] Kelly | Review of the elements of 2-categories[END_REF] of ρ, defined by

ρ * = L T R L ρ R S
.

We then have the following property: (ii) the natural transformation ρ * is an isomorphism.

Proof. We first show that (i) implies (ii). So let λ be as in (i). We prove that λ is an inverse for ρ * . We start by showing that λ • ρ * = id LT . By the correspondence given by the adjunction L R, it is equivalent to show that (R(λ

• ρ * )) • (ηT ) = ηT . From the fact that (L, λ) (R, ρ)
is an adjunction, we get in particular the following equality

D C D D C D L T 1D ⇓ λ R S ⇓ ρ T L R ⇓ η = D D D D C 1D T = T 1D L R ⇓ η (1)
from which we can prove the wanted equality as follows:

R L T R L ρ R S λ R L T = T R L ρ R S λ R L T = T R L T .
Symmetrically, in order to prove that ρ * • λ = id SL , it is equivalent to prove that

(S ) • ((ρ * • λ)R) = S .
In order to prove the latter, we use the equality satisfied by as a monad transformation:

C D C C D C R S ⇓ ρ L T ⇓ λ S R 1C L ⇓ = D C C C C L 1C S = R S 1C ⇓ . ( 2
)
Then, the wanted equality can be proved using string diagrams just as before. Thus, (ii) is proved.

Conversely, assume that (ii) holds. We put λ = (ρ * ) -1 and show that (L, λ) is a monad functor. First, we need to show that λ • (η S L) = (Lη T ), or equivalently, that (η S L) = ρ * • (Lη T ). We show the latter using string diagrams:

L T R L ρ R S = L R L S L = L S L
.

Second, we need to show that λ • (µ S L) = (Lµ T ) • (λT ) • (Sλ), or equivalently, that the equation

(µ S L) • (Sρ * ) • (ρ * T ) = ρ * • (Lµ T ) holds.
We show the latter using string diagrams again:

L T R L T ρ R S R L ρ R S S L = L T T R L ρ R S ρ R S S L = L T T T R L ρ R S S L
.

Thus, (L, λ) is a monad functor. We must now prove that η and induce monad transformations. First, we show that (1) holds, or equivalently, that

D C D C D L 1D R S ⇓ ρ T R ⇓ η = D D D C C D T L ⇓ ρ * 1D L ⇓ η 1D S R
.

But the latter equation follows directly from the string diagram definition of ρ * and the zigzag equations of the adjunction L R.

The other required equation ( 2), or equivalently,

C D C D C R S ⇓ ρ T R 1C L ⇓ = C D D C C C R 1C ⇓ T L ⇓ ρ * L 1C S
holds by a similar argument. Finally, the zigzag equations for η and seen as monad transformations follows from the zigzag equations satisfied by them as natural transformation in CAT.

Hence, (i) holds.

We have the same kind of property for left adjoints (first suggested by Dominic Verity to the author): (ii) the natural transformation λ is an isomorphism.

Proof. The proof is essentially the same as the one for Proposition 1.3.3. For (ii) implies (i), ρ is now defined by the string diagram

ρ = R L T R λ -1 S L
and we prove just as before that it induces a monad functor (R, ρ) such that (L, λ) (R, ρ) is an adjunction in MND.

Proposition 1.3.5. Given two adjunctions L R and L R, in the configuration

C D E L R L R ,
if we write S for the monad associated with L R and T for the monad associated with LL R R, and η for the unit of L R, we have a monad functor

(1 C , RηL) : (C, T ) → (C, S).
Proof. The fact that it is a monad functor can be checked using string diagrams. On the one hand, the compatibility of RηL with the units of S and T asserts that the two diagrams

U Ū L L = T
and T represents the same cell, which is true by definition of the unit of T . On the other hand, the compatibility of RηL with the multiplications of S and T asserts that the two diagrams

S S = R L R L R R L L = T and S S = R L R L R L R L R R L L = T
represents the same cell, which is true by the zigzag equations of L R. Thus, (1 C , RηL) is indeed a monad functor.

Higher categories as globular algebras

The notion of "higher category" encompasses informally all the structures that have higherdimensional cells which can be composed together with several operations. Such structures can differ on many points. First, there are several possible shapes for the cells of higher categories. For example, globular higher categories have 0-cells, 1-cells, 2-cells, 3-cells, etc. of the form

x, x y f , x y f g ⇓ φ , x y f g φ ⇓ F ≡ ⇓ ψ , etc.
But one can consider higher categories with other shapes than the globular ones. Common variants include cubical [START_REF] Fahd | Multiple categories: the equivalence of a globular and a cubical approach[END_REF] and simplicial [START_REF] Joyal | Quasi-categories and Kan complexes[END_REF] higher categories, whose 2-cells for example are respectively of the form

x y x y f g ⇓ φ h f and y x z g f h ⇓ φ .
Moreover, higher categories have several operations which satisfy axioms that can take different forms, according to their position in the strict/weak spectrum. For example, a strict 2-category is a globular 2-dimensional category that have, among others, an operation * 0 to compose 1-cells in dimension 0, as in

x y f * 0 y z g = x z f * 0 g
, and operations * 0 and * 1 to compose 2-cells in dimensions 0 and 1 respectively, as in

x y f g ⇓ φ * 0 y z f g ⇓ φ = x z f * 0 f g * 0 g ⇓ φ * 0 φ and x y f g ⇓ φ * 1 x y g h ⇓ ψ = x y f h ⇓ φ * 1 ψ .
These operations are required to satisfy several axioms consisting in equalities, like the associativity axiom: given 0-composable 1-or 2-cells u, v, w,

(u * 0 v) * 0 w = u * 0 (v * 0 w)
and, given 1-composable 2-cells φ, ψ, χ,

(φ * 1 ψ) * 1 χ = φ * 1 (ψ * 1 χ
). An example of a weak higher category is given by a bicategory, which is a globular 2-dimensional category that has operations similar to a strict 2-category but which satisfy axioms in the form of "weak equalities". For example, the 0-composition of 1-cells is only required to be weakly associative, in the sense that, given 0-composable 1-cells

w x y z f g h
, the equality (f * 0 g) * 0 h = f * 0 (g * 0 h) does not hold necessarily, but there should exist a coherence cell between the two sides, i.e., an invertible 2-cell α f,g,h as in w z

(f * 0 g) * 0 h f * 0 (g * 0 h) ⇓ α f,g,h .
Finally, a subtle difference between the different kinds higher categories is the algebraicity of their definition [START_REF] Leinster | Higher Operads, Higher Categories[END_REF][START_REF] Gurski | Coherence in Three-Dimensional Category Theory[END_REF]. This notion essentially pertains to weak higher categories. Informally, a definition of some sort of higher categories is algebraic when it can be equivalently described by means of a monad. Concretely, algebraic definitions of weak higher categories involve coherence cells that are distinguished (like the definition of bicategories, which requires that "there exists an invertible 2-cell α f,g,h between (f * 0 g) * 0 h and f * 0 (g * 0 h)"), whereas non-algebraic definitions of weak higher categories involve coherence cells that are not (a non-algebraic definition of bicategories would only require that "there exists some invertible 2-cell between (f * 0 g) * 0 h and f * 0 (g * 0 h)").

In the remainder of this article, we will restrain our attention to globular algebraic higher categories. A particular theory of k-categories can be seen as a monad on the category of k-globular sets, and a k-category instance of this theory is an algebra for this monad. A lot of globular higher categories that one usually encounters fit in this setting: strict k-categories, bicategories, Gray categories, etc. Several constructions can then be defined at this level of abstractions, like the truncation of globular algebras and its left adjoint.

In Section 2.1, we recall the definition of globular sets and elementary operations on them. We then introduce globular algebras as algebras of a monad on globular sets in Section 2.2, and then define the truncation and inclusion functors which relate globular algebras from different dimensions in Section 2.3. Then, in the case of a monad on Glob ω , we use the truncation functors to formally express Alg ω as a (bi)limit over the Alg k 's in Section 2.4. In Section 2.5, we introduce a criterion to recognize a tower of categories as equivalent to the categories of globular algebras over a monad, simplifying the concrete use of the theory developped in this article. In Section 2.6, we introduce the notion of truncable monads, which correspond more to the notions of higher categories that we are accustomed to than general globular monads, and, in Section 2.7, we prove a criterion to easily recognize such monads in the wild.

Globular sets and operations

Here, we recall the classical notion of globular set. It is the underlying structure of a globular higher category which describes globes of different dimensions together with their sources and targets. We moreover define the truncation and inclusion functors between globular sets of different dimensions.

Definition Given n ∈ N ∪ {ω}, an n-globular set (X, ∂ -, ∂ + ) (often simply denoted X) is the data of sets X k for k ∈ N n together with functions ∂ - i , ∂ + i : X i+1 → X i for i ∈ N n-1 as in X 0 X 1 X 2 • • • X k X k+1 • • • ∂ - 0 ∂ + 0 ∂ - 1 ∂ + 1 ∂ - 2 ∂ + 2 ∂ - k-1 ∂ + k-1 ∂ - k ∂ + k ∂ - k+1 ∂ + k+1 such that ∂ - i • ∂ - i+1 = ∂ - i • ∂ + i+1 and ∂ + i • ∂ - i+1 = ∂ + i • ∂ + i+1 for i ∈ N n-1 .
When there is no ambiguity on i, we often write ∂ -and ∂ + for ∂ - i and ∂ + i . An element u of X i is called an i-globe of X and, for i > 0, the globes ∂ - i-1 (u) and ∂ + i-1 (u) are respectively called the source and target and u. Given n-globular sets X and Y , a morphism of n-globular set between X and Y is a family of functions

F = (F k : X k → Y k ) k∈Nn , such that ∂ - i • F i+1 = F i • ∂ - i for i ∈ N n-1 .
We write Glob n for the category of n-globular sets.

Remark 2.1.1. The above definition directly translates to an essentially algebraic theory, so that Glob n is essentially algebraic. In particular, Glob n is locally finitely presentable, complete and cocomplete by Theorem A.2.1 and Proposition A.1.7.

For ∈ {-, +} and j ≥ 0, we write

∂ i,j = ∂ i • ∂ i+1 • • • • • ∂ i+j-1
for the iterated source (when = -) and target (when = +) operations. We generally omit the index j when there is no ambiguity and simply write ∂ i (u) for ∂ i,j (u). Given i, k, l ∈ N n with i < min(k, l), we write X k × i X l for the pullback

X k × i X l X l X k X i ∂ - i ∂ + i . Given p ≥ 2 and k 1 , . . . , k p ∈ N n , a sequence of globes u 1 ∈ X k 1 , . . . , u p ∈ X kp is said i-com- posable for some i < min(k 1 , . . . , k p ), when ∂ + i (u j ) = ∂ - i (u j+1 ) for j ∈ N * p-1 . Given k ∈ N n and u, v ∈ X k , u and v are said parallel when k = 0 or ∂ k-1 (u) = ∂ k-1 (v) for ∈ {-, +}.
To remove the side condition k = 0, we use the convention that X -1 is the set { * } and that

∂ - -1 , ∂ + -1 are the unique function X 0 → X -1 . For u ∈ X i+1 , we sometimes write u : v → w to indicate that ∂ - i (u) = v and ∂ + i (u) = w.
In low dimension, we use n-arrows such as ⇒, , , etc. to indicate the sources and the targets of n-globes in several dimensions. For example, given a 2-globular set X and φ ∈ X, we sometimes write φ :

f ⇒ g : x → y to indicate that φ ∈ X 2 , ∂ - 1 (φ) = f, ∂ + 1 (φ) = g, ∂ - 0 (φ) = x and ∂ + 0 (φ) = y.
We also use these arrows in graphical representations to picture the elements of a globular set X.

For example, given an n-globular set X with n ≥ 2, the drawing

x y z f g h ⇓ φ ⇓ ψ k (3)
figures two 2-cells φ, ψ ∈ X 2 , four 1-cells f, g, h, k ∈ X 1 and three 0-cells x, y, z ∈ X 0 such that

∂ - 1 (φ) = f, ∂ + 1 (φ) = ∂ - 1 (ψ) = g, ∂ + 1 (ψ) = h, ∂ - 0 (f ) = ∂ - 0 (g) = ∂ - 0 (h) = x, ∂ + 0 (f ) = ∂ + 0 (g) = ∂ + 0 (h) = ∂ - 0 (k) = y, ∂ + 0 (k) = z.
Truncation and inclusion functors Given m ∈ N n and X ∈ Glob n , we denote by X ≤m the m-truncation of X, i.e., the m-globular set obtained from X by removing the i-globes for i ∈ N n with i > m. This operation extends to a functor (-) Glob ≤m,n : Glob n → Glob m often denoted (-) Glob ≤m when there is no ambiguity. This functor admits a left adjoint (-) Glob ↑n,m : Glob m → Glob n often denoted (-) Glob ↑n when there is no ambiguity, and which maps an m-globular set X to the n-globular set X ↑n , called n-inclusion of X, and which is defined by (X ↑n ) ≤m = X and (X ↑n ) i = ∅ for i ∈ N n with i > m. The unit of the adjunction (-) Glob ↑n (-) Glob ≤m is the identity and the counit is the natural transformation denoted i m,n , or simply i m when there is no ambiguity, which is given by the family of canonical morphisms i m X : (X ≤m ) ↑n → X for X ∈ Glob n . The functor (-) Glob ≤m,n also admits a right adjoint (-) Glob ⇑m,n : Glob m → Glob n denoted (-) Glob ⇑n when there is no ambiguity, and which maps an m-globular set to the n-globular set X ⇑n defined by (X ⇑n ) ≤m = X, and, for i ∈ N n with i > m,

(X ⇑n ) i = {(u, v) ∈ X m | u and v are parallel} such that, for (u, v) ∈ (X ⇑n ) i , ∂ - m ((u, v)) = u and ∂ + m ((u, v)) = v and ∂ - j ((u, v)) = ∂ + j ((u, v)) = (u, v) for j ∈ N i-1 .
Note that, since they are left adjoints, the functors (-) Glob ↑n,m and (-) Glob ≤m,n preserves colimits.

Globular algebras

We now introduce categories of globular algebras, i.e., the Eilenberg-Moore categories induced by monads on globular sets, as were first introduced by Batanin in [START_REF] Michael | Computads for finitary monads on globular sets[END_REF]. We moreover give several additional constructions and properties on these objects.

Let n ∈ N ∪ {ω} and (T, η, µ) be a finitary monad on Glob n . We write Alg n for the category of T -algebras Glob T n and

U n : Alg n → Glob n F n : Glob n → Alg n
for the induced left and right adjoints, that were denoted U T and F T in Section 1: given an algebra (X, h) ∈ Alg n , the image of (X, h) by U n is X and, given

Y ∈ Glob n , F n Y is the free T -algebra (T Y, µ Y : T T Y → T Y ).
Given k < n, using Proposition 1.3.1 with the adjunction (-) Glob ≤k (-) Glob ↑n , we get a monad

(T k , η k , µ k ) on Glob k where T k = (-) Glob ≤k T (-) Glob ↑n and such that η k : id Glob k → T k is the composite id Glob k (-) Glob ≤k (-) Glob ↑n T k (-) Glob ≤k η(-) Glob ↑n i.e., η k X = (η X ↑n ) ≤k for X ∈ Glob k , and such that µ k : T k T k → T k is the composite T k T k (-) Glob ≤k T T (-) Glob ↑n T k (-) Glob ≤k T i k T (-) Glob ↑n (-) Glob ≤k µ(-) Glob ↑n .
So, for k ∈ N n , we get a category Alg k = Glob T k k , and canonical functors

U k : Alg k → Glob k F k : Glob k → Alg k defined like U n and F n above, forming an adjunction F k U k whose counit is denoted k . The objects of Alg k are called k-categories. Moreover, given a k-category C = (X, h), the elements of X i are called the i-cells of C for i ∈ N k .
Remark 2.2.1. In the above definition, we require that the monad (T, η, µ) is finitary in order to prove later the existence of several free constructions on the k-categories. This is not too restrictive, since it includes all the monads of algebraic globular higher categories that have operations with finite arities, i.e., most theories of algebraic globular higher categories. We can already derive several properties of the categories Alg k :

Proposition 2.2.2. For k ∈ N ∪ {n}, the category Alg k is locally finitely presentable. In particular, it is complete and cocomplete. Moreover, the functor U k preserves and creates directed colimits, and creates limits.

Proof. The category Alg k is locally finitely presentable as a consequence of Proposition A. This monad maps a 1-globular set G to the underlying 1-globular set of the category of paths on G seen as a graph. Using Beck's monadicity theorem (Theorem 4.2.1), one can verify that the functor Cat → Glob 1 is monadic, so that Alg 1 Cat. Moreover, the monad (T 0 , η 0 , µ 0 ) is essentially the identity monad on Glob 0 , and thus Alg 0 Set. More generally, we will see in Section 4 that the monads of strict k-categories for k ∈ N are derived from the monad of strict ω-categories. Example 2.2.4. We define a notion of weird 2-category as follows: a weird 2-category is a 2-globular set C equipped with an operation * :

C 2 × C 2 → C 0 .
Note that we do not require the composability of the arguments of * , and we do not enforce any axiom on * . A morphism between two weird 2-categories is then a morphism between the underlying 2-globular sets that is compatible with * . The category Weird of weird 2-categories and their morphisms is essentially algebraic, and the functor which maps a weird 2-category to its underlying 2-globular set is induced by an essentially algebraic theory morphism, so that it is a right adjoint and finitary by Theorem A.2.5. From the adjunction, we derive a finitary monad (T, η, µ) on Glob 2 , and, given X ∈ Glob 2 , we have that

(T X) 0 ∼ = X 0 (X 2 × X 2 ) (T X) 1 ∼ = X 1 (T X) 2 ∼ = X 2
so that, for Alg 2 derived from the monad T , Alg 2 ∼ = Weird. Moreover, the monads (T 0 , η 0 , µ 0 ) and (T 1 , η 1 , µ 1 ) are essentially the identity monads on Glob 0 and Glob 1 respectively, so that the associated notions of weird 0-and 1-categories are simply 0-and 1-globular sets.

The previous example moreover illustrates the unusual operations that notions of higher categories defined in the setting of Batanin can have. It is also an example of a monad on globular sets which is not truncable (c.f. Example 2.6.2). Example 2.2.5. Monoids can be considered in any category with a monoidal structure. Given a theory of globular algebraic higher category, one can define an associated notion of strict monoidal higher category by considering monoids in the category of algebras, choosing the monoidal structure to be the cartesian one. Monadically, we have an operation mapping a monad T on n-globular sets to a monad T on n-globular sets representing the theory of strictly monoidal higher categories which are instances of T . This operation can be seen to preserve a finitary hypothesis on T .

Truncation and inclusion functors

We now introduce truncation and inclusion functors between the categories Alg k together with some of their properties.

Let n ∈ N ∪ {ω} and (T, η, µ) be a finitary monad on Glob n . Given k < n, using Proposition 1.3.1, we get that (-) Glob ≤k,n lifts to a cocartesian morphism

(Glob n , T ) ((-) Glob ≤k ,(-) Glob ≤k T i k ) -------------→ (Glob k , T k )
with respect to the functor Und. By applying EM, we get a functor (-) Alg ≤k,n : Alg n → Alg k also denoted (-) Alg ≤k when there is no ambiguity. Now, given k, l ∈ N with k < l < n, since (-) Glob ≤k,n can be factored as (-) Glob ≤k,l (-) Glob ≤l,n , the cocartesianness of ((-) Glob ≤l , (-) Glob ≤l T i l ) ensures that there is a unique morphism (F, α) which factorizes ((-) Glob ≤k , (-

) Glob ≤k T i k ) through ((-) Glob ≤l , (-) Glob ≤l T i l ) in MND. Lemma 2.3.1. Given k, l ∈ N with k < l < n, the morphism ((-) Glob ≤k,l , (-) Glob ≤k T l i k,l ) : (Glob l , T l ) → (Glob k , T k ) is the factorization of ((-) Glob ≤k , (-) Glob ≤k T i k ) through the cocartesian morphism ((-) Glob ≤l , (-) Glob ≤l T i l ).
Proof. By Proposition 1.3.1, there is a morphism

((-) Glob ≤k,l , (-) Glob ≤k T l i k,l ) : ((-) Glob ≤l , T l ) → ((-) Glob ≤k , T )
where (T , η , µ ) is the monad on (-) Glob ≤k defined by

T = (-) Glob ≤k T l (-) Glob ↑l η = (-) Glob ≤k η l (-) Glob ↑l µ = ((-) Glob ≤k µ l (-) Glob ↑k ) • ((-) Glob ≤k T l i k,l T l (-) Glob ↑l ).
By a straight-forward computation, we get T = T k , η = η k and µ = µ k . To verify that the above morphism is the wanted factorization, we are left to check that

((-) Glob ≤k,l , (-) Glob ≤k T l i k,l ) • ((-) Glob ≤l , (-) Glob ≤l T i l ) = ((-) Glob ≤k , (-) Glob ≤k T i k ) in MND. But it is straight-forward too, since i l,n •((-) Glob ↑l,n i k,l (-) Glob ≤l,n ) = i k,n .
By applying EM to the factorization morphism given by Lemma 2.3.1, we get a functor (-) Alg ≤k,l : Alg l → Alg k also denoted (-) Alg ≤k when there is no ambiguity. Concretely, given a T l -algebra

(X, h : T l X → X),
its image by (-) Alg ≤k is the T k -algebra (X ≤k , h ), where h is defined as the composite

T k (X ≤k ) (T l X) ≤k X ≤k ((-) Glob ≤k,l T l i k,l ) X h ≤k .
The image of (X, h) in Alg l by (-) Alg ≤k is called the k-truncation of (X, h) and we denote it (X, h) ≤k . Note that the image of a morphism f : (X, h) → (X , h ) by (-) Alg ≤k is f ≤k (the globular k-truncation of f ). The same concrete description holds for the functors (-) Alg ≤k,n . The definition of the truncation functors allows for the following compatibility property:

Proposition 2.3.2. Given j, k, l ∈ N n ∪ {n} with j < k < l, we have (-) Alg ≤j,k • (-) Alg ≤k,l = (-) Alg ≤j,l .
Proof. The two morphisms

((-) Glob ≤j,k , (-) Glob ≤j T k i j,k ) • ((-) Glob ≤k,l , (-) Glob ≤k,l T l i k,l ) and ((-) Glob ≤j,l , (-) Glob ≤j,l T l i j,l )
provide a factorization of ((-) Glob ≤j,n , (-) Glob ≤j,n T i j,n ) through the cocartesian morphism

((-) Glob ≤l,n , (-) Glob ≤l,n T i l,n ).
Thus, they are equal. The conclusion follows from the functoriality of EM.

The finitary assumption on T enables the existence of a left adjoint to truncation functors:

Proposition 2.3.3. Given k, l ∈ N n ∪ {n} with k < l, the functor (-)
Alg ≤k,l is finitary and admits a left adjoint.

Proof. By the adjunction Inc EM, we have a commutative diagram

Alg l Alg k Glob l Glob k (-) Alg ≤k U l U k (-) Glob ≤k .
The functor (-) Alg ≤k,l is finitary since, by Proposition 2.2.2, U k creates directed colimits and the functor U k (-) Alg ≤k,l = (-) Glob ≤k U l preserves directed colimits. Moreover, (-) Alg ≤k,l preserves limits since U k creates limits and the functor U k (-) Alg ≤k,l = (-) Glob ≤k U l preserves limits (both (-) Glob ≤k,l and U l are right adjoints). Then, by Proposition A.1.8, the functor (-) Alg ≤k,l admits a left adjoint.

Given k, l ∈ N n ∪ {n} with k < l, we write

(-) Alg ↑l,k : Alg k → Alg l
for the left adjoint to (-) Alg ≤k,l , or even (-) Alg ↑l when there is no ambiguity on k. The image of (X, h) in Alg k by (-) Alg ↑l is called the l-inclusion of (X, h) and we denote it (X, h) ↑l .

Alg ω as a limit

Let (T, η, µ) be a finitary monad on Glob ω . The purpose of this paragraph is to characterize Alg ω as a limit on the categories Alg k for k ∈ N using the truncation functors (-) Alg ≤k . Proposition 2.4.1. The cone

((Glob ω , T ), ((-) Glob ≤k , (-) Glob ≤k T i k ) k∈N )
is a limit cone in MND on the diagram

(Glob 0 , T 0 ) (Glob 1 , T 1 ) (Glob 2 , T 2 ) (Glob 3 , T 3 ) • • • (-) Glob ≤0 (-) Glob ≤1 (-) Glob ≤2 (-) Glob ≤3
where we abbreviated by (-) Glob ≤k the monad functor ((-) Glob ≤k , (-) Glob ≤k T k+1 i k ) for k ∈ N for readability.

Proof. We already know that it is a cone by Lemma 2.3.1. Let us prove that it is a limit cone in MND (seen here as a 1-category).

Let (C, S) be a monad and

((Γ k , γ k ) : (C, S) → (Glob k , T k )
) k∈N be a cone on the diagram of the statement. By forgetting the 2-cells, we get a cone (Γ k : C → Glob k ) k and thus a functor Γ : C → Glob ω . In order to get a monad functor, we still need to build a 2-cell γ :

T Γ ⇒ ΓS. Such a 2-cell is the data of morphisms γ X : T ΓX → ΓSX for X ∈ C. Write R k for R k = (-) Glob ↑ω (-) Glob ≤k : Glob ω → Glob ω
and j k for the natural transformation

j k = (-) Glob ↑ω i k,k+1 (-) Glob ≤k+1 : R k ⇒ R k+1 . Note that, for all Y ∈ Glob ω , (i k,ω Y : R k Y → Y ) k∈N is a colimit cocone in Glob ω on the diagram R 0 Y R 1 Y • • • R k Y R k+1 Y • • • j 0 Y j 1 Y j k-1 Y j k Y j k+1 Y Since T is finitary, ((T i k,ω ) Y : T R k Y → T Y ) k∈N is a colimit cocone on the diagram T R 0 Y T R 1 Y • • • T R k Y T R k+1 Y • • • (T j 0 ) Y (T j 1 ) Y (T j k-1 ) Y (T j k ) Y (T j k+1 ) Y
In particular, the sought morphisms γ X are uniquely characterized by the cocone

((γ • (T i k,ω Γ)) X : T R k ΓX → ΓSX) k∈N
on the above diagram, where we put Y = ΓX. Using some rephrasing, we have a limit cone

((T i k,ω Γ) * : Hom(T Γ, ΓS) → Hom(T R k Γ, ΓS)) k∈N on the diagram Hom(T R 0 Γ, ΓS) Hom(T R 1 Γ, ΓS) Hom(T R 2 Γ, ΓS) • • • (T j 0 Γ) * (T j 1 Γ) * (T j 2 Γ) *
On the other hand, given a pair of functors G, G : C → Glob ω , every natural transformation α : G ⇒ G is uniquely characterized by the projections (-) Glob ≤k α for k ∈ N. In other words, we have a limit cone

((-) Glob ≤l : Hom(G, G ) → Hom((-) Glob ≤l G, (-) Glob ≤l G ) l∈N on the diagram Hom((-) Glob ≤0 G, (-) Glob ≤0 G ) Hom((-) Glob ≤1 G, (-) Glob ≤1 G ) Hom((-) Glob ≤2 G, (-) Glob ≤2 G ) • • • (-) Glob ≤0 (-) Glob ≤1 (-) Glob

≤3

By combination of the two limit diagrams, we have that Hom(T Γ, ΓS) is limit cone on the diagram . . . . . .

• • • Hom((-) Glob ≤l+1 T R k Γ, (-) Glob ≤l+1 ΓS) Hom((-) Glob ≤l+1 T R k+1 Γ, (-) Glob ≤l+1 ΓS) • • • • • • Hom((-) Glob ≤l T R k Γ, (-) Glob ≤l ΓS) Hom((-) Glob ≤l T R k+1 Γ, (-) Glob ≤l ΓS) • • • . . . . . . (-) Glob ≤l+1 (-) Glob ≤l+1 (j k-1 ) * (-) Glob ≤l (j k ) * (-) Glob ≤l (j k+1 ) * (-) Glob ≤l-1 (j k-1 ) * (j k ) * (-) Glob ≤l-1 (j k+1 ) *
expressed on the category (N × N, ≤ × ≤) op . By finality of the diagonal functor

(N, ≤) op → (N × N, ≤ × ≤) op ,
Hom(T Γ, ΓS) is in fact a limit cone on the diagram

Hom((-) Glob ≤0 T R 0 Γ, (-) Glob ≤0 ΓS) Hom((-) Glob ≤1 T R 1 Γ, (-) Glob ≤1 ΓS) Hom((-) Glob ≤2 T R 2 Γ, (-) Glob ≤2 ΓS) • • •
One can check that a compatible sequence for this diagram is precisely given by the γ k for k ∈ N. Indeed, it is a consequence of the fact that ((Γ k , γ k )) k∈N is a cone. Thus, we get γ :

T Γ ⇒ ΓS such that ((-) Glob ≤k γ) • ((-) Glob ≤k T i k,ω Γ) = γ k
and γ is uniquely defined by this property. Thus, we have the uniqueness of a factorizing (Γ, γ) in MND for the cone we started from. We are left to show that (Γ, γ) is indeed a monad functor for existence.

Let's prove the first required equality, i.e., γ • (η T Γ) = Γη S . By an argument similar to the one we used above, it is enough to prove that

((-) Glob ≤k γ) • ((-) Glob ≤k η T Γ) • ((-) Glob ≤k i k,ω Γ) = ((-) Glob ≤k Γη S ) • ((-) Glob ≤k i k,ω Γ)
for every k ∈ N. We compute that

((-) Glob ≤k γ) • ((-) Glob ≤k η T Γ) • ((-) Glob ≤k i k,ω Γ) =((-) Glob ≤k γ) • ((-) Glob ≤k T i k,ω Γ) • ((-) Glob ≤k η T R k Γ) (by naturality) =γ k • ((-) Glob ≤k η T R k Γ) =γ k • (η k Γ k ) (since the unit of (-) Glob ↑ω (-) Glob ≤k is the identity) =Γ k η S =(-) Glob ≤k Γη S =((-) Glob ≤k Γη S ) • ((-) Glob ≤k i k,ω Γ) (since (-) Glob ≤k i k,ω is an identity).
In order to show the other equality, that is,

γ • (µ T Γ) = (Γµ S ) • (γS) • (T γ) (4)
we need to use twice the argument we used earlier to get that

(π k : Hom(T T Γ, ΓS) → Hom((-) Glob ≤k T R k T R k Γ, (-) Glob ≤k ΓS)) k∈N
is a limit cone on the adequate diagram, where π k is the composite

Hom(T T Γ, ΓS) Hom((-) Glob ≤k T T Γ, (-) Glob ≤k ΓS) Hom((-) Glob ≤k T R k T R k Γ, (-) Glob ≤k ΓS). (-) Glob ≤k ((-) Glob ≤k T i k T i k Γ) *
Then, using the existing equations and naturality, the reader can prove similarly as above that

((-) Glob ≤k (γ • (µ T Γ))) • ((-) Glob ≤k T i k T i k Γ) = ((-) Glob ≤k ((Γµ S ) • (γS) • (T γ))) • ((-) Glob ≤k T i k T i k Γ)
so that (4) holds and (Γ, γ) is indeed a monad functor, which moreover factorizes uniquely the cone (Γ k , γ k ) k∈N . Thus, (Glob ω , T ) is indeed a limit cone in MND as stated.

Proposition 2.4.2. ((-) Alg ≤k : Alg ω → Alg k ) k∈N is a (bi)limit cone in CAT on the diagram Alg 0 Alg 1 Alg 2 Alg 3 • • • (-) Alg ≤0 (-) Alg ≤1 (-) Alg ≤2 (-) Alg ≤3
Proof. This is a consequence of Proposition 2.4.1 and that EM is a right adjoint.

Remark 2.4.3. The above proof only show that Alg ω is a limit in the 1-categorical sense, i.e., only factorizes cones of functors by a functor (and not morphisms of cones as natural transformations, a priori). But, by a generic argument (stated for example as [23, Lemma 7.5.1]), any limit in the 1-categorical sense in CAT is also a strict 2-limit, i.e., factorizes morphisms between cones as well.

Remark 2.4.4. If we restrain our interest to weakly truncable monads (defined in Section 2.6), another proof is possible which dispenses with the specific and technical argument of Proposition 2.4.1. Indeed, writing MND psd for the sub-2-category of MND consisting of monads, pseudo monad functors and monad transformations, where a monad functor (F, φ) is said pseudo when φ is an isomorphism, we have that the underlying functor Und : MND psd → CAT, mapping a monad (C, T ) to its underlying category C, creates bilimits, and the latter are moreover preserved by the inclusion MND psd → MND (this is left as an exercise for now). Thus, a bilimit version of Proposition 2.4.1 can be deduced from the fact that Glob ω is a bilimit of the Glob k 's for k ∈ N. This argument does not apply for MND as a whole, and it is really the finitary hypothesis on T which makes Proposition 2.4.1 work.

A criterion for globular algebras

Usually, a specific notion of higher category and the associated truncation and inclusion functors are not directly derived from a monad. Instead, we often manipulate higher categories that are defined, in each dimension k ∈ N, as structures with operations satisfying some equations, and the truncation and inclusion functors are defined by hand. Such equational definitions surely induce monads on k-globular sets, but it is not immediate that the monad in dimension l 1 is obtained by truncating the monad in dimension l 2 for l 1 < l 2 , as was done earlier, nor is the equivalence between the boilerplate definitions of truncation and inclusion functors and the ones defined earlier in this section. Verifying the equivalences of these definitions is required in order to use general constructions for globular algebras, like the ones of the next section. But, without a generic argument, the verification can be tedious since it involves, among others, an explicit description of the different monads. In this section, we give a criterion, in the form of Theorem 2.5.2, to recognize that categories and functors between them are equivalent to categories of globular algebras and truncation functors derived from some monad on globular sets.

We first prove a technical lemma:

(D, R) ( C, 1) ( D, T ) ( D, S) ( D, S) Inc(T ) (U,U F,U ) (T ,T R I ,T ) ( Ū , Ū F , Ū ) (1, Ū η I,T F ) ∼
where R, S, S and T are the monads respectively derived from the adjunctions F U , F I T U , I F Ū T and F Ū , and ( D, S) → ( D, S) is the isomorphism of monads induced by T U = Ū T , and where we wrote η L,R and L,R for the unit and counit of each adjunction L R. Moreover, if the unit of the adjunction I T is an isomorphism (or, equivalently, I is fully faithful), then the morphism ( D, S) → ( D, T ) is an isomorphism.

Proof. By Propositions 1.3.1 and 1.3.5 already introduced, the morphisms shown on the diagram are indeed monad functors. We are left to check that the diagram commutes. More precisely, we need to show that pasting of 2-cells

C D D D D C D D D D U 1 = T R ⇓ T R I ,T 1 S ⇓ Ū T θ -1 1 S ⇓ Ū η I,T F T U T 1 1 is equal to C C D C C D T 1 = Ū 1 ⇓ Ū F , Ū T T Ū
where θ : F I ⇒ I F is the canonical isomorphism between the two functors which are left adjoint to Ū T = T U , defined by

θ = F I Ū T = T U I F .
We check that the wanted equality holds using string diagrams:

T T U = Ū F T I = θ -1 T U F I = T T U = Ū F T I = = T U Ū T = T T U = = Ū F Ū T = T U .
The criterion for recognizing categories and functors as categories of globular algebras and truncation functors between them is the following:

C ω Glob ω C k Glob k Uω T ω k (-) Glob ≤k,ω U k
commute for every k ∈ N. Then, there exist equivalences of categories

H ω : C ω → Alg ω and (H k : C k → Alg k ) k∈N such that C ω Alg ω C k Alg k Hω T ω k (-) Alg ≤k,ω H k and C k+1 Alg k+1 C k Alg k H k+1 T k+1 k (-) Alg ≤k,k+1 H k (5)
commute for every k ∈ N.

Remark 2.5.3. The statement of the above theorem can easily be adapted when working on a monad T on Glob n for some n ∈ N by requiring instead that

C k+1 Glob k+1 C k Glob k U k+1 T k+1 k (-) Glob ≤k,k+1
U k commutes for every k < n, and then one only gets the right commuting square of (5).

Proof. Let k ∈ N. Taking C ω , C k , Glob ω and Glob k respectively for C, C, D and D, and U ω , U k , T ω k and (-) Glob ≤k,ω respectively for U , Ū , T and T in Lemma 2.5.1, and using the adjunction Inc EM, we get a commutative square

C ω Alg ω C k Glob T k Glob S k Alg k T ω k Hω (-) Alg ≤k,ω Hk ∼ ∼
where S and T are the monads defined in the lemma. Remember that both Alg k and (-) Alg ≤k,ω

were defined using Proposition 1.3.1 so that the arrow on the right of the above diagram is indeed (-) Alg ≤k,ω . Also, H ω and Hk are equivalences since U ω and U k were supposed monadic. Finally, by the final part of Lemma 2.5.1 and the hypothesis, the middle arrow in the bottom line is an isomorphism. Thus, by defining H k to be the composition of the three morphisms on the bottom line (after inverting the second and third ones), we get the commutative diagram on the left of ( 5), and we are left to get the one on the right. Writing I k+1 ω for a left adjoint to T ω k+1 , since the unit 1 ⇒ T ω k+1 I k+1 ω is an isomorphism, it is enough to check that

(-) Alg ≤k H k+1 T ω k+1 I k+1 ω = H k T k+1 k T ω k+1 I k+1 ω . But (-) Alg ≤k H k+1 T ω k+1 I k+1 ω = (-) Alg ≤k (-) Alg ≤k+1,ω H ω I k+1 ω = (-) Alg ≤k,ω H ω I k+1 ω = H k T ω k I k+1 ω = H k T k+1 k T ω k+1 I k+1 ω
which concludes the proof.

Truncable globular monads

The general setting of higher category theories as monads over globular sets allows defining theories with unusual operations, like compositions of l-cells that produce unrelated l -cells for some l < l (c.f. Example 2.2.4). Anticipating the next section, such theories are badly behaved when it comes to freely adding new (k+1)-generators to k-categories, since the underlying k-categories will not be preserved in the process. In order not to allow such monads, we recall from [START_REF] Michael | Computads for finitary monads on globular sets[END_REF] the notion of truncable monad which forbids those problematic operations and still includes most usual theories for higher categories: those are the monads which "commute with truncation" in a suitable sense. As we will see in the nextsection, the k-categories of these theories are preserved when freely adding (k+1)-generators.

Let n ∈ N ∪ {ω} and (T, η, µ) be a finitary monad on Glob n . For k ∈ N n , remember that we used Proposition 1.3.1 to define both the monad (T k , η k , µ k ) and the cocartesian morphism

((-) Glob ≤k,n , (-) Glob ≤k T i k,n ) : (Glob n , T ) → (Glob k , T k ).
In the following, we write t k for the natural transformation (-) Glob ≤k T i k,n . The monad T is said weakly truncable when t k is an isomorphism for each k < n; it is truncable when, for each k < n, t k is the natural identity transformation (so that T k (-) Glob ≤k = (-) Glob ≤k T ). Example 2.6.1. The monad (T, η, µ) of categories on Glob 1 defined in Example 2.2.3 is weakly truncable. By choosing adequately the left adjoint Glob 1 → Cat that defines T , we can even suppose that T is truncable. More generally, we will see in Section 4.4 that the monad of strict ω-categories is weakly truncable, and even truncable up to an isomorphism of monads.

Example 2.6.2. The monad (T, η, µ) of weird 2-categories on Glob 2 defined in Example 2.2.4 is not truncable since, for X ∈ Glob 2 , we have

(T X) 0 ∼ = X 0 (X 2 × X 2 ) and (T 0 (X ≤0 )) 0 ∼ = X 0 .
The following property tells that we can always adapt a weakly truncable monad to a truncable monad:

Proposition 2.6.3. If (T, η, µ) is weakly truncable, then it is isomorphic to a monad which is truncable.

Proof. We define a truncable monad ( T , η, μ) on Glob n and an isomorphism φ : T → T from their trunctations (-) Glob ≤k T and φ ≤k : (-) Glob ≤k T → (-) Glob ≤k T and we define those using an induction on k for k ∈ N n . In dimension 0, we put

(-) Glob ≤0 T = T 0 (-) Glob ≤0 and φ 0 = (t 0 ) -1
Then, given k ∈ N n and a (k+1)-globular set X, we define ( T X) ≤k+1 as the (k+1)-globular set Y where Y ≤k = ( T X) ≤k and Y k+1 = (T k+1 (X ≤k+1 )) k+1

and the operation ∂ k : Y k+1 → Y k is defined as the composite

Y k+1 = (T k+1 (X ≤k+1 )) k+1 ∂ k -→ (T k+1 (X ≤k+1 )) k (t k+1 ) k ----→ (T X) k (φ k ) k ---→ ( T X) k
for ∈ {-, +}. Our definition extends canonically to a functor

(-) Glob ≤k+1 T : Glob n → Glob k+1 .
We also extend φ ≤k on dimension k + 1 by putting, for X ∈ Glob n ,

(φ X ) k+1 = ((t k+1 X ) -1 ) k+1 : (T X) k+1 → ( T X) k+1
So we defined T : Glob n → Glob n together with an isomorphism φ : T → T . Finally, we put

η = φ • η and μ = φ • µ • (φ -1 φ -1 )
so that ( T , η, μ) is a monad and (1, φ -1 ) : (Glob n , T ) → (Glob n , T ) a monad isomorphism. By the definition of T , we easily verify that ( T , η, μ) is truncable.

The truncability with respect to dimension n implies the truncability with respect to dimension l for any l < n: Lemma 2.6.4. If T is weakly truncable (resp. truncable), then, for every k, l ∈ N with k < l < n, (-) Glob ≤k T l i k,l is an isomorphism (resp. an identity).

Proof. We have i k,n = i k,l •((-) Glob ↑l,k i k,l (-) Glob ≤k,l ), so that

(-) Glob ≤k,n T i k,n = ((-) Glob ≤k,l (-) Glob ≤l,n T i l,n ) • ((-) Glob ≤k,l T l i k,l (-) Glob ≤l,n ).
By the 2-out-of-3 property for isomorphisms, we get that (-) Glob ≤k,l T l i k,l (-) Glob ≤l,n is an isomorphism. By precomposing with (-) Glob ↑n,l , we get that (-) Glob ≤k,l T l i k,l is an isomorphism. When T is truncable, this isomorphism is an equality.

When T is truncable, the T k , η k and µ k can be related through the equations given by the following lemma: Lemma 2.6.5. If T is truncable, then, for k, l ∈ N n ∪ {n} with k < l, we have

T k (-) Glob ≤k,l = (-) Glob ≤k,l T l and (-) Glob ≤k,l η l = η k (-) Glob ≤k,l and (-) Glob ≤k,l µ l = µ k (-) Glob ≤k,l
Proof. By Lemma 2.6.4, we have that (-) Glob ≤k T l i k,l is an identity. In particular,

T k (-) Glob ≤k,l = (-) Glob ≤k,l T l .
Moreover, from the equations satisfied by the monad functor ((-) Glob ≤k,l , (-

) Glob ≤k T l i k,l ), we deduce that (-) Glob ≤k,l η l = η k (-) Glob ≤k,l and (-) Glob ≤k,l µ l = µ k (-) Glob ≤k,l .
We now prove several properties of truncable monads regarding truncation of algebras. First, the truncation of algebras has now a simpler definition:

Proposition 2.6.6. If T is truncable, then given k, l ∈ N n ∪ {n} such that k < l, and an l-algebra (X, h) ∈ Alg l , we have (X, h) ≤k = (X ≤k , h ≤k ).

Proof. Indeed, since T is truncable, we have

((-) Glob ≤k,l T l i k,l ) X = (T k (-) Glob ≤k,l i k,l ) X = id T k X so that (X, h) ≤k = (X ≤k , h ≤k ).
Moreover, the operation of truncation of algebras is now a left adjoint:

Proposition 2.6.7. If T is truncable, then, given k, l ∈ N n ∪ {n} with k < l, the functor (-) Alg ≤k,l : Alg l → Alg k
is a left adjoint. In particular, it preserves colimits.

Proof. By Lemma 2.6.4, (-) Glob ≤k T l i k,l is an identity and in particular an isomorphism. Thus, by Proposition 1.3.4, since we have an adjunction (-) Glob ≤k,l (-) Glob ⇑l,k , this adjunction lifts canonically through Und to an adjunction

((-) Glob ≤k,l , (-) Glob ≤k T l i k,l ) ((-) Glob ⇑l,k , ρ)
for some ρ given by Proposition 1.3.4. By applying EM, we get an adjunction (-

) Alg ≤k,l (-) Alg ⇑l,k
where (-) Alg ⇑l,k = EM((-) Glob ⇑l,k , ρ).

Characterization of truncable monads

Earlier, we introduced Theorem 2.5.2 that allows recognizing that some categories and functors between them are equivalent to the categories of globular algebras and the associated truncation functors derived from a monad T on globular sets, without having to explicitly describe this monad. But, by the current definition of truncability, in order to show that the monad T is truncable, a direct proof would require to show that the natural transformations (-) Glob ≤l T i l,n are isomorphisms, so that a description of T is still needed. Below, we introduce a characterization of the truncability of T that does not rely on such tedious description.

We start by proving the following lemma, relating the functors F k : Lemma 2.7.1. Let n ∈ N ∪ {ω} and (T, η, µ) be a finitary monad on Glob n . Given k ∈ N such that k < n, we have

(-) Alg ≤k F n (-) Glob ↑n,k = F k .
Proof. By the adjunction Inc EM, it amounts to prove that the two pastings of 2-cells

Glob k Glob n Glob n Glob k Glob k Glob n Glob n Glob k (-) Glob ↑n 1 = T 1 ⇓ µ (-) Glob ≤k T ⇓ (-) Glob ≤k T i k T k (-) Glob ↑n T (-) Glob ≤k and Glob k Glob k Glob k Glob k T k 1 ⇓ µ k T k T k
are equal. But this directly follows from the definition of µ k . So the wanted equality holds. Now, we prove that truncable monads can be characterized through the associated globular algebras:

Proposition 2.7.2. Let n ∈ N ∪ {ω} and (T, η, µ) be a finitary monad on Glob n . Then, the monad (T, η, µ) is weakly truncable (resp. truncable) if and only if, for k ∈ N n-1 , the natural transformation (-

) Alg ≤k F n i k,n : F k (-) Glob ≤k ⇒ (-) Alg ≤k F n is an isomorphism (resp. an identity).
Proof. Note that the domain of (-) Alg ≤k F n i k,n is the claimed one by Lemma 2.7.1. Now, for k ∈ N n-1 , we have that

U k (-) Alg ≤k F n i k = (-) Glob ≤k U n F n i k = (-) Glob ≤k T i k .
The proposition follows from the fact that U k reflects isomorphisms (resp. identities).

We will need the following folklore property about adjunctions:

L θ L = L R L θ L R L .
Then, θ is an isomorphism if and only if θ is an isomorphism.

Proof. An inverse for θ can be straight-forwardly constructed from an inverse for θ using string diagrams, and symmetrically.

Given k ∈ N, we write j k,n : id Globn ⇒ (-) Glob ⇑n,k (-) Glob ≤k,n or simply j k , for the unit of the adjunction (-) Glob ≤k,n (-) Glob ⇑n,k : Glob k → Glob n . We can now introduce the criterion for showing the truncability of monads through their globular algebras: Theorem 2.7.4. Let n ∈ N∪{ω} and (T, η, µ) be a finitary monad on Glob n . The monad (T, η, µ) is weakly truncable if and only if, for k ∈ N n-1 , the functor (-) Alg ≤k,n has a right adjoint, that we write (-) Alg ⇑n,k , which satisfies that j k U n (-) Alg ⇑n,k is an isomorphism.

Proof. By Proposition 2.6.7, if T is weakly truncable, (-) Alg ≤k,n has a right adjoint, so we can assume that this adjoint exists and denote it by (-) Alg ⇑n,k . Then, the morphism (-) Alg ≤k F n i k , pictured by

(-) Alg ≤k F n (-) Glob ↑n (-) Glob ≤k i k
is a natural transformation between two composites of left adjoints. Then, by deriving the units and counits of these composite adjunctions (as in [17, IV. §8 Theorem 1] for example), and using (the dual of) Proposition 2.7.3, the above natural transformation is an isomorphism if and only if the natural transformation depicted by the string diagram

(-) Glob ⇑n (-) Glob ≤k U n (-) Alg ⇑n (-) Alg ≤k F n (-) Glob ↑n (-) Glob ≤k U n (-) Alg ⇑n α η n γ j k i k n α
is an isomorphism, where (α, α ), (η n , n ), (γ, i k ) are the pairs of units and counits associated with the adjunctions (-) Alg which is the diagram associated to the morphism j k U k (-) Alg ⇑k . Thus, (-) Alg ≤k F n i k is an isomorphism if and only if j k U k (-) Alg ⇑k is an isomorphism. We conclude with Lemma 2.7.2.

We will use the above criterion to show that the monad associated to the theories of strict categories is weakly truncable (c.f. Theorem 4.4.2).

Free higher categories on generators

Given some theory of higher categories, an important construction is the one that builds a k-category which is freely generated on a set of generators. Indeed, like for other algebraic theories, a k-category can be described by means of a presentation, i.e., by quotienting a free k-category by a set of relations. For example, a formal adjunction can be described as the strict 2-category generated by two 0-cells x and y, two 1-cells l : y → x and r : x → y, and two 2-cells γ : id y ⇒ l * 0 r and : r * 0 l ⇒ id x satisfying the zigzag identities. Given a theory of higher categories expressed in Batanin's setting, i.e., as a monad (T, η, µ) on Glob n for some n ∈ N ∪ {ω}, there are several free constructions that one can consider. First, the functors F k : Glob k → Alg k already enable to construct the free k-category on a k-globular set. Moreover, there is a construction which produces a (k+1)-category from a k-cellular extension, i.e., a pair consisting of a k-category and a set of (k+1)-generators. Such construction was introduced for strict categories in [START_REF] Burroni | Higher-dimensional word problems with applications to equational logic[END_REF]. Finally, one can consider the free k-category on a k-polygraph: the latter is a system of i-generators for i ∈ N n which is organized inductively as cellular extensions. It differs from a mere k-globular set in the sense that a k-polygraph allows generators to have complex sources and targets that are composites of other generators, whereas the sources and targets of generators organized in a k-globular set can only be globes. Polygraphs were first introduced by Street [START_REF] Street | Limits indexed by category-valued 2-functors[END_REF] and Burroni [START_REF] Burroni | Higher-dimensional word problems with applications to equational logic[END_REF] for strict categories, and then generalized to any finitary monad on globular sets by Batanin [START_REF] Michael | Computads for finitary monads on globular sets[END_REF].

In this section, we define free constructions for algebraic globular higher categires following the path of Burroni, giving in the process another light on the results of Batanin, who was not relying on cellular extensions in his proofs. More precisely, we define the notion of cellular extension for any algebraic theory of globular higher categories, and then derive the notion polygraphs from it, together with the free construction associated to each notion. Since most of the definitions rely on pullbacks in CAT, we first recall some properties of these pullbacks (Section 3.1). Then, we introduce cellular extensions together with the associated free construction for any finitary monad on globular sets, and, in the case of a truncable monad, we show that this construction is stable, i.e., that freely adding (k+1)-generators does not change the underlying k-category (Section 3.2). Then, we introduce polygraphs together with the associated free construction for any finitary monad on globular sets (Section 3.3). Finally, we recover in our setting the adjunction of Batanin between higher categories and polygraphs in Section 3.4.

Pullbacks in CAT

In the following sections, we define the categories of cellular extensions and polygraphs using pullbacks in CAT. We will be interested in showing that these categories are cocomplete and that several of the projection functors are left or right adjoints. Such properties are consequence of general properties of pullbacks that we recall below. In particular, a pullback of an isofibration, i.e., a functor which lifts isomorphisms, has good properties with regard to cocompleteness and preservation of colimits. This is convenient since, as we will see below, all the truncation functors introduced until now are isofibrations.

In the following, given C ∈ CAT, we write id 2 C for the identity natural transformation on the identity functor id C : C → C. We begin with a property of compatibility of pullbacks in CAT with left and right adjoints: Proof. We define H using the universal property of pullbacks by

D C C D D H•F H id D F G G F
which satisfies G H = id D by definition. Moreover, suppose that there is an adjunction H G whose unit is id 2 D . Then, since C is defined by a pullback, a morphism f :

H X → Y ∈ C
is the data of morphisms f l : X → G Y and f r : HF X → F Y with F (f l ) = G(f r ). But, since the unit of H G is id 2 D , G induces a bijective correspondence between C(HF X, F Y ) and D(F X, GF Y ), so that f r is uniquely defined by F (f l ). Thus, G induces a bijective natural correspondence between C (H X, Y ) and D (X, G Y ) for all X ∈ D and Y ∈ C , so that there is an adjunction H G with unit id 2 D . The case where G is left adjoint is similar.

Moreover, we prove that isofibrations are well-behaved regarding pullbacks in CAT. We recall that a functor G : C → D ∈ CAT is an isofibration when it lifts isomorphisms, i.e., for all X ∈ C and Ỹ ∈ D, given an isomorphism f : GX → Ỹ in D, there exists Y ∈ C and an isomorphism f : X → Y such that GY = Ỹ and G(f ) = f . We then have:

Proposition 3.1.2. Given a pullback in CAT C C D D F G G F
such that G is an isofibration, the following hold:

(i) G is an isofibration, (ii) given a small category I, if C and D have all I-colimits and F and G preserve them, then C has all I-colimits and F and G preserve them.

Proof. Proof of (i):

Let X ∈ C , Y L ∈ D and θ L : G X → Y L be an isomorphism. Then, since G is an isofibration, there is Y R ∈ C and an isomorphism θ R : F X → Y R such that F (θ L ) = G(θ R ). Moreover, F (θ -1 L ) = G(θ -1 R ) so that (θ L , θ R ) : X → (Y L , Y R )
(F (p L,i ) : F (d L (i)) → F (X L )) i∈I and (G(p R,i ) : F (d L (i)) → G(X R )) i∈I
are colimit cocones for F • d L . So there exists an isomorphism θ : F (X L ) → G(X R ) between the two cocones. Since G is an isofibration, we can suppose that F (X L ) = G(X R ) and θ = id F (X L ) . Thus, we have a cocone ((p L,i , p R,i ) : d(i) → (X L , X R )) i on d, and we easily verify that it is a colimit cocone.

Remark 3.1.3. Pullbacks in CAT should normally raise suspicion since strict limits are not wellbehaved in CAT in general. Indeed, a limit cone in CAT on a diagram is not stable when replacing some functors of the diagram by isomorphic functors. Moreover, the limit cone is defined up to isomorphism, and not up to equivalence of categories. To solve this problem, one usually considers a weaker notion of limits, where the triangles of cones commute only up to isomorphisms, as with weighted bilimits [START_REF] Makkai | Accessible Categories: The Foundations of Categorical Model Theory[END_REF]. But the strict limit on a diagram is generally not equivalent to the associated weighted bilimit. However, introducing weighted bilimits here would be an unnecessary pain for what we want to do, since the pullbacks along isofibrations are equivalent to the weighted bipullbacks (see [START_REF] Makkai | Accessible Categories: The Foundations of Categorical Model Theory[END_REF]Proposition 5.1.1]).

We say that a monad functor is an isofibration when the underlying functor is an isofibration. We then have: Lemma 3.1.4. The functor EM preserves isofibrations.

Proof. Let (F, α) : (C, S) → (D, T ) be a monad functor isofibration. Let (X, h : SX → X) be an S-algebra, and f : F α (X, h) → (Y, k) be a T -algebra isomorphism. Since F is an isofibration, there is an isomorphism f : X → Ỹ such that F ( f ) = f . One can equip Ỹ with a structure of S-algebra ( Ỹ , k) by putting k = f • h • S( f -1 ). Then, we have an S-algebra morphism f : (X, h) → ( Ỹ , k). Moreover, ( Ỹ , k) is mapped to (Y, k) by F α , so that f is an isomorphism which lifts f . Hence, EM preserves isofibration.

We now verify that several functors of interest to us are isofibrations: Proposition 3.1.5. Given k, l ∈ N ∪ {ω} with k < l, the functor (-) Glob ≤k,l is an isofibration.

Proof. Straight-forward.

Proposition 3.1.6. Let n ∈ N ∪ {ω} and (T, η, µ) be a finitary monad on Glob n . Given k, l ∈ N ∪ {ω} with k < l, the functor (-) Alg ≤k,l is an isofibration.

Proof. The functor (-) Alg ≤k,l is the image by EM of ((-) Glob ≤k,l , (-) Glob ≤k,l T l i k,l ), which is an isofibration. Thus, by Lemma 3.1.4, it is an isofibration.

Cellular extensions

In this section, we introduce the notion of k-cellular extension, which describes a k-category (for some theory of higher categories) equipped with a set of (k+1)-generators. We moreover give the construction of the free (k+1)-category on a k-cellular extension together with more specific results when the theory we are considering is associated with a truncable monad.

Let n ∈ N ∪ {ω} and (T, η, µ) be a finitary monad on Glob n . Given k ∈ N n-1 , we define the category Alg + k of k-cellular extensions as the pullback

Alg + k Glob k+1 Alg k Glob k G k+1 A k (-) Glob ≤k U k
We verify that: Proposition 3.2.1. The category Alg + k is locally finitely presentable. In particular, it is complete and cocomplete. Moreover, both G k+1 and A k are finitary right adjoints.

Proof. The categoy Alg +

k is defined as the pullback of the finitary right adjoint isofibration (-) Glob ≤k along the right adjoint U k . Thus, it is a bipullback of right adjoints between locally finitely presentable categories. Since the 2-category of locally finitely presentable and finitary right adjoint functors is closed under bilimits (see [7, Theorem 2.17]), Alg + k is locally finitely presentable and the two projections G k+1 and A k are finitary right adjoint functors. Remark 3.2.2. In fact, one can check by hand that the finitely presentable objects of Alg + k are exactly the compatible pairs (C, X), where C is a finitely presentable object of Alg k and X is a compatible (k+1)-globular set such that X k+1 is finite. Proof. By adjunction, it is equivalent to prove that its right adjoint is finitary. By the constructive content of Proposition 3.1.1, this right adjoint is built from a cone of finitary functors on the (bi)pullback defining Alg + k , itself made of finitary functors. Thus, the factorizing functor is itself finitary.

There is a functor V k : Alg k+1 → Alg + k defined as the factorization arrow

Alg k+1 Alg + k Glob k+1 Alg k Glob k U k+1 (-) Alg ≤k V k A k G k+1 (-) Glob ≤k U k .
Then, there is an operation which produces a (k+1)-category from a k-cellular extension. It is the left adjoint to V k , that exists by the following property:

Theorem 3.2.5. V k has a left adjoint.

Proof. Let α k be the unit of the adjunction (-) Alg ↑k+1,k (-) Alg ≤k,k+1 , and let

Φ L : Alg k+1 ((-) Alg ↑k+1 , -) ⇒ Alg k (-, (-) Alg ≤k ) Ψ L : Alg k ((-) Alg ↑k+1 F k (-), -) ⇒ Glob k (-, U k (-) Alg ≤k,k+1 ) Φ R : Alg k+1 (F k+1 (-), -) ⇒ Glob k+1 (-, U k+1 (-)) Ψ R : Glob k+1 (F k+1 (-) Glob ↑k+1,k , -) ⇒ Glob k (-, (-) Glob ≤k U k+1 (-)
) be the natural bijections derived from the associated adjunctions. Note that these bijections can be defined using the units of the adjunctions. For example, given C ∈ Alg k and D ∈ Alg k+1 , Φ L maps a morphism f : C ↑k+1 → D ∈ Alg k+1 to the morphism

f ≤k • α k C : C → D ≤k ∈ Alg k
where α is the unit of (-) Alg ≤k (-) Alg ↑k+1 . Since

F k+1 (-) Glob ↑k+1 and (-) Alg ↑k+1 F k are both left adjoint to U k (-) Alg ≤k,k+1 = (-) Glob ≤k U k+1 , the natural morphism θ : F k+1 (-) Glob ↑k+1,k ⇒ (-) Alg ↑k+1 F k defined as the composite θ = ( k+1 (-) Alg ↑k+1,k F k ) • (F k+1 i k U k+1 (-) Alg ↑k+1,k F k ) • (F k+1 (-) Glob ↑k+1,k U k α k F k ) • (F k+1 (-) Glob ↑k+1,k η k ) which can be represented by Fk+1 (-) Glob ↑k+1,k θ (-) Alg ↑k+1,k Fk = Fk+1 (-) Glob ↑k+1,k Uk (-) Alg ≤k,k+1 = (-) Glob ≤k,k+1 Uk+1 (-) Alg ↑k+1,k
Fk is an isomorphism as a consequence of Proposition 2.7.3. In the following, given a morphism f : X → Y of a category C, we write f * : C(Y, Z) → C(X, Z) for the function g → g • f for all Z ∈ C. One can verify using the zigzag equations that the natural transformation θ makes the diagram

Alg k+1 ((F k Z) ↑k+1 , A) Glob k (Z, U k (A ≤k )) Alg k+1 (F k+1 (Z ↑k+1 ), A) Glob k (Z, (U k+1 A) ≤k ) (θ Z ) * Ψ L Z,A Ψ R Z,A (6)
commutes for all

Z ∈ Glob k and A ∈ Alg k+1 . Let (C, X) ∈ Alg + k , D ∈ Alg k+1 and (D ≤k , Y ) be V k D. Since U k C = X ≤k and U k D = Y ≤k
and by the properties of adjunctions, we have a diagram

Alg k+1 (C ↑k+1 , D) Alg k (C, D ≤k ) Alg k+1 ((F k U k C) ↑k+1 , D) Glob k (U k C, U k (D ≤k )) Alg k+1 (F k+1 ((X ≤k ) ↑k+1 ), D) Glob k (X ≤k , Y ≤k ) Alg k+1 (F k+1 X, D) Glob k+1 (X, Y ) (e L (C,X) ) * U k (θ X ≤k ) * (e R (C,X) ) * (-) Glob ≤k Φ L C,D Ψ L U k C,D Ψ R X ≤k ,D Φ R X,D (7)
such that each square commutes and where e L and e R are the natural transformations

e L = (-) Alg ↑k+1 k A k and e R = F k+1 i k G k+1
respectively. Indeed, the middle square commutes by ( 6) and the top and bottom squares commute by the zigzag equations. By definition of Alg + k , the set

Alg + k ((C, X), V k D) is the pullback Alg + k ((C, X), V k D) Glob k+1 (X, G k+1 V k D) Alg k (C, A k V k D) Glob k (X ≤k , (G k+1 V k D) ≤k ) G k+1 A k (-) Glob ≤k U k . Since (-) Alg ≤k = A k V k and U k+1 = G k+1
V k and by the commutative diagram [START_REF] Bird | Limits in 2-categories of locally-presented categories[END_REF], the following diagram is also a pullback:

Alg + k ((C, X), V k D) Alg k+1 (F k+1 X, D) Alg k+1 (C ↑k+1 , D) Alg k+1 (F k+1 ((X ≤k ) ↑k+1 ), D) (Φ R X,D ) -1 •G k+1 (Φ L C,D ) -1 •A k (e R (C,X) ) * (e L (C,X) •θ X ≤k ) * . Since Alg k+1 is cocomplete by Proposition 2.2.2, the diagram Alg k+1 (C[X], D) Alg k+1 (F k+1 X, D) Alg k+1 (C ↑k+1 , D) Alg k+1 (F k+1 ((X ≤k ) ↑k+1 ), D) (p R (C,X) ) * (p L (C,X) ) * (e R (C,X) ) * (e L (C,X) •θ X ≤k ) *
is also a pullback, where C[X], p L (C,X) and p R (C,X) are defined as the pushout

C[X] F k+1 X C ↑k+1 F k+1 ((X ≤k ) ↑k+1 ) p R (C,X) p L (C,X) e R (C,X) e L (C,X) •θ X ≤k .
Thus, there is an isomorphism

Alg k+1 (C[X], D) ∼ = Alg + k ((C, X), V k D)
which is natural in D. Hence, V k admits a left adjoint.

The operation (C, X) → C[X] defined in the proof of Theorem 3.2.5 extends to a functor

-[-] k : Alg + k → Alg k+1
that we often write -[-] when there is no ambiguity on k, and which is left adjoint to V k . The image C[X] of some (C, X) ∈ Alg + k is called the free extension on (C, X).

Example 3.2.6. Consider the monad (T, η, µ) on Glob 1 defined in Example 2.2.3. A 0-cellular extension (C, X) is then essentially the data of a set C 0 of 0-cells, a set X 1 of 1-generators, and functions d - 0 , d + 0 : X 1 → C 0 , i.e., a graph. Moreover, the 1-category C[X] is the image of (C, X) seen as a graph by the left adjoint to the functor Cat → Gph defined in Example A.2.8. Remark 3.2.7. Theorem 3.2.5 is a particular case of the fact that the category of locally presentable categories and right adjoints are closed under weighted bilimits (see [START_REF] Bird | Limits in 2-categories of locally-presented categories[END_REF] and the end of [19, §5.1]). But the concrete pushout description given by the proof will be useful later to show properties of the functor -[-]. Proposition 3.2.8. For every k ∈ N, the functor -[-] k preserves finitely presentable objects.

Proof. By adjunction, it is equivalent to show that its right adjoint V k is finitary. But, since T is finitary, U k is finitary, and (-) Alg ≤k is finitary by Proposition 2.3.3, so that the same argument as in the proof of Proposition 3.2.4 applies to conclude that V k is finitary.

The truncable case Let n ∈ N ∪ {ω} and (T, η, µ) be a finitary monad on Glob n . In this paragraph, we consider the case where T is a truncable monad, and show that the underlying k-category of a k-cellular extension is preserved by -[-] k . In the following, we write η A,k for the unit of the adjunction (-) Alg ↑k+1,k (-) Alg ≤k,k+1 . We have:

Proposition 3.2.9. If T is truncable, then η A,k is an isomorphism for k ∈ N n-1 .
Proof. The adjunction (-) Alg ≤k (-) Alg ⇑k+1 was built from the adjunction (-) Glob ≤k (-) Glob ⇑k+1 by lifting. The counit of the latter being an isomorphism, the counit of the former is as well, so that (-) Alg ⇑k+1 is fully faithful. Since we have (-) Alg ↑k+1 (-) Alg ≤k (-) Alg ⇑k+1 , by the unity and identity of opposites, (-) Alg ↑k+1 is fully faithful as well, so that η A,k is an isomorphism.

We can conclude a conservation result for the underlying k-category of (k+1)-categories produced by -[-] k :

Proposition 3.2.10. If T is truncable, then, given k ∈ N n and (C, X) ∈ Alg + k , there is an isomorphism C ∼ = C[X] ≤k which is natural in (C, X).
Proof. Recall that C[X] was defined in the proof of Theorem 3.2.5 as the pushout

C[X] F k+1 X C ↑k+1 F k+1 ((X ≤k ) ↑k+1 ) p R (C,X) p L (C,X) e R (C,X) e L (C,X) •θ X ≤k .
By Proposition 2.6.7, the following diagram is also a pushout

C[X] ≤k (F k+1 X) ≤k (C ↑k+1 ) ≤k (F k+1 ((X ≤k ) ↑k+1 )) ≤k (p R (C,X) ) ≤k (p L (C,X) ) ≤k (e R (C,X) ) ≤k (e L (C,X) •θ X ≤k ) ≤k . Since T is truncable, we have (-) Alg ≤k F k+1 = F k (-) Glob ≤k . Thus, (e R ) ≤k = (-) Alg ≤k F k+1 i k G k+1 = F k (-) Glob ≤k i k G k+1 = id F k (-) Glob ≤k G k+1 (since (i k ) ≤k = id Glob k ) so that (e R (C,X) ) ≤k = id F k (X ≤k )
. Hence, (p L (C,X) ) ≤k is an isomorphism, since the pushout of an isomorphism is an isomorphism. By Proposition 3.2.9, we conclude that the composite

C (C ↑k+1 ) ≤k C[X] ≤k η A,k C (p L (C,X) ) ≤k
is an isomorphism.

Remark 3.2.11. If T is truncable, given k ∈ N n , by Proposition 3.1.6, we can suppose that we chose -[-] k so that the isomorphism of Proposition 3.2.10 is the identity. When such a choice is made, we have C[X] ≤k = C for all k-cellular extension (C, X).

Polygraphs

In this section, we recover the generalized notion of polygraph of Batanin using cellular extensions. Intuitively, a polygraph is a system of generators which organizes inductively as cellular extensions, so that a definition of polygraphs based on the latter structures seems relevant. In the process, we study some properties of the different functors involved, and consider the truncable case.

Another definition of cellular extensions Let n ∈ N∪{ω} and (T, η, µ) be a finitary monad on Glob n . Before defining polygraphs, we first provide an alternative definition of Alg k which is simpler than the one based on pullbacks given in Section 3.2.

Proposition 3.3.1. Given k ∈ N n-1 , the category Alg + k is isomorphic to the category -whose objects are the pairs (C, S) where C ∈ Alg k and S is a set, equipped with two functions

d - k , d + k : S → C k such that ∂ k-1 • d - k = ∂ k-1 • d + k for ∈ {-, +},
-and whose morphisms between two such pairs (C, S) and (C , S ) are the pairs (F, f ) where

F : C → C ∈ Alg k and f : S → S ∈ Set and such that d k •f = F k • d k for ∈ {-, +}.
Proof. Write Alg + k for the category described in the statement. An isomorphism between Alg + k and Alg + k can be described as follows. Given (C, X) ∈ Alg + k , we map (C, X) to the pair (C, X k+1 ) and, for ∈ {-, +} and x ∈ X k+1 , we put d k (x) = ∂ k (x) (where ∂ k is the operation of the globular structure on X), and we extend this mapping to morphisms of Alg + k as expected. Since U k C = X ≤k for (C, X) ∈ Alg + k , the resulting functor is an isomorphism of categories.

In the following, we will prefer this new definition of cellular extensions to the original one. This other description helps better understand how a colimit of a diagram (C i , S i ) in Alg + k is computed: first, one computes a colimit C of the C i 's in Alg k , then one compute a colimit S of the S i 's and equips it with the evident source and target operations

d - k , d + k : S → C k .
Categories of polygraphs Let n ∈ N ∪ {ω} and (T, η, µ) be a finitary monad on the category Glob n . For k ∈ N n , we define the category Pol k of k-polygraphs by induction on k, together with a functor (-) * ,k : Pol k → Alg k simply denoted (-) * when there is no ambiguity on k, which maps a k-polygraph P to the free k-category P * on P. First, we put Pol 0 = Glob 0 and (-) * ,0 = F 0 . Now suppose that Pol k and (-) * ,k are defined for some k ∈ N n-1 . We define Pol k+1 as the pullback

Pol k+1 Alg + k Pol k Alg k (-) Pol ≤k,k+1 E k+1 A k (-) * ,k
and (-) * ,k+1 as the composite

Pol k+1 Alg + k Alg k+1 E k+1 -[-] k .
As usual, we write P ≤k for the image of P ∈ Pol k+1 by (-) Pol ≤k,k+1 , and we often simply write (-) Pol ≤k for the latter functor. Using the simpler definition of Alg + k from Proposition 3.3.1, we can give a more concrete description of Pol k for k ∈ N n . A 0-polygraph P is the data of a set P 0 of 0-generators, and a morphism P → P in Pol 0 is the data of a function F 0 : P 0 → P 0 . Given k ∈ N n-1 , a (k+1)-polygraph is the data of a pair P = (P ≤k , P k+1 )

where P ≤k is a k-polygraph and P k+1 is a set of (k+1)-generators, together with functions

d - k , d + k : P k+1 → ((P ≤k ) * ) k such that ∂ k-1 • d - k = ∂ k-1 • d + k for ∈ {-, +}, where ∂ - k-1 , ∂ + k-1 : ((P ≤k ) * ) k → ((P ≤k ) * ) k-1
are the source and target operations of the k-category (P ≤k ) * . Moreover, a morphism P → P in Pol k+1 is the data of a pair (F ≤k , F n+1 ) where F ≤k : P ≤k → P ≤k is a morphism of Pol k and F n+1 :

P n+1 → P n+1 is a function such that d k •F n+1 = (F ≤k ) * • d k for ∈ {-, +}, i.e., a (k+1)
-generator g is mapped by F n+1 to a generator g whose k-source and k-target are exactly the images of the k-source and k-target of g by (F ≤k ) * .

Remark 3.3.2. Note that the diagram

Pol k+1 Glob k+1 Pol k Glob k G k+1 E k+1 (-) Pol ≤k (-) Glob ≤k U k (-) * ,k (8)
is a pullback, since Alg + k is defined as a pullback and the concatenation of two pullbacks is still a pullback.

In order to better handle side conditions, we use the convention that

Alg + -1 = Glob 0 , E 0 = id Glob 0 , and -[-] 0 = F 0 so that (-) * ,0 = -[-] 0 • E 0 .
We then have:

Proposition 3.3.3.
For k ∈ N n , the category Pol k is locally ω 1 -presentable (in particular, complete and cocomplete), and the functor E k (resp. (-) Pol ≤k-1 when k > 0) is a left adjoint which preserves ω 1 -presentable objects.

Proof. We prove this property by induction on k. The category Pol 0 is locally finitely presentable since equivalent to Set. Moreover, since U 0 is finitary, it is also ω 1 -accessible so that F 0 preserves finitely presentable objects. Thus, the property holds for k = 0. Now assume that it holds in dimension k. By Proposition 3.2.8, the functor -[-] k is a left adjoint which preserves finitely presentable objects. Thus, its right adjoint is finitary and in particular ω 1 -accessible. Thus, -[-] k also preserves ω 1 -presentable objects. By induction hypothesis, (-) * ,k is a left adjoint which preserves ω 1 -presentable objects. By Proposition 3.2.4 and the same argument, A k is also a left adjoint which preserves ω 1 -presentable objects. By [7, Proposition 3.14], the (bi)pullback Pol k+1 of these two functors is a locally ω 1 -presentable category, and the two projecting functors (-) Pol ≤k and E k+1 are left adjoints which preserve ω 1 -presentable objects. Remark 3.3.4. Sadly, [7, Proposition 3.14] requires us to deal with uncountable cardinals, so that we can not use it to prove that Pol k is locally finitely presentable. But one can use an ad hoc argument as in [START_REF] Forest | Computational descriptions of higher categories[END_REF]Paragraph 1.3.3.16] to prove that it actually is. Moreover, the finitely presentable objects of Pol k are the expected ones, that is, the k-polygraphs with a finite number of generators. Proposition 3.3.5. For k ∈ N n , the functor (-) Pol ≤k,k+1 is an isofibration which has both a left adjoint and a right adjoint.

Proof. We know already that it has a right adjoint by Proposition 3.3.3. But it is also the consequence, as is the remainder of the statement, of Propositions 3.1.1 and 3.1.2.

Given i, k ∈ N such that i ≤ k < n + 1, we write (-) k i : Pol k → Set
or simply (-) i when there is no ambiguity on k, for the functor which maps a k-polygraph P to its set of i-generators P i . We verify that colimits of polygraphs are computed dimensionwise: Proposition 3.3.6. Given i, k ∈ N n such that i ≤ k, the functor (-) k i preserves colimits.

Proof. This functor can be described as the composite

(-) g • E i • (-) Pol ≤i • • • • • (-) Pol ≤k-1
where (-) g : Alg + i-1 → Set is the functor mapping a cellular extension (X, S) to its set of i-generator S. By our comment on the computation of colimit using the concrete description of Alg + i-1 , the functor (-) g preserves colimits. Moreover, all the other functors of the above composition preserve colimits by Proposition 3.3.3, so that the conclusion holds.

In the case where T is truncable, given k, l ∈ N with k < l, the underlying k-category of the free l-category on an l-polygraph is only determined by the underlying k-polygraph, as stated by the following proposition: Proposition 3.3.7. If T is truncable, then, given k ∈ N such that k < n and a (k+1)-polygraph, there exists an isomorphism (P * ) ≤k ∼ = (P ≤k ) * .

Proof. By definition of (-) * ,k , we have

P * = (P ≤k ) * [P k+1 ]
so that the wanted isomorphism comes from Proposition 3.2.10. Remark 3.3.8. When T is truncable, under the assumption of Remark 3.2.11, the isomorphism given by Proposition 3.3.7 is the identity. This enables to simplify some notations: given k, l ∈ N n with k ≤ l and an l-polygraph P, we write directly P * ≤k for both (P * ) ≤k and (P ≤k ) * , and P * k for both (P * ) k and ((P ≤k ) * ) k . Remark 3.3.9. When T is truncable, given k ∈ N n , a k-polygraph P can be alternatively described as a diagram in Set of the form

P 0 P 1 P 2 . . . P k-1 P k P * 0 P * 1 . . . P * k-2 P * k-1 e 0 d - 0 d - 0 e 1 d - 1 d - 1 e 2 d - k-2 d - k-2 e k d - k-1 d - k-1 ∂ - 0 ∂ + 0 ∂ - 1 ∂ + 1 ∂ - k-2 ∂ + k-2
where, for i ∈ N k-1 , e i is the embedding of the i-generators in the i-cells induced by the unit of the adjunction -[-] i V i-1 at ((P ≤i-1 ) * , P i ), such that

∂ - i • d - i+1 = ∂ - i • d + i+1 and ∂ + i • d - i+1 = ∂ + i • d + i+1 for i ∈ N k-1 .
The above description of polygraphs can already be found in the original paper of Burroni [START_REF] Burroni | Higher-dimensional word problems with applications to equational logic[END_REF] for polygraphs of strict categories.

ω-polygraphs Let (T, η, µ) be a finitary monad on Glob ω . We define the category of ω-polygraphs Pol ω as the limit in CAT

((-) Pol ≤k,ω : Pol ω → Pol k ) k∈N on the diagram Pol 0 Pol 1 • • • Pol k Pol k+1 • • • (-) Pol ≤0 (-) Pol ≤1 (-) Pol ≤k-1 (-) Pol ≤k (-) Pol ≤k+1
Concretely, an ω-polygraph P is the data of a sequence (P k ) k∈N , where P k is a k-polygraph, such that (P k+1 ) ≤k = P k for k ∈ N. We start with a presentability result for Pol ω :

Proposition 3.3.10. The category Pol ω is locally ω 1 -presentable (in particular complete and cocomplete), and the functors (-) Pol ≤k,ω are both left and right adjoints and preserve ω 1 -presentable objects.

Proof. By Proposition 3.3.3, the functors (-) Pol ≤k,k+1 are isofibrations, so that the limit defining Pol ω is in fact a bilimit. Since (-) Pol ≤k,k+1 preserves colimits as left adjoints, they are ω 1 -accessible right adjoints. By [7, Theorem 2.17], Pol ω is locally ω 1 -presentable and the functors (-) Pol ≤k,ω are ω 1 -accessible right adjoint functors.

The functors (-) Pol ≤k,k+1 are also left adjoints which preserve ω 1 -presentable objects by Proposition 3.3.3. Thus, [7, Proposition 3.14] also applies, so that we moreover get that (-) Pol ≤k,ω are left adjoints which preserve ω 1 -presentable objects.

Remark 3.3.11. Assuming the finite presentability of the Pol k given by Remark 3.3.4, we can apply [START_REF] Bird | Limits in 2-categories of locally-presented categories[END_REF]Theorem 2.17] to deduce that Pol ω is in fact locally finitely presentable. A small additional argument would then prove that the finitely presentable objects of Pol k are the ω-polygraph with a finite number of generators. A proof of these facts without using Bird can be found in [START_REF] Forest | Computational descriptions of higher categories[END_REF]Paragraph 1.3.3.16]. Now, in the truncable case, we can easily define the free ω-category on an ω-polygraph, just like for finite-dimensional polygraphs: Proposition 3.3.12. If T is truncable, there is a functor (-) * ,ω : Pol ω → Alg ω which is uniquely defined by (-) Alg ≤k,ω • (-) * ,ω = (-) Remark 3.3.13. In the case where T is only weakly truncable, the squares in the proof of Proposition 3.3.12 only commute up to isomorphism, so that we only get a pseudocone on the Alg k 's of vertex Pol ω . In this case, we can use the fact that Alg ω is a bilimit on the Alg k 's (since the functors (-) Alg ≤k,k+1 are isofibrations by Proposition 3.1.6) to get a functor (-) * ,ω : Pol ω → Alg ω which factorizes up to isomorphism that pseudocone. Remark 3.3.14. We can still define a functor (-) * ,ω : Pol ω → Alg ω in the case where T is not weakly truncable. However, this functor is not expected to be compatible with the functors (-) Alg ≤k as in Proposition 3.3.12. Indeed, in this case, the functor -[-] k does not preserve the underlying k-category C of a k-cellular extension (C, S) ∈ Alg + k .

Pol 0 Pol 1 • • • Pol k Pol k+1 • • • Alg 0 Alg 1 • • • Alg k Alg k+1 • • • (-) * ,0 (-) Pol ≤0 (-) * ,1 (-) Pol ≤1 (-) Pol ≤k-1 (-) * ,k (-) Pol ≤k (-) * ,k+1 (

The polygraphic adjunctions

We now translate in our setting the definition given by Batanin of the adjunction between globular algebras and polygraphs. In our case, this adjunction will be derived from one between cellular extensions and polygraphs that we are going to introduce. The constructions of this section are done using an induction on k ∈ N to build a functor

R + k : Alg + k → Pol k
which is part of an adjunction E k R + k , with unit ξk and counit νk , from which we derive a functor R k : Alg k → Pol k which is part of an adjunction (-) * ,k R k , with unit ξ k and counit ν k .

When k = 0, this is easy: we take R + k = 1 Glob 0 and R 0 = U 0 . So now, we assume that we have defined the right adjoints R + l and R l up to dimension k ∈ N, and we define the right adjoints R + k+1 and R k+1 starting with the former. By the pullback definition of Pol k+1 , this will require defining a functor Alg + k → Pol k and a functor Alg + k → Alg + k , the latter being reasonably suspected to be the functor of the comonad induced by the adjunction.

The functor Alg + k → Pol k is defined as expected as the composite

Alg + k A k --→ Alg k R k --→ Pol k .
We define the functor Alg + k → Alg + k , denoted S k , as follows: given (C, S) ∈ Alg + k , S k (C, S) is the pullback

S k (C, S) (C, S) ((R k C) * ) ⇑k+1 C ⇑k+1 q R (C,S) q L (C,S) j k (C,S) ((-) Alg+ ⇑k+1 ν k ) C
where j k denotes the unit of the adjunction A k (-) Alg+ ⇑k+1,k , with (-) Alg+ ⇑k+1,k being the right adjoint given by Proposition 3.2.3, and where ν k is the counit of the adjunction (-) * ,k R k defined by induction hypothesis. The idea behind this pullback is the following: we forget the k-category C as a k-polygraph and freely generate it back immediately to a k-category (the left leg), then we attach back the generators of S to this new k-category, taking into account that there now several choices of cells which evaluate to the old sources and targets of the elements of S (the right leg).

Since A k preserves limits (as a right adjoint), the diagram

(S k (C, S)) ≤k C (R k C) * C (q R ) ≤k (q L ) ≤k id C ν k C
is a pullback (we picked (-) Alg+ ⇑k+1,k so that the counit of A k (-) Alg+ ⇑k+1,k is the identity, which is possible by Proposition 3.1.1). Moreover, since A k is an isofibration, we can suppose that we defined S k so that (S k (C, S)) ≤k = (R k C) * and (q L ) ≤k = id.

Thus, we get as a factorization through Pol k+1 of the cone made of the above two functors a functor

R + k+1 : Alg + k → Pol k+1 which is characterized by (-) Pol ≤k R + k+1 = R k A k and E k+1 R + k+1 = S k . We now equip (E k+1 , R + k+1
) with a structure of an adjunction. First, we build a unit ξk+1 = ξk+1 l , ξk+1 r :

1 Pol k+1 ⇒ R + k+1 E k+1
through the pullback of Pol k+1 as follows. The projection of ξk+1 through (-

) Pol ≤k is ξk+1 l = ξ k (-) Pol ≤k ; this is well-defined, since (-) Pol ≤k R + k+1 E k+1 = R k A k E k+1 = R k (-) * ,k (-) Pol ≤k .
Moreover, the projection of ξk+1 through E k+1 is a natural transformation

ξk+1 r : E k+1 ⇒ E k+1 R + k+1 E k+1 = S k E k+1 : Pol k+1 → Alg + k
which is defined using the pullback definition of S k : we have the cone

E k+1 S k E k+1 E k+1 (-) Alg+ ⇑k+1 (-) * ,k R k A k E k+1 (-) Alg+ ⇑k+1 A k E k+1 id λ ξk+1 r q R q L j k E k+1 (-) Alg+ ⇑k+1 ν k A k E k+1
where λ is defined using string diagram as

λ = Ek+1 (-) Alg+ ⇑k+1 Ak = (-) * ,k Rk (-) * ,k (-) Pol ≤k = (-) Alg+ ⇑k+1 (-) * ,k Rk Ak Ek+1
. This is indeed a cone, as one can easily verify using the zigzag equations of adjunctions that the following two string diagrams so that the equation holds by the zigzag equations of adjunctions. Thus,

ξk+1 = ξk+1 l , ξk+1 r : 1 Pol k+1 ⇒ R + k+1 E k+1
is well-defined. are now required to give a counit

νk+1 : E k+1 R + k+1 ⇒ 1 Alg + k .
A candidate already exists: since E k+1 R + k+1 = S k , we can take νk+1 = q R . We now verify that we have an adjunction: Theorem 3.4.1. There is an adjunction E k+1 R + k+1 with ξk+1 and νk+1 as unit and counit.

Proof. We verify the first zigzag equation, namely

(ν k+1 E k+1 ) • (E k+1 ξk+1 ) = id E k+1 : (ν k+1 E k+1 ) • (E k+1 ξk+1 ) = (ν k+1 E k+1 ) • ( ξk+1 r ) = id E k+1
by the definition ξk+1 r . We now verify the second zigzag equation, namely (R

+ k+1 νk+1 ) • ( ξk+1 R + k+1 ) = id R + k+1
. We first check that the projection along (-) Pol ≤k is an identity using string diagrams:

(-) Pol ≤k R + k+1 R + k+1 Ek+1 R + k+1 = (-) Pol ≤k R + k+1 Rk (-) * ,k = Ak Ek+1 = (-) Pol ≤k R + k+1 = (-) Pol ≤k R + k+1 Rk (-) * ,k = Ak Ek+1 = (-) Pol ≤k R + k+1 = (-) Pol ≤k R + k+1 Rk (-) * ,k = Ak Ek+1 = (-) * ,k Rk Ak = (-) Pol ≤k R + k+1 = (-) Pol ≤k R + k+1 = Rk Ak Rk (-) * ,k = (-) Pol ≤k R + k+1 = Ak Ek+1 = (-) * ,k Rk Ak = (-) Pol ≤k R + k+1 = (-) Pol ≤k R + k+1 = Rk (-) * ,k Rk Ak = (-) Pol ≤k R + k+1 = (-) Pol ≤k R + k+1 (-) Pol ≤k R + k+1 .
We now check that the projection along E k+1 is also an identity, i.e.,

(S k q R ) • ( ξk+1 r R + k+1 ) = id S k . (9)
As an equation between two natural transformation with codomain S k , we check it by verifying that the projections along q L and q R are the same. We start with q L and use for this purpose the following property: Lemma 3.4.2. Given two natural transformation α, β : F ⇒ (-) Alg+ ⇑k+1 G for some functors

F : C → Alg + k and G : C → Alg k , we have α = β if and only if A k α = A k β.
Proof. The adjunction A k (-) Alg+ ⇑k+1 induces a correspondence between natural transformations of type F ⇒ (-) Alg+ ⇑k+1 G and the ones of type A k F ⇒ G. Since the counit of this adjunction is an identity, the forward map of this correspondence is given by the application of A k . Thus, by Lemma 3.4.2, q L is a cofork of the two sides of (9) if the equation

(A k S k q R ) • (A k ξk+1 r R + k+1 ) = id A k S k holds. We compute that (A k S k q R ) • (A k ξk+1 r R + k+1 ) = ((-) * ,k R k A k q R ) • ((-) * ,k ξ k (-) Pol ≤k R + k+1 ) = ((-) * ,k R k ν k A k ) • ((-) * ,k ξ k R k A k ) = id (-) * ,k R k A k = id A k S k
(by the zigzag equations).

We proceed with verifying that q R is a cofork of the two sides of the equation:

q R • (S k q R ) • ( ξk+1 r R + k+1 ) = q R • (q R S k ) • ( ξk+1 r R + k+1 ) (by the exchange law) = q R = q R • id S k (by definition of ξk+1 r ).
Thus, by the universal property of the pullback, the equation ( 9) holds. Hence, since its projections along q L and q R holds, the second zigzag equation holds, concluding the proof.

Writing R k+1 for the composite R + k+1 V k , we get:

Corollary 3.4.3.
There is an adjunction (-) * ,k+1 R k+1 : Alg k+1 → Pol k+1 .

Proof. By composing the two adjunctions given by Theorem 3.2.5 and Theorem 3.4.1.

The unit ξ k+1 and counit ν k+1 are defined in the process of composing the two adjunctions. This concludes the inductive argument of this section.

The full example of strict categories

In this section, we illustrate the previous constructions on the classical example of strict categories, is a well-known theory of higher categories. Strict categories, as their name suggests, are a classical example of a theory for higher categories that lies on the strict side of the strict/weak spectrum of higher categories. As such, they do not represent faithfully the homotopical information of topological spaces (see [START_REF] Simpson | Homotopy types of strict 3-groupoids[END_REF] or [START_REF] Berger | Double loop spaces, braided monoidal categories and algebraic 3-type of space[END_REF]). Nevertheless, they admit a relatively simpler axiomatization than weak higher categories, and can be encountered in several situations of interest. In the following, we recall the equational definition of strict categories and show that it is associated with a truncable monad on globular sets using the criterions proved in the previous sections (Theorem 2.5.2 and Theorem 2.7.4). This allows deriving notions of cellular extensions and polygraphs with the associated free constructions.

We start by recalling the equational definition of strict categories in Section 4.1. Then, we give the full calculation that the forgetful functor from strict categories to globular sets is monadic in Section 4.2. Next, we give the boilerplate definitions of the truncation and inclusion functors for strict categories in Section 4.3. Then, we show that the categories of strict categories that we obtain in each dimension are coherently equivalent to the categories of globular algebras derived from a monad on Glob ω (the monad of strict ω-categories) in Section 4.4. Finally, we instantiate the free constructions introduced in Section 3 in the case of strict categories in Section 4.5.

Equational definition

Given n ∈ N∪{ω}, a strict n-category (C, ∂ -, ∂ + , id, * ) (often simply denoted C) is an n-globular set (C, ∂ -, ∂ + ) together with, for k ∈ N with k < n, identity operations id k+1 : C k → C k+1 often writen id when there is no ambiguity on k, and, for i, k ∈ N n with i < k, composition operations

* i,k : C k × i C k → C k
often denoted * i when there is no ambiguity on k, which satisfy the axioms (S-i) to (S-vi) below. Given k, l ∈ N n such that k ≤ l and u ∈ C k , we extend the notations for identity operations and write id l (u) for id

l (u) = id l • • • • • id k+1 (u)
and, for the sake of conciseness, we often write id l u for id l (u), or even id u when l = k + 1. The axioms are the following:

(S-i) for k ∈ N n-1 and u ∈ C k , ∂ - k (id k+1 u ) = ∂ + k (id k+1 u ) = u, (S-ii) for i, k ∈ N n with i < k, (u, v) ∈ C k × i C k and ∈ {-, +}, ∂ k-1 (u * i v) =      ∂ k-1 (u) * i ∂ k-1 (v) if i < k -1, ∂ - k-1 (u) if i = k -1 and = -, ∂ + k-1 (v) if i = k -1 and = +, (S-iii) for i, k ∈ N n such that i < k, and u ∈ C k , k (∂ - i (u)) * i u = u = u * i id k (∂ + i (u)), (S-iv) for i, k ∈ N n such that i < k, and i-composable u, v, w ∈ C k , (u * i v) * i w = u * i (v * i w), (S-v) for i, k ∈ N n-1 such that i < k, and (u, v) ∈ C k × i C k , id k+1 (u * i v) = id k+1 u * i id k+1 v ,
(S-vi) for i, j, k ∈ N n such that i < j < k, and u, u , v, v ∈ C k such that u, v are i-composable, and u, u are j-composable, and v, v are j-composable,

(u * i v) * j (u * i v ) = (u * j u ) * i (v * j v ).
Note that the composition that appear in Axioms (S-iii), (S-iv), (S-v) and (S-vi) are well-defined as a consequence of Axioms (S-i) and (S-ii) and the equations satisfied by the source and target operations of a globular set. The Axiom (S-vi) is frequently called the exchange law of strict categories.

Example 4.1.1. Given a 2-category C and 0-, 1-and 2-globes as in the following configuration

x y z f 1 f 2 f 3 g 1 g 2 g 3 ⇓ u ⇓ u ⇓ v ⇓ v we have (u * 0 v) * 1 (u * 0 v ) = (u * 1 u ) * 0 (v * 1 v ) by Axiom (S-vi).
Our definition of strict categories involves sets, but we could have written a similar definition using classes to define large strict categories. For such alternative definition, we have the following classical example:

Example 4.1.2. There is a large strict 2-category Cat whose 0-cells are the small categories, whose 1-cells are the functors between the 1-categories, and whose 2-cells are the natural transformations between functors, and where the operations * 0,1 is the composition of functors, and the operations * 0,2 and * 1,2 are respectively the horizontal and vertical compositions of natural transformations. Note that the exchange law Axiom (S-vi) in this setting corresponds to the usual exchange law for natural transformations.

Given two strict n-categories C and D, a morphism F between C and D is the data of an n-globular morphism F : C → D which moreover satisfies that

-F (id k+1 u ) = id k+1 F (u) for every k ∈ N n-1 and u ∈ C k , -F (u * i v) = F (u) * i F (v) for every i, k ∈ N n with i < k and i-composable u, v ∈ C k .
We often call such morphisms n-functors. We write Cat n for the category of strict n-categories.

There is a functor Ūn : Cat n → Glob n which maps a strict n-category to its underlying n-globular set. The above definition of strict n-categories directly translates into an essentially algebraic theory (c.f. Appendix A.2), so that the functor Ūn is induced by a morphism between the essentially algebraic theory of n-globular sets (c.f. Remark 2.1.1) and the one of strict n-categories. Thus, we get:

Monadicity

We prove here that the functors Ūn are monadic. For this purpose, we use Beck's monadicity theorem, that we first recall quickly. Given a category C and morphisms f, g : X → Y and h : Y → Z in C, we say that h is a split coequalizer of f and g when there exist s : Z → Y and t : Y → X as in

X Y Z f g h t s
such that h • f = h • g, h • s = id Z , f • t = id Y , and s • h = t • g. From this data, it can be shown that h is a coequalizer of f and g. Beck's monadicity theorem is then: Theorem 4.2.1. Given a functor R : C → D, the functor R is monadic if and only if the following conditions are satisfied:

(i) R is a right adjoint, (ii) R reflects isomorphisms, (iii) for every pair of morphisms f, g : X → Y in C, if R(f ), R(g) have a split coequalizer, then f, g have a coequalizer which is preserved by R.

Proof. See [START_REF] Borceux | Handbook of Categorical Algebra[END_REF]Theorem 4.4.4] or the original work of Beck [START_REF] Beck | Triples, algebras and cohomology[END_REF].

We can then prove the following: = KS(u) * i KS(v), so that K is an n-functor. Hence, H is the coequalizer in Cat n of F and G. We can conclude with Theorem 4.2.1.

Truncation and inclusion functors

Let k, l ∈ N ∪ {ω} such that k < l. There is a truncation functor There is an adjunction (-) Cat ↑l,k (-) Cat ≤k,l whose unit is the identity and whose counit i k,l is such that, given a strict l-category C, the l-functor i k,l C : (C ≤k ) ↑l → C is defined by (i k,l C ) ≤k = id C ≤k and, for m ∈ N l with m > k, i k,l C maps u ∈ ((C ≤k ) ↑l ) m = C k to id m u .

Strict categories as globular algebras

By Proposition 4.1.3, each functor Ūn admits a left adjoint Fn for n ∈ N ∪ {ω}. In particular, the adjunction Fω Ūω defines a monad (T, η, µ), which is finitary by Proposition 4.1.3, and it induces categories of algebras Alg n for n ∈ N ∪ {ω} as explained in Section 2.2. By Proposition 4.2.2, the comparison functor H ω : Cat ω → Alg ω is an equivalence of categories, that moreover satisfies that U ω H ω = Ūω . Using the criterion introduced in Section 2.5, we prove that the other categories Cat n are, up to equivalence, the categories of algebras Alg n : Proof. The unit of the adjunction (-) Cat ↑ω,n (-) Cat ≤n is the identity, so that (-) Cat ↑ω,n is fully faithful and Theorem 2.5.2 applies.

Finally, we prove the truncability of the monad of strict ω-categories: (-) Glob ⇑ω,k , there is a unique ω-globular morphism F : D → C such that F ≤k = F , which is defined by

F (u) = (F (∂ - k (u)), F (∂ + k (u)))
for every l ∈ N with k < l and u ∈ D l . We verify that F is an ω-functor by checking the compatibility with the id l and * i,l operations. Given l ∈ N with l ≥ k and u ∈ D l , we have

F (id l+1 u ) = (F (∂ - k (u)), F (∂ + k (u))) = id k+1 F (u) .
Moreover, given i, l ∈ N with max(i, k) < l and i-composable u, v ∈ D l , we have

F (u * i v) = (F (∂ - k (u)) * i F (∂ - k (v)), F (∂ + k (u)) * i F (∂ + k (v))) if i < k (F (∂ - k (u)), F (∂ + k (v))) if i ≥ k = F (u) * i F (v).
Thus, F is an ω-functor. Hence, the natural bijective correspondence (ii) this factorization is essentially unique, i.e., if there exist others i ∈ I and g : P → d(i) such that f = p i • g , then there exist j ∈ I, h : i → j ∈ I and h : i → j ∈ I such that d(h) • g = d(h ) • g .

Example A.1.3. Given a set S, S is finitely presentable if and only if it is finite. See [1, Example 1.2(1)] for details.

Example A.1.4. A monoid is finitely presentable when it admits a presentation consisting of a finite number of generators and equations. A similar description of finitely presentable objects holds for the other categories of algebraic structures (groups, rings, etc.). See [1, Theorem 3.12] for details.

Locally finitely presentable categories A locally small category C ∈ CAT is locally finitely presentable when (i) it has all small colimits, (ii) every object of C is a directed colimit of locally finitely presentable objects, (iii) the full subcategory of C whose objects are the finitely presentable objects is essentially small.

Example A.1.5. The category Set is locally finitely presentable. Indeed, it is cocomplete and every set is a directed colimit of its finite subsets, which are finitely presentable objects of Set.

Example A.1.6. The category Mon of monoids is locally finitely presentable. More generally, the categories of algebraic structures (groups, rings, etc.) are locally finitely presentable. This is the consequence of the fact that such categories can be described by means of essentially algebraic theories, as we will see in the next section.

Identifying a category as locally finitely presentable enables to derive several elementary properties, like completeness:

Proposition A.1.7. A locally finitely presentable category is complete.

Proof. See [1, Corollary 1.28, Remark 1.56(1), Theorem 1.58] for details.

Moreover, showing that a functor between two locally finitely presentable categories is a left or right adjoint is easier than in the general case, since we do not need the existence of solution set like in Freyd's adjoint theorem ([8, Theorem 3.3.3]):

Proposition A.1.8. Given a functor F : C → D between two locally finitely presentable categories C and D, the following hold:

(i) F is left adjoint if and only if it preserves colimits, (ii) if F preserves limits and directed colimits, then it is right adjoint.

Finally, there is a simple criterion for a category of algebras on a monad to be locally finitely presentable. We recall that a functor F is finitary when F preserves directed colimits, and a monad (T, η, µ) on a category C is finitary when T is finitary. We then have:

Proposition A.1.9. Given a locally finitely presentable category C and a finitary monad (T, η, µ) on C, the category of algebras C T is locally finitely presentable. Moreover, the canonical forgetful functor C T → C preserves directed colimits.

  Monads, monad functors and monad transformations form a (very large) strict 2-category denoted MND. There is a functor Inc : CAT → MND which maps a large category C to the identity monad (C, 1 C ). This functor admits a right adjoint EM : MND → CAT which maps a monad (C, T ) to the Eilenberg-Moore category C T , and a monad functor (F, α) : (C, S) → (D, T ) to a functor F α : C S → D T mapping an algebra (X, h) ∈ C S to the algebra (F X, F h • α X ) ∈ D T , and mapping an algebra morphism f to F (f ). Finally, a monad transformation m : (F, α) ⇒ (G, β) : (C, S) → (D, T )

Proposition 1 . 3 . 1 .

 131 Let C and D be two categories, (S, η S , µ S ) be a monad on C, and L R : C → D be an adjunction. The functor R lifts through Und to a cocartesian map (R, RS ) : (C, S) → (D, T )

Proposition 1 . 3 . 3 .

 133 Given an adjunction L R : C → D and a monad functor (R, ρ) : (C, S) → (D, T ), the following are equivalent: (i) there exists λ : SL ⇒ LT such that (L, λ) (R, ρ) is an adjunction in MND, whose image by Und is the adjunction L R;

Proposition 1 . 3 . 4 .

 134 Given an adjunction L R : C → D and a monad functor (L, λ) : (D, T ) → (C, S), the following are equivalent: (i) there exists ρ : SR ⇒ RT such that (L, λ) (R, ρ) is an adjunction in MND, whose image by Und is the adjunction L R;

Lemma 2 . 5 . 1 .Ū

 251 Given a commutative diagram of functors which are part of adjunctions F U , F Ū , I T , I T , we have a diagram in MND (C, 1)

Theorem 2 . 5 . 2 .

 252 Let (T, η, µ) be a finitary monad on Glob ω , and (C k ) k∈N and C ω be categories, and (U k : C k → Glob k ) k∈N and U ω : C ω → Glob ω be monadic functors, and (T k+1 k : C k+1 → C k ) k∈N and (T ω k : C ω → C k ) k∈N be right adjoint functors with fully faithful left adjoints such that T k+1 k T ω k+1 = T ω k and

Proposition 2 . 7 . 3 .

 273 Let L R : C → D and L R : C → D be two adjunctions with respective unit-counit pairs (γ, ) and (γ , ), and θ : L ⇒ L and θ : R ⇒ R be two natural transformations such that θ = ( L ) • (L θL ) • (Lγ ), i.e., graphically:

  Alg ⇑n , F n U n and (-) Glob ↑n (-) Glob ≤k respectively. Using the zigzag equations satisfied by adjunctions to reduce the above diagram, we obtain (-) Glob ⇑n (-) Glob ≤k U n (-) Alg ⇑n j k

Proposition 3 . 1 . 1 .F

 311 Given a pullback in CAT and a functor H : D → C such that GH = id D , then there exists a canonical H : D → C such that G H = id D . Moreover, if there is an adjunction H G (resp. G H) whose unit (resp. counit) is id 2 D , then there is an adjunction H G (resp. H G) whose unit (resp. counit) is id 2 D .

  is an isomorphism of C . Proof of (ii): Let d : I → C be a functor, which is the data of d L : I → D and d R : I → C. Then, there are colimit cocones (p L,i : d L (i) → X L ) i∈I and (p R,i : d R (i) → X R ) i∈I . Since both F and G preserve colimits, both

Proposition 3 . 2 . 3 .

 323 The functor A k is an isofibration and has a right adjoint.Proof. This is a consequence of Propositions 3.1.1 and 3.1.5. Proposition 3.2.4. The functor A k preserves finitely presentable objects.

  the definition of Pol ω and Proposition 2.4.2, induces a functor (-) * ,ω which satisfies the wanted properties.

  * ,k Rk (-) * ,k (-) Pol ≤k natural transformation. Thus, we get a factorization natural transformation ξk+1 r : E k+1 ⇒ E k+1 R + k+1 E k+1 . We still need to verify that the equation (-) * ,k ξk+1 l

Proposition 4 . 2 . 2 .

 422 Given n ∈ N ∪ {ω}, the functor Ūn is monadic.Moreover, given i, k ∈ N n with i < k, and (u, v) ∈ C k × C k , we have KS(u * i v) = KSH(S(u) * i S(v)) = K(S(u) * i S(v))

(- )

 ) Cat ≤k,l : Cat l → Cat k which maps a strict l-category C to its evident underlying strict k-category, denoted C ≤k , and called the k-truncation of C. Conversely, there is an inclusion functor (-) Cat ↑l,k : Cat k → Cat l which maps a strict k-category C to the strict l-category C ↑l , called the l-inclusion of C, and defined by (C ↑l ) ≤k = C and (C ↑l ) m = C k for m ∈ N l with k < m, and such that -for m ∈ N l-1 with k ≤ m and u ∈ (C ↑l ) m+1 , ∂ - m (u) = ∂ + m (u) = u, -for m ∈ N l-1 with k ≤ m and u ∈ (C ↑l ) m , id m+1 u = u,-for i, m ∈ N l with i < k < m and (u, v) ∈ (C ↑l ) m × i (C ↑l ) m , u * i,m v = u * i,k v, -for i, m ∈ N l with k ≤ i < m and (u, v) ∈ (C ↑l ) m × i (C ↑l ) m , u * i,m v = u = v.

Theorem 4 . 4 . 1 .

 441 There exists a family of equivalences(H k : Cat k → Alg k ) k∈N that U k H k = Ūk for every k ∈ N.

Theorem 4 . 4 . 2 .

 442 The monad (T, η, µ) on Glob ω derived from Fω Ūω is weakly truncable.Proof. By Theorem 2.7.4 and Theorem 4.4.1, it is enough to show that, for every k ∈ N, the functors (-) Cat ≤k,ω have right adjoints such that j k U ω (-) Cat ⇑ω,k is an isomorphism, where recall that j k is the counit of (-) Glob ≤k,ω (-) Glob ⇑ω,k . So let k ∈ N.Given a strict k-category C, we define a strict ω-category C whose underlying globular set is the image the underlying k-globular set of C by (-) Glob ⇑ω,k , i.e.,C ≤k = C and C l = {(u, v) ∈ C 2 k | u, v are parallel} for l > k,and we equip C with a structure of a strict ω-category that extends the one on C by puttingid k+1 u = (u, u) for u ∈ C k , id l+1 (u,v) = (u, v) for l ∈ N with l > k and (u, v) ∈ C l ,and moreover, for i, l ∈ N with max(i, k) < l and i-composable(u, v), (u , v ) ∈ C l , (u, v) * i,l (u , v ) = (u * i,k u , v * i,k v ) if i < k, (u, v ) if i ≥ k.One can show that the axioms of strict ω-categories are verified by C . Now, let D be a strict ω-category and F : D ≤k → C be a k-functor. By the properties of the adjunction (-) Glob ≤k,ω

(- ) 4 )

 )4 Glob ≤k,ω : Glob ω (D, C ) → Glob k (D ≤k , C) obtained by concatenating horizontally (resp. vertically) representations of u and v. For example, using this representation, the 3-generators L, R and A, can be pictured by L : by Axiom (S-vi), a 2-cell can admit several representations as string diagrams. For example, the 2-cellµ * 0 id 2 3 * 0 µ = (µ * 0 id 2 5) * 1 (id 2 4 * 0 µ) = (id 2 5 * 0 µ) * 1 (µ * 0 id 2can be represented by the three string diagrams and and .

  1.9 since Glob k is locally finitely presentable by Remark 2.1.1. The functor U k preserves directed colimits by Proposition A.1.9. Moreover, since U k reflects isomorphisms and Alg k is cocomplete, U k creates directed colimits. Finally, it is well-known that the forgetful functor associated to an Eilenberg-Moore category creates limits (see [9, Proposition 4.3.1] for example).We can usually derive monads from equational definitions of higher categories as illustrated by the following examples.

Example 2.2.3. The canonical forgetful functor Cat → Glob 1 is a finitary right adjoint (see Example A.2.8 for a detailed argument) which thus induces a finitary monad (T, η, µ) on Glob 1 .

  Proposition 4.1.3. For every n ∈ N ∪ {ω}, the category Cat n is locally finitely presentable, complete and cocomplete. Moreover, the functor Ūn is a right adjoint which preserves directed colimits.Proof. The category Cat n is locally finitely presentable by Theorem A.2.1 and in particular cocomplete. It is moreover complete by Proposition A.1.7. The required properties on Ūn are a consequence of Theorem A.2.5.

https://github.com/smimram/satex.

This work was partially supported by the French ANR project PPS (ANR-19-CE48-0014).

Proof. By Proposition 4.1.3, Ūn is a right adjoint. Moreover, given a morphism

then there is a morphism

defined by (F -1 ) k = (F k ) -1 for k ∈ N n , so that Ūn reflects isomorphisms. Now, let F, G : X → Y be two morphisms of Cat n such that there exist Z ∈ Glob n , and morphisms

that witness that Ūn (F ), Ūn (G) is a split coequalizer. We prove that F, G has a coequalizer which is preserved by Ūn . For this purpose, we shall equip Z with a structure of a strict n-category.

For i, k ∈ N n with i < k and (u, v) ∈ Z k × i Z k , we put

and, given k ∈ N n-1 and u ∈ C k , we put

We verify that the axioms of strict n-categories are verified. Let k ∈ N n-1 , u ∈ Z k and ∈ {-, +}.

We have

S(u) )) = H(S(u)) = u so that Axiom (S-i) is satisfied. Now, let i, k ∈ N n such that i < k, (u, v) ∈ Z k × i Z k and ∈ {-, +}. We have

so that, by reducing the last expressions, we see that Axiom (S-ii) is satisfied. Now, let i, k ∈ N n such that i < k, and u ∈ Z k . We have

and, similarly, u * i id k (∂ + i (u)) = u, so that Axiom (S-iii) holds. Now, let i, k ∈ N n such that i < k, and i-composable u, v, w ∈ C k . We have

and, similarly, u * i (v * i w) = H(S(u) * i S(v) * i S(w)). So that Axiom (S-iv) is satisfied. Axioms (Sv) and (S-vi) are proved similarly, so Z is equipped with a structure of a strict n-category.

We now verify that H is a strict n-category morphism. Given k ∈ N n-1 and u ∈ Y k , we have

and, given i, k ∈ N n with i < k, and

so that H is a strict n-category morphism.

We now prove that H is the coequalizer of F and G in Cat n . Let K : Y → W be an n-functor such that KF = KG. Then, since H is the coequalizer of Ūn (F ) and Ūn (G), there is a unique morphism K : Ūn Z → Ūn W of Glob n such that K H = K. We are only left to prove that K is an n-functor. First, note that we have

restricts to a bijective correspondence

so that the operation C → C extends to a functor (-) Cat ⇑ω,k which is right adjoint to (-) Cat ≤k,ω . Moreover, by the definition of C above, the natural morphism j k U ω (-) Cat ⇑ω,k is an isomorphism. Hence, Theorem 2.7.4 applies and (T, η, µ) is a weakly truncable monad.

Remark 4.4.3. We highlight that the criterions given by Theorem 2.5.2 and Theorem 2.7.4 enabled us to prove that the categories Cat n are globular algebras derived from a truncable monad on Glob ω without giving an explicit description of this monad, which could have been a tedious exercise [START_REF] Penon | Approche polygraphique des ∞-catégories non strictes[END_REF].

Free constructions

Using Theorem 4.4.1 and Theorem 4.4.2, we can instantiate the definitions and properties developed in Section 3 to define free constructions on strict n-categories. In particular, for every n ∈ N, there is a notion of n-cellular extension, with associated category Cat + n defined like Alg + n . Moreover, there is a canonical forgetful functor Cat n+1 → Cat + n which has a left adjoint

As was shown in [START_REF] Métayer | Cofibrant objects among higher-dimensional categories[END_REF], the (n+1)-cells of a free extension admit a syntactical description consisting of "well-typed" terms considered up to the axioms of strict categories (c.f. Section 4.1).

Using the functors -[-] k , we can define, for every n ∈ N ∪ {ω}, a notion of n-polygraph with associated category Pol n , and a functor (-) * ,n : Pol n → Cat n which maps an n-polygraph P to the free strict n-category P * induced by the generators contained in P. Note that, when n > 0, as a consequence of the compatibility of -[-] n-1 with truncation, the underlying strict (n-1)-category (P * ) ≤n-1 of P * is exactly (P ≤n-1 ) * . As before, the cells of P * admit a syntactic description as equivalence classes of well-typed terms (see [START_REF] Makkai | The word problem for computads[END_REF] or [START_REF] Forest | Computational descriptions of higher categories[END_REF]Proposition 1.4.1.16]).

Example 4.5.1. Given the 1-polygraph P with P 0 = {x} and P 1 = {f : x → x}, the strict 1-category P * is the monoid of natural numbers (N, 0, +).

Example 4.5.2. We define a 3-polygraph P that aims at encoding the structure of a pseudomonoid in a 2-monoidal category as follows. We put

where, given n ∈ N, we write n for the composite 1 * 0 • • • * 0 1 of n copies of 1, and we define P 3 as the set with the following three elements

It is convenient to represent the 2-cells of P * using string diagrams. In this representation, the 2-generators η and µ are represented by and respectively, and the 2-cells of the form id 2 n are represented by sequences of n wires

A Local presentability

Locally presentable categories are a standard tool for deriving elementary properties on categories of algebraic structures (monoids, groups, but also categories, 2-categories, etc.). They are those categories where every object is a directed colimit of "finitely presentable" objects, which are a generalization of the notions of finitely presentable monoids or groups. Knowing that some categories are locally finitely presentable category is helpful since those categories are complete, cocomplete and satisfy other nice properties. For a more complete presentation, we refer to the existing literature [START_REF] Gabriel | Lokal präsentierbare Kategorien[END_REF][START_REF] Adámek | Locally Presentable and Accessible Categories[END_REF][START_REF] Borceux | Handbook of Categorical Algebra[END_REF].

We first recall the definition of locally finitely presentable categories (Appendix A.1) and then introduce essentially algebraic theories, which are a standard tool to show that some categories are locally finitely presentable (Appendix A.2).

A.1 Presentability

In this section, we define the notion of locally finitely presentable category, after recalling directed colimits and presentable objects of categories.

Directed colimits A partial order (D, ≤) is directed when D = ∅ and for all x, y ∈ D, there exists z ∈ D such that x ≤ z and y ≤ z. A small category I is called directed when it is isomorphic to a directed partial order (D, ≤).

Given a category C ∈ CAT, a diagram in C is the data of a functor d : I → C where I is a small category. We say that it is a directed diagram when

A set is a directed colimit of its finite subsets. A monoid is a directed colimit of its finitely generated submonoids.

In Set, we have the following characterization of directed colimits: is the free monoid functor on Set. It can be shown that T is finitary, so that we obtain another proof that Mon is locally finitely presentable using Proposition A.1.9.

Locally ω 1 -presentable categories The above definitions and properties can be generalized to higher cardinals in order to define more general notions of presentable categories, in particular for the first non-countable cardinal

A partial order (D, ≤) is ω 1 -directed when every countable subset S ⊆ D admits an upper bound in D. A small category I is called ω 1 -directed when it is isomorphic to an ω 1 -directed partial order (D, ≤).

Given a diagram d : I → C in a category C, we say that it is an

Let C ∈ CAT. An object P ∈ C is ω 1 -presentable when its hom-functor

A locally small category C ∈ CAT is locally ω 1 -presentable when (i) it has all small colimits, (ii) every object of C is an ω 1 -directed colimit of locally ω 1 -presentable objects, (iii) the full subcategory of C whose objects are the ω 1 -presentable objects is essentially small.

Proposition A.1.11. A locally ω 1 -presentable category is complete.

Proof. See [1, Corollary 1.28].

Proposition A.1.12. Given a functor F : C → D between two locally ω 1 -presentable categories C and D, the following hold:

(i) F is left adjoint if and only if it preserves colimits, (ii) if F preserves limits and ω 1 -directed colimits, then it is right adjoint.

We stop the copy-and-paste here and refer the reader to [START_REF] Adámek | Locally Presentable and Accessible Categories[END_REF] for other properties shared by locally ω 1 -and finitely presentable categories.

A.2 Essentially algebraic theories

Verifying that some category is locally finitely presentable with the above definition can be tedious. A simpler way consists in describing it as the category of models of some essentially algebraic theory. The latter is similar to an algebraic theory (theory of monoids, theory of groups, etc.), except that operations with partial domains are allowed, as long as those domains are specified by equations. Another interesting property is that morphisms between such theories induce functors between the associated categories of model, and those functors are moreover right adjoints and preserve directed colimits. The main reference here is [1, Section 3.D].

Definition Given a set S, an S-sorted signature is the data of a set Σ of symbols such that each σ ∈ Σ has an arity under the form of a finite sequence (s i ) i∈N * n of elements of S for some n ∈ N, and a target in the form of an element s ∈ S and we write

such a symbol σ of Σ with such arity and target.

Let (x i ) i∈N be a chosen sequence of distinct variable names. Given a set S, an S-sorted context is the data of a finite sequence Γ = (s i ) i∈N * n of elements of S for some n ∈ N. Under the context Γ, the variable x i should be thought "of type s i " for i ∈ N n so that we often write

Given a set S and S-sorted signature Σ and context Γ, we define Σ-terms on Γ together with judgements Γ t : s where t is a Σ-term and s ∈ S, inductively as follows:

-if Γ = (s i ) i∈N * n for some n ∈ N and s 1 , . . . , s n ∈ S, then, for every i

Note that s is uniquely determined by t in a judgement Γ t : s.

An essentially algebraic theory is a tuple

where -S is a set, -Σ is an S-sorted signature, -E is a set of triples (Γ, t 1 , t 2 ) where Γ is an S-sorted context, and t 1 , t 2 are Σ-terms on Γ such that there exists s ∈ S so that Γ t i : s for i ∈ {1, 2},

of Σ t -terms such that there exists s ∈ S so that (x 1 : s 1 , . . . , x n : s n ) t i : s for i ∈ {1, 2}.

The set S represents the different sorts of the theory, the set Σ the different operations that appear in the theory, the set E the global equations satisfied by the theory, the set Σ t the operations whose domains are total, and the function Def the equations that define the domains of the partial operations. Given such an essentially algebraic theory T, a model of T, or T-model, is the data of -for all s ∈ S, a set M s , -for all σ :

-for every triple (Γ, t 1 , t 2 ) ∈ E where Γ = (s i ) i∈N * n for some n ∈ N and sorts s 1 , . . . , s n ∈ S, given a tuple ȳ = (y 1 , . . . ,

where, given an S-sorted context Γ = (s i ) i∈N * n , a sort s ∈ S, a Σ-term t such that Γ t : s, and a tuple ȳ = (y 1 , . . . , y n ) ∈ M s 1 × • • • × M sn , the evaluation of t at ȳ, denoted t ȳ, is either undefined or an element of M s , and is defined by induction on t by -if t = x i for some i ∈ N * n , then t ȳ is defined and

for some k ∈ N * and Σ t -terms t 1 , . . . , t k , then t ȳ is defined if and only if t 1 ȳ, . . . , t k ȳ are defined and M σ is defined at t 1 ȳ, . . . , t k ȳ and, in this case,

Given two models M and M of T, a morphim of T-model between M and M is a family of functions f = (f s :

-for all σ :

We then write Mod(T) for the category of T-models and their morphisms. We say that a (big) category C ∈ CAT is essentially algebraic when it is equivalent to the category of models of some essentially algebraic theory. Identifying a category as essentially algebraic enables to deduce that it is locally finitely presentable, since the two notions are the same: Theorem A.2.1. Given a category C ∈ CAT, C is essentially algebraic if and only if it is locally finitely presentable.

Proof. See the proof of [START_REF] Adámek | Locally Presentable and Accessible Categories[END_REF]Theorem 3.36].

Example A.2.2. The category Set is essentially algebraic since it is the category of models of the essentially algebraic theory ({s}, ∅, ∅, ∅, ⊥). m(m(x 1 , x 2 ), x 3 ) = m(x 1 , m(x 2 , x 3 )) in the context (x 1 : s, x 2 : s, x 3 : s).

In particular, it gives a simple proof that Mon is locally finitely presentable.

Example A.2.4. The category Cat of small categories is essentially algebraic since it is the category of models of the essentially algebraic theory T cat = (S, Σ, E, Σ t , Def) defined as follows. The set S consists of two sorts c 0 and c 1 corresponding to 0-cells and 1-cells, and

Moreover, E consists of the equations -∂ - 0 (id 1 (x 1 )) = x 1 and ∂ + 0 (id 1 (x 1 )) = x 1 in the context (x 1 : c 0 ),

Finally, Σ t = {∂ - 0 , ∂ + 0 , id 1 }, and Def( * ) is the singleton set containing the equation ∂ + 0 (x 1 ) = ∂ - 0 (x 2 ). This shows that Cat is a locally finitely presentable category.

Morphisms of theories

and which maps morphisms of models as expected. The functors induced this way by morphisms between theories have good properties:

Theorem A.2.5. Given a morphism (f, g) : T → T between two essentially algebraic theories T and T , the functor Mod((f, g)) is a right adjoint which preserves directed colimits.

Proof. The fact that it is a right adjoint is given by [START_REF] Palmgren | Partial Horn logic and cartesian categories[END_REF]Theorem 5.4]. Moreover, one easily verifies that the directed colimits are computed pointwise in both Mod(T) and Mod(T ), so that they are preserved by Mod((f, g)).

Remark A.2.6. A more general definition of morphisms between essentially algebraic theories for which Theorem A.2.5 holds can be defined. However, it would require the introduction of formal deduction systems, which would be quite long and technical. This would be in vain since our definition of morphisms is enough for our purposes.

Example A.2.7. One can define the essentially algebraic theory T grp of groups from the one of monoids given in Example A.2.3 by adding a symbol i : s → s representing a total function, and by adding the equations m(i(x 1 ), x 1 ) = e and m(x 1 , i(x 1 )) = e in the context (x 1 : s). The canonical embedding T mon → T grp induces a functor Grp → Mon between the categories of groups and monoids which is the expected forgetful functor. This functor is a right adjoint and preserves directed colimits by Theorem A.2.5.

Example A.2.8. The essentially algebraic theory

exhibits the category Gph of graphs as an essentially algebraic category. Recalling from Example A.2.4 the definition of T cat , the mappings d - 0 → ∂ - 0 and d + 0 → ∂ + 0 define a morphism of essentially algebraic theories T gph → T cat , which induces a functor Cat → Gph that is the expected forgetful functor. This functor is a right adjoint and preserves directed colimits by Theorem A.2.5.