added publication data to:

- Chris Kapulkin, Peter LeFanu Lumsdaine,
*The homotopy theory of type theories*, Advances in Mathematics**337**(2018) 1-38 (arXiv:1610.00037, doi:10.1016/j.aim.2018.08.003)

or rather, maybe, Isaev 16

]]>added pointer to Isaev 18. This seems to be pretty useful.

Peter Lumsdaine pointed to this today as a parallel/alternative to the approach he was presenting here (and Bas Spitters kindly unraveled what the pointer was pointing to)

]]>Another problem with this:

take the image under their equivalence of the toposes inside all locally cartesian closed categories. That gives a 2-category of type theories equivalent to that of toposes. These are the geometric type theories.

that just occurred to me is that in this 2-category the morphisms will correspond to locally cartesian closed functors (between toposes). Surely in the 2-category of geometric type theories the morphisms should be (inverse image functors of) geometric morphisms.

]]>any further news on the directed HoTT of Denis-Charles (#15)?

He’s communicated privately with me about it. I wasn’t convinced by what he had to say at the time, but I look forward to reading more if and when he ever writes it down.

]]>Interesting times. I wonder if there’s some greater power of expression building in dependency intrinsically in some future dependent type $n$-theory that we haven’t seen before. Looking back I remember Urs being highly impressed by opetopic type theory, in this discussion. But dependent types hadn’t been given definitive expression at that time (#3).

By the way, any further news on the directed HoTT of Denis-Charles (#15)?

]]>I’m now writing a Cafe blog post about $n$-theories, and as I do so, I’m coming to the conclusion that I was wrong back in #81, and you right in #82. An $n$-theory does have an $n$-category of models, which means that its models are structured $(n-1)$-categories. I was misled by the fact that HoTT appears to be a theory of $(\infty,1)$-categories, but actually it is a theory of certain 1-categorical *presentations of* $(\infty,1)$-categories (“tribes”). In particular, it doesn’t have a *judgment* for higher cells, only for objects and morphisms; the higher cells are represented implicitly as morphisms into a path-type. As such, it is simply a 2-theory (a doctrine), and any particular 1-theory in that doctrine is a structured 1-category. Similarly, Riehl-Shulman directed type theory is implicitly (sort of) about an $(\infty,2)$-category, but explicitly it is only about another particular kind of 1-categorical presentation, so it is again simply a 2-theory.

The spectrum/pyramid of presentations quoted in #76, though, I still believe fails when we get to dependent type theory, where we can’t distinguish any more between types, terms, and axioms, or at least we can’t distinguish them in the sense of giving all the types, then giving all the terms, then giving all the axioms. Peter Lumsdaine explained this to me very well in terms of a ladder of complexity for syntactic presentations and their corresponding universal properties.

- In the simplest case, you can give the entire presentation first and only
*then*start generating things freely from it. For instance, free categories are generated by directed graphs, and you can specify a directed graph without mentioning any part of the structure of a category; only afterwards do you take strings of composable arrows to be the morphisms in your free category. In this case the universal property is a simple adjunction $F : Pres \leftrightarrows Alg : U$ between presentations and algebras. - In the next simplest case, you have a sequence of “layers of dependency” in which when specifying the generators at layer $n+1$ you have to refer to the
*free structure*generated from the generators in level $n$. For instance, free 2-categories are generated by 2-computads, and in order to specify the 2-cells in a computad you have to already have taken strings of the generating 1-cells as in the free category that they generate, to be the domain and codomain of the 2-cells. In this case the universal property is a sequence of adjunctions $F_n : n Pres \leftrightarrows : Alg : U_n$ defined inductively, with the definition of the category $n Pres$ (and the adjunction $F_n\dashv U_n$) involving the previously defined adjunction $F_{n-1} \dashv U_{n-1}$, as for instance described for globular operads at computad. - In the final case, such as dependent type theory, there is not even any division into layers.
*Every*generator has a type which can refer arbitrarily to the previous generators and all the structure generated from them freely. In this case one natural way to express the universal property of a “presented object” is as a cell complex, in which each generator is added on by a pushout that glues it to whatever structure was generated freely by the previous generators. A “category of presentations” can only be defined inductive-recursively together with its “free functor”, or perhaps after the fact as the category of coalgebras for an awfs.

In the first two cases, I believe there is a “spectrum of realization” for theories that realizes at some layer and above but not below it. But in the third case I don’t see how to do this.

]]>So is it right then that as we ascend the ladder of whatever is doing the indexing, the categorical dimension increases: a category of types, a 2-category of modes? Perhaps were one to want to relate different 2-categories of modes, this would require higher indexing. This process tops out somewhere with the trivial $n$-category of higher modes. So a non-modal unary type theory could be seen as a modal unary type theory indexed by a trivial $\mathcal{M}$. (Cf. that “untyped is uni-typed” idea.)

And presumably at all levels of indexing there is something like the spectrum of presentations of the first quote in #76. So in the case of slide 29, I could present that cartesian monoidal 2-category of modes via the generators or, at the other extreme, as the walking model with all rules of the 3-theory applied.

Stuff-structure-property isn’t applying to the groupoidal level but across a given indexing level.

]]>In that case, yes. I’m not sure whether I believe that that’s always the case. But even that is enough to break the pyramid picture, since an $(\infty,2)$-category still has $\infty$ many levels of stuff-structure-property.

]]>Isn’t that just down to the second number? So the 2-theory HoTT has the $(\infty, \mathbf{2})$-category of $(\infty, 1)$-toposes as semantics.

We’re going wrong in that work in #83 by running the dependency levels together with $n$-groupoid levels. But iterated dependency is a good idea.

]]>I think the $n$ is related to a *different* category level. (-:O I’m not sure how best to explain this, but maybe it helps to just point out that HoTT is a theory of $(\infty,1)$-categories, but it is still just a 2-theory?

I knew bells were ringing. The idea of an iterated dependency was what John Baez and I were discussing in Minneapolis. About the only glimpse of this is in a comment here. Curiously we thought two levels of dependency had a modal flavour.

We didn’t begin to achieve the intricacy of your modal dependent type 2-theory, but those metatypes are pointing somewhere in the direction of your modes.

]]>@Mike#81

I think the length of the stuff-structure-property stratification at any fixed level of $n$-theories would probably depend on the category level (or dependency structure) of the theory in question, rather than on $n$

I thought the $n$ of $n$-theory *is* supposed to be related to the category level. You have on the semantic side (slide 33):

A 2-theory is a structured 2-category freely generated by something…

and

]]>A 3-theory is a 3-category like “2-categories”,“cartesian monoidal 2-categories”…

@David #78: Yes, this should generalize somewhat. However, when you get to things like dependent type theory, the distinction between “types” and “terms” and “axioms” is no longer straightforward. And even if we ignore that problem, I think the length of the stuff-structure-property stratification at any fixed level of $n$-theories would probably depend on the category level (or dependency structure) of the theory in question, rather than on $n$, so that you wouldn’t get a pyramid.

@David #80: One would hope, yes, but I have no idea yet what such a “4-theory” would mean.

]]>Where does one stop with the hierarchy? If unary, simple and dependent are three kinds of type 3-theories, do they take their place in a 4-theory?

I guess for each $n$ there’s the vacuous $n$-theory. In the doctrine case, this was described as the doctrine of no structure at all.

But perhaps first I’d need to know what a syntactic formulation of a type 3-theory looks like.

]]>Urs, check out #74. Do you see how the category of abelian groups corresponds to the syntactic axiom $\forall x \forall y. (x y = y x)$, and how there is no corresponding first-order axiom corresponding to the category of nilpotent groups?

]]>That’s just the same issue with new words plugged in.

No, it’s not! That’s the point I’m making, which is not just a terminological one: *not every* collection of geometric 1-theories is a 2-theory. In the case of geometric 1-logic, the collection of “geometric 1-theories” does coincide with a particular 2-theory, but in the case of “geometric type theory” the collection of “geometric type 1-theories” does not correspond to any yet-known 2-theory. I think this is what Vickers would have meant. The standard terminology is ambiguous, but the people who use it generally know when they are using “theory” to mean what I would call a 1-theory and when what I would call a 2-theory, and it seems clear to me from Vickers’ usage that “geometric type theory” in this sense should be (but is not yet defined as) what I am calling a 2-theory.

Could a fuller picture than slide 33 of Mike’s talk look something like a pyramid with level $n$ corresponding to $n$-theory in the $n+1$-theory of the level above, and there being a horizontal sequence from the most syntactic to the most semantic, where the passage to the right is driven by closure under entries on a higher level.

Then passage to the right may not be straightforward in that it may be hard to determine identities there (such as in the word problem for groups). And the passage back to the left may be difficult (such as in deriving presentations). Sometimes there are reconstruction theorems which allow passage to the left, but maybe just up to some equivalence of presentation.

Then the task of left passage having formed a sub-n-category at some point in the pyramid may also be problematic, since it may be impossible to reconstruct a presentation within the framework of the pyramid (as with Mike’s nilpotent group example).

]]>Is there still some of the subtlety to capture from that discussion on What is a Theory?

So it seems like a theory (in any given doctrine) can be considered at various different levels of “completedness” or “embodiment.” From least to greatest, we have:

- An axiomatization in terms of types, operations, and axioms.
- The seemingly more traditional notion, with generating types and operations fixed, but the “axioms” are closed under implication.
- Something like a (generalized) operad/multicategory, where the generating types are fixed, but the operations are closed under composition and satisfaction of the axioms.
- A fully embodied walking model, in which all the type-constructing rules are also fully applied.

and at the end

Perhaps the conclusion to draw is that there is no one “traditional” notion of morphism of theories; we have (at least) four possible categories of theories (per doctrine) and they are all potentially interesting. All the more reason to have good systematic names for them.

Now we have 3-theories, they’ll be more levels to worry about. Is the property-structure-stuff framework worth reviving, as suggested there?

]]>So you could, I guess, define a “geometric type 1-theory” to be a dependent type 1-theory whose corresponding lccc is a topos.

All right! That’s the resolution which I had suggested above, only that I thought you would have a “0” here instead of “1”. Whichever number it is, it is good that we have determined it now!

However, this would not be a “dependent-type-theory refinement of geometric logic”, because “geometric logic” is not just a collection of syntactic 1-theories, but a syntactic

2-theory

That’s just the same issue with new words plugged in. So it’s geometric 1-logic then. The key fact is that logic is but a fragment of type theory. If your terminology does not reflect this, I’d say it’s missing something.

I do appreciate that you are proposing more find-grained terminology. But given the common existing terminology, it is a little disingenuous to behave as if you don’t understand anymore what people say in the classical terminology.

Better than exclaiming “I don’t know what an X-theory is!!” (implying, since you are the expert, that your discussion partner is not making any sense) would be to say “I know what you mean, but just saying ’X-theory’ is, while established practice, a little ambiguous. What you mean is what I suggest to call an ’X-1-theory’, in the terminology that I proposed, to be frank, just the other day.”

]]>Maybe it will help to bump it down a notch. Fix a particular 1-theory, say the 1-theory of groups (in the 2-theory of finite-product theories, in the 3-theory of simple type theory). A syntactic 0-theory is a group presentation; a semantic 0-theory is a group. The syntactic 1-theory of groups consists of the operations and axioms of a group, while the semantic 1-theory of a group is the category of groups. The rules of the syntactic 1-theory (the operations and axioms of a group) can be applied to a syntactic 0-theory (group presentation) to incarnate it as a semantic 0-theory (the group presented by a group presentation). A model of such a group presentation $\langle G | R \rangle$ in a group $H$ is an interpretation of the generators $G$ as elements of $H$ such that the relations $R$ are satisfied; the universal property of presented groups says that this is equivalent to a group homomorphism from the group presented by $\langle G|R\rangle$ into $H$.

Now suppose we are interested in some subcategory of groups, such as abelian groups, torsion-free groups, nilpotent groups, etc. In the semantic world we can just say “consider the full subcategory of X-groups”, obtaining a category that one might be tempted to call a new “semantic 1-theory”. But the corresponding sub-class of group presentations does not necessarily correspond to any syntactic 1-theory, and certainly not one in the same 2-theory. Abelian groups, yes: add the commutativity axiom, which can be expressed in the same 2-theory (finite-product theories). But torsion-free groups and nilpotent groups can’t be axiomatized as finite-product theories: I believe torsion-free groups are a geometric theory, while probably nilpotent groups require higher-order logic.

Similarly, when we go back up a level, it’s not obvious that the sub-2-category of toposes within the semantic 2-theory of lccc’s corresponds to any *syntactic* 2-theory in the same dependent type 3-theory.

Firstly, I’m not really happy with calling the objects in the 2-category on the left (the “syntax side”) “theories” of any sort, despite what various people in the literature do. To me a syntactic 1-theory is a syntactic object. I would call the objects of that 2-category on the left by the actual categorical structure that they are (“categories with families” in Clairambault-Dybjer).

It is true though that every category with families is presentable by some syntactic 1-theory. So you could, I guess, define a “geometric type 1-theory” to be a dependent type 1-theory whose corresponding lccc is a topos. However, this would not be a “dependent-type-theory refinement of geometric logic”, because “geometric logic” is not just a collection of syntactic 1-theories, but a syntactic *2-theory* (written in the syntactic 3-theory of first-order logic — a 3-theory that I didn’t mention in the talk because it should be subsumed by the 3-theory of dependent type theory). Thus, geometric type theory should also be a syntactic 2-theory, this time written in the syntactic 3-theory of dependent type theory.

We are still talking past each other.

I am looking at that theorem 3.2, the classical statement by Seely, in its improved version.

It uses the following words:

There are 2-functors

$Cont$, that forms a category of contexts of a Martin-Löf dependent type theory;

$Lang$ that forms the internal language of a locally cartesian closed category

that constitute an equivalence of 2-categories

$MLDependentTypeTheories \underoverset {\underset{Cont}{\longrightarrow}} {\overset{Lang}{\longleftarrow}} {\simeq} LocallyCartesianClosedCategories \,.$(I may have typed that nLab version of the statement originally, but I believe this accurately reflects the language used in the corresponding articles.)

There is no mentioning of “2-theory” here. There is mentioning just of “theories”. And these are the objects in the 2-category on the left.

How do you want to call the objects in the 2-category on the left? “1-theories”? I am happy with whatever term you like best.

But since we have an equivalence between these “theories” and locally Cartesian closed cateories, we are entitled to transfer all names of special kinds of objects on the right to left left.

The sub-2-category $Toposes\hookrightarrow LocallyCartesianClosedCategories$ has an essential image

$Lang(Toposes) \hookrightarrow MLDependentTypeTheories$which consists of some more special kind of “theories” – necessarily, since all objects in the 2-category $MLDependentTypeTheories$ are called “theories”, at least by Seely et al.

]]>On the syntactic side, you can’t just take an arbitrary sub-2-category of the 2-category of models of some 2-theory and call it another 2-theory. You need a *syntactic* presentation of it.