{'fraction_non_alphanumeric': 0.06798088752825385, 'fraction_numerical': 0.0077823238247832684, 'mean_word_length': 3.5647120282094815, 'pattern_counts': {'":': 0, '<': 10, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 22, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Weak omega-categories from intensional type theory

We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.

1. Introduction 1.1. Overview. Starting with the Hofmann-Streicher groupoid model [HS98], higher categories have emerged as a natural approach to the semantics of intensional Martin-Löf type theory. In the globular approach to higher categories, a higher category has objects ("0cells"), arrows ("1-cells") between objects, 2-cells between 1-cells, and so on, with various composition operations and laws depending on the kind of category in question (strict or weak, n-or ω-, . . .). The paradigm for semantics of type theory is then (very roughly!) that types (or contexts) are thought of as objects [ This idea has recently been explored by various authors in various directions: see for instance [GG08], [Gar09], [AW09]. One such direction is investigating the structures formed by the syntax of type theory. In particular, it has been suggested that (terms of) any type, considered together with its higher identity types, should carry the structure of a weak ω-category or -groupoid. We will show that this is indeed the case, using the definition of weak ω-category given by Tom Leinster in [Lei04] following the approach of Michael Batanin [Bat98].
(Note that for this construction, based on a specific type A, the dimensions of cells are always one lower than described above: 0-cells will be terms τ : A, 1-cells will be terms ρ : Id A (τ, τ ′ ), and so on. This comes from the general rule that if X, A are objects of an n-category C, then C(X, A) forms an (n − 1)-category whose 0-cells are 1-cells of C, and so on.) While writing this paper, I found that Benno van den Berg had independently discovered a similar proof (proposed in 2006 and completed in unpublished work [vdB]); a development of this is forthcoming in joint work of van den Berg and Richard Garner [GvdB08].

Figure 1: Some cells, composites, and associativities in a strict ω-category
In a weak ω-category, we do not expect strict associativity, so may have multiple composites for a given pasting diagram, but we do demand that these composites agree up to cells of the next dimension ("up to homotopy"), and that these associativity cells satisfy certain coherence laws of their own, again up to cells of higher dimension, and so on. This is exactly the situation we find in intensional type theory. For instance, even in constructing a term witnessing the transitivity of identity-that is, a composition law for the pasting diagram ( • G G • G G • ), or explicitly a term c such that x, y, z : X, p : Id(x, y), q : Id(y, z) ⊢ c(q, p) : Id(x, z) -one finds that there is no single canonical candidate: most obvious are the two equally natural terms c l , c r obtained by applying (Id-elim) to p or to q respectively. These are not definitionally equal, but are propositionally equal, i.e. equal up to a 2-cell: there is a term e with x, y, z : X, p : Id(x, y), q : Id(y, z) ⊢ e(q, p) : Id(c l (q, p), c r (q, p)). In Leinster's definition [Lei04], a system of composition laws of this sort is wrapped up in the algebraic structure of a globular operad with contraction, and a weak ω-category is given by a globular set equipped with an action of such an operad. We generalise this slightly, to define an internal weak ω-category in any suitable category C.
Accordingly, we would like to find an operad-with-contraction P ML Id of all such typetheoretically definable composition laws, acting on terms of any type and its identity types. In fact, rather than using the full type theory for this, it is more convenient to consider the composition laws definable using just the Id-rules, hence also obtaining the construction for a wider class of theories.
The heart of the paper is Sect. 4, where we formalise this idea. We consider ML Id [X], the fragment of intensional Martin-Löf type theory generated just by the structural and Id-rules plus a single generic base type X. The operad P ML Id of definable composition therein laws may then be formally constructed as an endomorphism operad in its syntactic category C(ML Id [X]); and by some analysis of the fragment ML Id [X], we show that P ML Id is contractible.
Since X is generic, P ML Id acts on all other types, giving our main theorem: Theorem. Let T be any type theory extending ML Id , and A any type of T . Then the system of types (A, Id A , Id Id A , . . .) is equipped naturally with a P ML Id -action, and hence with the structure of an internal weak ω-category in C(T ).
To prepare for this, we first lay out in Sect. 2 our presentation of the type theory ML Id , and in Sect. 3 the relevant background on globular operads and their algebras.
2. Type-theoretic setting 2.1. The type theories ML Id , ML Id [X]. Our main theories of interest are the various versions of Intensional Martin-Löf Type Theory, usually given with identity types (Id-types), dependent sums and products ( -and -types), units (1-types), and possibly more base types (natural numbers, Booleans. . .). To cover all these in the main theorem, and for a self-contained presentation, we will work throughout this paper in the fragment ML Id with only Id-types, and construct our operad from this.
Some care is thus required in our choice of presentation; presentations which are equivalent in the presence of -or -types may not be so in their absence. The presentation we use is taken, up to notation, from that of Jacobs [Jac99]; we list in Table 1 the rules assumed, referring to [Jac99] for their statements, except for the Id-rules, given in full in Table 2. A few more of the rules will later be given explicitly, as their precise statements are required.
compatibility with substitution and = The only features perhaps needing comment are the explicit inclusion of exchange rules, and of the extra dependent context ∆ in the Id-rules; these are each natural rules, but often omitted since they are derivable in the presence of Π-types (as discussed on e.g. p.587 of [Jac99]). Note that from Exch and this Id-elim rule, we can derive a still slightly more general elimination rule Id-elim + , as Id-elim but with context Γ, x : A, ∆, y : A, ∆ ′ , p : Table 2: Rules for Id-types To simplify notation when referring to iterated identity types, we introduce the notation (following Warren [War08]) A n for the nth iterated identity type of a type A; that is, if Γ ⊢ A type, then Γ ⊢ A 0 := A type, and inductively Γ, x 0 , y 0 : A 0 , x 1 , y 1 : A 1 (x 0 , y 0 ), . . . , x n , y n : A n (x 0 , y 0 ; . . . ; x n−1 , y n−1 ) We will often omit the superscripts on these when unambiguous. As usual, we will also be inconsistent in suppression of free variables, writing usually e.g. y : Γ ⊢ A( y) type for clarity in simple cases, but sometimes Γ ⊢ A type to avoid unmanageable proliferations of variables.
Finally, for a finite partial order I = {i 1 < . . . < i n }, we will write i∈I x i : A i (or just i∈I A i ) to denote the context x i 1 : A i 1 , . . . , x in : A in .

2.2.
Translations and syntactic categories. For reference on this section (including proofs not given here), see Cartmell [Car86] and Jacobs [Jac99]. From here on, we will consider type theories extending ML Id ; formally, by a type theory we will mean a generalised algebraic theory in the sense of Cartmell [Car86], together with an interpretation of the Id-rules in T .
Recall that a translation F from such a type theory T into a type theory S consists of suitable mappings of types, terms, and derivable judgements, taking each judgement Γ ⊢ A type in T to a judgement F (Γ) ⊢ F (A) type in S, and so on, preserving Id-types and their term-constructors, considered up to definitional equality. (In other words, it is a morphism of generalised algebraic theories, preserving the interpretation of the Id-rules.) Given T , we write T [X] for the result of adjoining to T a fresh base type X ⊢ X type X-form with no term formation rules. For any S, a translation F : T [X] G G S then consists of a translation F ′ : T G G S together with a closed type of S. Stating this universal property precisely, in the particular case that we will need: Proposition 2.1. If S is any type theory extending ML Id , and A any closed type of S, then there is a unique translation F S,A : ML Id [X] G G S preserving Id-types and their termconstructors and with F S,A (X) = A.
For any type theory T , there is a syntactic category C(T ), having as objects the closed contexts Γ of T , and as arrows f : Γ G G ∆ suitable strings of terms in context Γ (context maps), all up to definitional equality. Moreover, a translation F : T G G S induces a functor C(F ) : C(T ) G G C(S); in other words, we have a functor C(−) : Th G G Cat. Context maps are sometimes known as substitutions, since substitution along them is an important derived rule: if y : Γ ⊢ A( y) type and f : x : Γ G G ∆ is a context map, then x : ∆ ⊢ A(f ( x) type. When suppressing free variables, we will write this as ∆ ⊢ f * (A) type.
We will need a simple proposition on limits in syntactic categories: Proposition 2.2. Suppose Γ = i∈I x i : A i is a context in T , and F ⊆ P(I) a set of subsets of I, closed under binary intersection and with F = I, such that for each J ∈ F, Γ J = i∈J x i : A i is also a well-formed context. Then the Γ J 's and dependent projections between them give a diagram and the dependent projections Γ G G Γ J express Γ as its limit: Here dependent projections are the obvious context morphisms from a context to any well-formed subcontext, constructed from the Vble, Wkg and Exch rules.
A familiar special case asserts that if Γ ⊢ A type and Γ ⊢ B type, then the following square of projections is a pullback: The proof of the general proposition is essentially the same.
To relativise the constructions of this section to dependent types and contexts over a (closed) context Γ = 0≤i<n x i : A i of T , we can consider the slice type theory T /Γ, given by adjoining to T a "generic term of type Γ", i.e. n new constant symbols c i and axioms ⊢ c i : A i (c 0 , . . . , c i−1 ). Closed types (resp. terms, contexts) of T /Γ then correspond precisely to types (terms, contexts) of T in context Γ.

Globular operads and weak ω-categories
As described in the introduction, we want to describe "the globular operad of composition laws". Accordingly, we recall briefly in this section what a globular operad is, and how it formalises the intuition of a set of composition laws for pasting diagrams with structure specifying how these laws themselves compose. For a slightly (resp. much) fuller treatment, and background on strict higher categories, see Leinster [Lei02] (resp. [Lei04]).

Globular sets and operads.
A globular set A • is a presheaf on the category G generated by arrows subject to the equations ss = ts, st = tt (omitting subscripts on the arrows, as usual). We thus have the category G := [G op , Sets] of globular sets and natural transformations between them. More generally, a globular object in a category C is a functor A • : G op G G C. Explicitly, a globular set A • has a set A n of "n-cells" for each n ∈ N, and each (n + 1)cell x has parallel source and target n-cells s(x), t(x), as illustrated in the first line of Fig. 1 x, t(z) = y}, the set of (n + 1)-cells from x to y.
Our notation will vary: we will typically call globular objects A • , B • , . . . when emphasising the point of view of the category C, or A, B, . . . when working more in [G op , C].
Example 3.1. For any topological space X, there is a globular set Π ω (X) in which 0-cells are points of X, 1-cells are paths between points, 2-cells are homotopies between paths keeping endpoints fixed, and in general, n-cells are suitable maps H : [0, 1] n G G X, viewed as homotopies between (n − 1)-cells.
Example 3.2. For any type A in a type theory T , the contexts along with their dependent projections, form a globular object A • in C(T ).
Any strict ω-category (as sketched in the introduction) has an evident underlying globular set, and in fact there is an adjunction (moreover monadic) F : str-ω-Cat : U , giving rise to the "free strict ω-category" monad (T, µ, η) on G. Cells of T A • are free (strictly associative) pastings-together of cells from A • , including degenerate pastings from the identity cells of F (A • ) (as shown in figure 2). In particular, T 1 (where 1 denotes the terminal globular set, with just one cell of each dimension) consists informally of pastings of this sort, but without labels on the cells. This is the crucial globular set of pasting diagrams. A peculiarity of T 1 is that the source and target of any pasting diagram are equal; for this ambivalent operation we write ∂π := s(π) = t(π).
Every pasting diagram π ∈ T 1 n has an associated globular setπ-intuitively, the set of cells appearing in π, as shown in our pictures of pasting diagrams throughout. We then 8 P. LEF. LUMSDAINE have maps of globular setsŝ k ,t k : ∂ k π G Gπ , embedding ∂ k π as the (n − k)-dimensional source or target ofπ.
Taking categories of elements then gives categories π := Gπ , with objects the cells ofπ and arrows into each cell c from its sources and targets s k (c), t k (c), and with a functor dim : π G G G giving the dimension of each cell; π may be seen as the shape of the canonical diagram of basic cells whose colimit in G givesπ.
For more discussion of these and other various ways of looking at a pasting diagram, see Street [Str00].
A globular operad is a globular set P with maps a : e. e and m are maps over T 1), satisfying the axioms Considering the fibers of a, we may view P as a family of sets P (π) of "π-ary operations" for each π ∈ T 1: an element p of P (π) is seen as a formal operation symbol, taking πshaped labelled pasting diagrams as input and returning n-cells as output. The map e then gives us an n-cell "identity" operation for each n, while m allows us to compose operations appropriately.
For readers not familiar with this definition, it may be helpful to first contemplate the simpler case of plain operads, defined by diagrams as above but with E = Sets and T the "free monoid" monad. These thus have arities valued in T 1 ∼ = N, and present certain finitary, single-sorted equational theories [Lei04, 2.2]. However, "operad" from here on will always mean "globular operad"; we will not deal further with any other kind.
A map f : P G G Q of globular operads is a map of underlying globular sets commuting with a, e and m.
An action of a globular operad P on a globular set A is a composition map c : Informally, this implements the "formal operations" in P as actual composition operations on A. An element of T A× T 1 P over some π ∈ T 1 n is a π-shaped diagram x with labels from A, together with a π-ary operation p of P ; c tells us how to apply p to x, yielding a single n-cell c( x, p) of A.
A P -algebra is a globular set A together with an action of P on A. A map f : A G G B of P -algebras is a map of globular sets commuting with the P -actions. We denote the resulting category by P -Alg. Example 3.3. The globular set T 1 is itself trivially an operad (indeed, the terminal one), with a = 1 T 1 , i.e. T 1(π) = 1 for every π; a T 1-algebra is then exactly a strict ω-category. This fits with our description above of a strict ω-category having a unique composition for each pasting diagram.
Weak ω-categories will also be described as algebras for a certain globular operad; to find a suitable operad, we need to specify a little extra structure.
A contraction on a map d : A G G B of globular sets is a choice of liftings for fillers of parallel pairs: that is, for each parallel pair x, x ′ ∈ A (with the convention that all 0-cells are parallel), a map χ x, A globular operad with contraction is a globular operad P with a contraction on the map a : P G G T 1; this ensures both that enough composition operations exist in P , and that the operations will be associative up to cells of the next dimension, themselves satisfying appropriate coherence laws up to yet higher cells, and so on.
It is shown in [Lei04] that the category of globular operads with contraction has an initial object L; this gives the key definition: Definition 3.4. A weak ω-category is an L-algebra, where L is the initial operad-withcontraction.
A map O G G P of operads induces a "restriction of scalars" functor P -Alg G G O-Alg; so if we have an algebra A for any operad P with contraction, restriction along the unique operad-with-contraction map L G G P endows A with the structure of a weak ω-category. Definition 3.7. For a globular object A • in a category C, and a pasting diagram π ∈ T 1 n , we define A π := lim ← −c∈ π A dim c , "the object of diagrams of shape π in A • ", whenever this limit exists in C. The mapŝ An illustration may be useful here: the definition of A π says, for instance, that if giving the object of 0-composable pairs of 2-cells in A. Similarly, if π is the basic n-cell, then A π = A n .
In the case C = Sets, the sets A π are precisely the fibers of the map T ! : T A G G T 1, by the description of T as a familially representable functor ([Lei04, 8.1]).
Proposition 3.8. If A • is a globular object in a category C, and the objects A π exist, then there is an operad End C (A • ), the endomorphism globular operad of A • , in which (for π ∈ T 1 n ) an element of End C (A • )(π) is a sequence of maps (σ 0 , τ 0 ; σ 1 , τ 1 ; . . . , τ n−1 ; ρ), commuting appropriately with the source and target maps, in the sense that In other words, an element of End(A • )(π) is a map ρ composing diagrams of shape π in A • to basic n-cells of A, extending maps (σ i , τ i ) composing their sources and targets in each lower dimension.
Such a diagram of maps may be more abstractly seen as a natural transformation ρ : A ≤π G G A ≤n between two evident functors A ≤π , A ≤n : Proof. This construction of the endomorphism operad is a straightforward generalisation of the topological case given in [Lei04,9.2.7]. The proof requires more technical background on globular operads from [Lei04] than can be recalled here; readers unfamiliar with this are encouraged to "black-box" this proof and skip to the last few paragraphs of the section. Recall from [Lei04,6.4] that if S is a cartesian monad on a locally cartesian closed category E, then any object A of E has an endomorphism S-operad End S (A) given by the exponential in E/S1 of the objects SA G G S1, S1 × A G G S1; in the internal language of E this may be written as the dependent sum of exponentials: End S (A) = π:S1 [SA π , A]. Now, in the case of ( G, T ), this gives for any globular set A • an endomorphism globular operad End T (A • ). For π ∈ T 1 n , an operad element p ∈ End T (A • )(π) then corresponds to a commutative triangle But this in turn corresponds to a map y(n) × π T (A • ) G G y(n) × A • in G/y(n) and hence, via the equivalence G/y(n) ≃ [(G/n) op , Sets], to a map ρ : A ≤π G G A ≤n as described above. Now, given any category C, consider the category Composition with T induces a cartesian monad T * on E. Since E is a presheaf category, it is locally cartesian closed; so any object Y = Y (−) • of E has an endomorphism T * -operad End T * (Y (−)).
Using the familial representability of T and the fact that Γ preserves limits, we have a cartesian lax map of cartesian monads (Γ, κ) : (E, T * ) G G ( G, T ), and hence an induced functor Γ * : T * -Operads E G G T -Operads G . As in the case E = G, we wish to show that this agrees with the explicit description of End C (A • ) given in Proposition 3.8. Again, an element p ∈ End C (A • )(π) is by definition a triangle in G: which corresponds, by the adjunction ∆ ⊣ Γ and the definition of End T * (C), to a map ∆(y(n)) × ∆(π) T * (y(A • )) G G ∆(y(n)) × y(A • ) Since all limits and colimits are pointwise, this corresponds to a family of maps natural in C, so (as before) to a natural family of maps i.e. to a map ρ (−) : y(A • ) ≤π G G y(A • ) ≤n . But since y is full and faithful and preserves all existing limits, if the objects A π exist in C then this corresponds in turn to a map ρ : A ≤π G G A ≤n , as desired.
We can now extend the definitions of the previous subsection. An action of an operad P on A • is a map of operads P G G End(A • ). (If C = Sets then this agrees with our earlier notions of an action on a globular set, by [Lei04, 6.4]). A P -algebra in a category C is a globular object in C together with a P -action; an internal weak ω-category in C is an L-algebra in C.
Moreover, an action of P on A • induces an action of P on the globular set C(Y, A • ) for any Y ∈ C, since C(Y, −) : C G G Sets preserves all limits, and hence we have maps

The contractible globular operad P ML Id
In this section, we construct the promised operad P ML Id of all definable composition laws; we then show that it is contractible, and describe (in the main theorem) how it acts to give the desired weak-ω-category structures on types.
4.1. Construction of P ML Id . We saw above that for a type A in a type theory T extending ML Id , the contexts x 0 , y 0 : A, x 1 , y 1 : A 1 (x 0 , y 0 ) . . . , z : A n (x 0 , y 0 . . . , x n−1 , y n−1 ), and the dependent projections between them form a globular context A • : G op G G C(T ). In particular, the generic type X gives a globular context X • in C(ML Id [X]). Using the machinery of the previous section, it is now easy to describe P ML Id : it will be End C(ML Id [X]) (X • ). However, since C(T ) does not have all finite limits in general, to use the description of End C(T ) (A • ) provided by Proposition 3.8 we must construct contexts Γ π exhibiting the objects A π .
Accordingly, suppose we are given π ∈ T 1 n , with associated globular setπ. There are various ways of putting a total order on the i-cells ofπ for each i ≤ n; pick any such.
(There is in fact a canonical choice of such orderings, using the representation of pasting diagrams as Batanin trees ( [Bat98], [Lei04,8.1]). This choice has some good compatibility between the orderings on different pasting diagrams, which will later spare us some use of Exch rules, so for simplicity we will assume it is the ordering chosen; however, since this is purely cosmetic, we will not go into the details here.) Then take Γ π to be the context c∈π 0 which we met back in the introduction. Note that we also have projections src, tgt : Γ π G G Γ ∂π .
We make no attempt to give a formal syntactic description of composition within this operad, but in specific cases it is "exactly what you would expect", and is essentially just substitution. Definition 4.3. As as special case of the above construction, we take the operad of all definable composition laws on the generic type.
For general T , A, we cannot expect End C(T ) (A • ) to be contractible: contractibility implies (at least) that any two elements of End C(T ) (A • )(•) are connected by an element of , or in other words that any two terms x : A ⊢ τ (x), τ ′ (x) : A are propositionally equal, which clearly may fail. However, in the specific case of P ML Id , we do wish to show contractibility, since this is the operad which naturally acts on any type.
Given π, such a parallel pair amounts to terms (σ i , τ i ) 0≤i<n as in the definition of a composition law for π, and a filler is a term ρ completing the definition; that is, we seek to derive a judgment x : Γ π ⊢ ρ( x) : Id(σ n−1 (src x), τ n−1 (tgt x)). Playing with small examples (the reader is strongly encouraged to try this-to derive, for instance, the composition and associativity terms mentioned in the introduction) suggests that we should be able to do this by applying Id-elim (possibly repeatedly, working bottom-up as usual) to the variables of identity types in Γ π . Id-elim says that to obtain ρ, it's enough to obtain it in the case where one of the variables is of the form r(−), and its source and target variables are equal; and by repeated application, it's enough to obtain ρ in the case where multiple higher cells have had identities plugged in in this way. Now, since the terms σ i , τ i have themselves been built up from just the Id-rules, as we plug r(−) terms into them and identify the lower variables, they should sooner or later collapse by Id-comp to be of the form r i (x) themselves. In particular, after applying Idelim as far as possible, plugging in reflexivity terms for the higher variables and contracting all variables of type X to a single x : X, the σ i , τ i should all reduce to reflexivity terms, and in particular σ n−1 = τ n−1 = r n−1 (x), so we can take the desired filler to be x : X ⊢ r n (x) : Id(r n−1 (x), r n−1 (x)).
Below, we formalise this argument. The crucial lemma is that the context x : X is an initial object in C(ML Id [X]): that is, since any context Γ in ML Id [X] is built up just from X and its higher identity types, there is always a unique way to substitute x and its reflexivity terms r i (x) for all variables of Γ, and when we subsitute these in to any context morphism σ : Γ G G Γ ′ , the result must again reduce to terms of this form.  , for instance, it is easily seen to be false, since for instance there is no term x : X ⊢ τ : Π y:X Id(x, y).

X is initial in ML
Proof. We work by structural induction (as, essentially, we must, since this is a property of the theory ML Id [X] which can fail in extensions). So, given any derivation δ of a judgement J in ML Id [X], we recursively derive various terms and/or judgments, depending on the form of J, assuming that we have already done so for all sub-derivations of δ. The form of the terms and judgements we derive will depend on the form of J as follows: Here, for a context Γ = y 0 : A 0 , . . . , y n : A n ( y <n ), we write r Γ for the context map . . Moreover, applying (*) and (**) above to this definition shows that the maps r Γ respect definitional equality in Γ, and are preserved by context maps in that for any f : ∆ G G Γ, we have f (r ∆ (x)) = r Γ (x).
Finally, once the induction is complete, applying this last fact together with the definition r (x:X) (x) := x will show that for any other context map f : (x : X) G G Γ, we have f (x) = f (r (x:X) ) = r Γ (x), and so r Γ is the unique such map, as originally desired.
(This last step is an instance of the general categorical fact that given an object X in a category C and natural maps ! Y : X G G Y to every other object, such that ! X = 1 X , it follows that X is initial.) As usual, the induction proceeds by cases on the last rule used in the derivation of J. Most cases are routine; we include here X-form and Wkg-type as examples of these, together with the less straightforward cases of the Id-rules and Subst-type.
Our definitions for the Subst-type and Wkg-type cases ensure, as usual, that the terms constructed do not depend on the derivation of the judgement used. As warned earlier, we will vary for readability between showing dependent variables and leaving them implicit, and hence also between the notations A(f ( x)) and f * A for substitution.
(X-form): in the easiest case, our derivation consists of just the axiom X-form ⊢ X type X-form and so defining r ⊢ X (X) := x, we have x : X ⊢ x : X type as needed.
(Wkg-type): Given a derivation ending x : X ⊢ r Γ,y,y ′ :A ⊢ Id A (y,y ′ ) : Id (r Γ ) * A (r Γ ⊢ A , r Γ,y:A ⊢ A ) But Γ, y : A ⊢ A type may be derived using weakening, and so by our construction for Wkg-type above, r Γ,y:A ⊢ A = r Γ ⊢ A , so we have and so can set r Γ,y,y ′ :A ⊢ Id A (y,y ′ ) := r(r Γ ⊢ A ). (Id-intro): Now we are given a derivation with last step Γ ⊢ A type Γ, y : A ⊢ r(y) : Id A (y, y) Id-intro and wish to show x : X ⊢ r(r Γ ⊢ A ) = r Γ,y,y:A ⊢ Id A (y,y) : (r Γ ) * A. But by our construction of r Γ,y,y ′ :A ⊢ Id A (y,y ′ ) above (our Id-form case), and of r Γ,y:A ⊢ Id A (y,y) from it (our Contr-type case), this is just the definition of r Γ,y,y:A ⊢ Id A (y,y) .
Unwrapping the former term, we have (all in context (x : X)): (r Γ,y,y ′ :A,p:Id(y,y ′ ) ) * (J z.d (y, y ′ , p)) (by induction) = r Γ,y,y ′ :A,p:Id(y,y ′ ) ⊢ C(y,y ′ ,p) (by the definition of r Γ,z:A ⊢ C(z,z,r(z)) using our Wkg-type and Id-elim cases.) If ∆ in the application of Id-elim is non-empty, we have a few more lines, relying inductively on our Subst-rules cases.
(Subst-type): For this case we will need one more piece of notation, generalising the context maps r Γ : for a dependent context ∆ = i A i over Γ, we write r Γ ⊢ ∆ : (x : X) G G (r Γ ) * ∆ for the map built up from terms r Γ,∆ <i ⊢ A i in the obvious way.
So, we are given a derivation ending with the rule Subst-type and we wish to derive a judgement Unfolding the definition of the desired type, we have (by def'n of r Γ ⊢ f * ∆ , i.e. by previous applications of this case) = (r Γ,y:A,∆ ) * B so since by induction x : X ⊢ r Γ,y:A,∆ ⊢ B : (r Γ,y:A,∆ ) * B, we take r Γ,f * ∆ ⊢ f * B := r Γ,y:A,∆ ⊢ B .
The cases for the other structural rules and X-form are straightforward, similar to the Wkg-type case above. , 4.3. Contractibility of P ML Id . We are now ready to show that P ML Id is contractible, arguing along the lines sketched above.
Theorem 4.6. The operad P ML Id is contractible.
Proof. As described above, this amounts to the statement: for every n ∈ N and pasting diagram π ∈ T 1 n , and every sequence (σ i , τ i ) i<n of terms such that , we can find a "filler", i.e. a term ρ with x : Γ π ⊢ ρ( x) : X (σ 0 (src n x), . . . , τ n−1 (tgt x))

We show this by induction on the number of cells in π.
Suppose π has more than one cell. Then it must have some cells in dimension > 1. Let k be the highest dimension in which π has cells, and c be some k-cell ofπ. Now take π −c ∈ T 1 n to be the pasting diagram whose globular set is obtained (up to isomorphism) from that of π by removing c and identifying s(c) and t(c). Now Γ π −c is exactly (up to renaming of variables, and possibly re-ordering if we do not assume that we chose compatible orderings of the cells of pasting diagrams) the context obtained from Γ π by removing the variables x k c and x k−1 t(c) , and replacing any occurrences of the latter in subsequent types by x k−1 s(c) , and we have a natural context map h : Γ π −c G G Γ π given by plugging in x k−1 s(c) for x k−1 t(c) and r(x k−1 s(c) ) for x k c ; and these are exactly right for x : Γ π −c ⊢ ρ −c ( x) : X (σ 0 (src n h( x)), . . . , τ n−1 (tgt h( x))) x : Γ π ⊢ J x k−1 s(c) .ρ −c (x k−1 s(c) , x k−1 t(c) , x k c ) : X (σ 0 (src n x), . . . , τ n−1 (tgt x)) to be an instance of Id-elim + . So to give the desired filler ρ, it is enough to give ρ −c with x : Γ π −c ⊢ ρ −c ( x) : X (σ 0 (src n h( x)), . . . , τ n−1 (tgt h( x))).
But now note that moreover, we can construct context maps (analogous to h if i ≥ k, and just the identity otherwise), and these commute with the maps src and tgt. So for each i < n, we have i.e. the sequence of terms (h * (σ i ), h * (τ i )) i<n are a parallel pair for π −c . So by induction (since π −c has fewer cells than π), these terms have a filler; but this filler is exactly the desired term ρ −c . Thus it is enough to show the existence of fillers in the case where π has just one cell, i.e. where π = (•). But in this case, Γ π = Γ ∂ i (π) = Γ ∂ i (π) = (x : X) for each i < n, and so by the initiality of (x : X) we must have σ i (x) = τ i (x) = r i (x) for each i; so now ρ := r n (x) gives the filler, and we are done.
Unwinding this induction, we can see that it exactly formalises the process described at the start of Subsection 4.2, of repeatedly plugging in higher reflexivity terms for all variables, knowing that the given composites will themselves eventually compute down to higher reflexivity terms.
Note that Lemma 4.4 was applied only at the base case of the induction, and only to show that terms x : X ⊢ σ : Id(r n (x), r n (x)) must be equal to r n+1 (x). A sufficiently strong normalisation result would also imply this, resting on showing that these are the only appropriate normal forms; this could then extend also to the operad End ML I [X] (X • ) of all composition laws of the full type theory, which cannot be shown contractible by the present method. However, working with the fragment ML Id seems more economical, showing that Id-types are the only structure required.

4.4.
Types as weak ω-categories. Putting the above results together, we obtain our main goal: Theorem 4.7. Let T be any type theory extending the fragment ML Id , Γ any closed context of T , A a dependent type over Γ. Then the globular context A • carries the structure of a P ML Id -algebra in C(T /Γ).

Proof. By Proposition 2.1, there is a unique translation F T /Γ,A : ML Id [X]
G G T /Γ taking X to A, and hence taking X • to A • . By Proposition 3.8, this induces an action of P ML Id on A • , and so, since by Theorem 4.6 P ML Id admits a contraction, an action of L (the initial operad-with-contraction) on A • , as desired.
Corollary 4.8. Let T , Γ, A be as above, and ∆ a dependent context over Γ. Then the globular set of terms of types A, Id A , Id Id A , . . . in context Γ, ∆ carries the structure of a P ML Id -algebra, and hence of a weak ω-category.
Proof. This is just the globular set of C(T /Γ)(∆, A • ) of context maps f : Γ, ∆ G G Γ, x 0 , y 0 : A, . . . , x n−1 , y n−1 : A(x 0 , . . . , y n−2 ), z : A(x 0 , . . . , y n−1 ) and so inherits a P ML Id -action, and hence an L-action, from the actions on A • . Remark 4.9 (Functoriality). The construction of the P ML Id -algebra C(T /Γ)(∆, A • ) should be covariantly functorial in T , and contravariantly in Γ and ∆. That is, translations T G G T ′ and context maps Γ ′ G G Γ, ∆ ′ G G ∆ should induce strict maps of P ML Idalgebras, composing appropriately. A proof of this should be fairly straightforward, by an extension of the methods of the current paper; essentially, the missing ingredient is a treatment of maps of internal operad algebras.
More subtly, it should be functorial in A, but only to weak maps: a map of types A G G A ′ should induce weak maps of P ML Id -or L-algebras-that is, weak ω-functors. This seems an altogether trickier question, due partly but not only to the lack, until fairly recently ([Gar08]), of a suitable definition of weak ω-functor. Remark 4.10 (Comparison with [GvdB08]). As mentioned in the Introduction, Richard Garner and Benno van den Berg have independently given ([GvdB08]) a proof of essentially the same result. The core of their approach is the same as that given here: the ω-category action is induced via contractible operads constructed from endomorphism operads of the globular contexts of identity types. The main differences between construction of the present paper and that of [GvdB08] are, roughly, as follows: