In the “Overview”-table (here) I have added pointer to Lambek & Scott 1986, Part I in the line for CCCs.

Also re-arranged the line on dependent linear typed theory to come after that on plain linear types.

]]>To the *Overview*-table (here) I added a line for *bunched logic* $\leftrightarrow$ *dobly closed monoidal category*

polished up all of the following reference items (adding missing publication data and doi-s):

R. A. G. Seely,

*Locally cartesian closed categories and type theory*, Math. Proc. Camb. Phil. Soc.**95**(1984) 33-48 [doi:10.1017/S0305004100061284, pdf]Pierre-Louis Curien,

*Substitution up to isomorphism*, Fundamenta Informaticae,**19**1-2 (1993) 51-86 [doi:10.5555/175469.175471] and: Diagrammes**23**(1990) 43-66 [numdam:DIA_1990__23__43_0]Martin Hofmann,

*On the interpretation of type theory in locally cartesian closed categories*, in*Computer Science Logic. CSL 1994*, Lecture Notes in Computer Science**933**(1994) 427–441 [doi:10.1007/BFb0022273]Pierre Clairambault, Peter Dybjer,

*The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories*, in*Typed lambda calculi and applications*, Lecture Notes in Comput. Sci.**6690**Springer (2011) [arXiv:1112.3456, doi:10.1007/978-3-642-21691-6_10]Pierre-Louis Curien, Richard Garner, Martin Hofmann,

*Revisiting the categorical interpretation of dependent type theory*, Theoretical Computer Science**546**21 (2014) 99-119 [doi:10.1016/j.tcs.2014.03.003, CurienGarnerHofmann.pdf:file]

also added dual intutionistic logic to the list, which corresponds to co-Heyting algebras

Anonymous

]]>propositional logic goes with Lindenbaum-Tarski algebras, and the specific examples of intuitionistic and classical propositional logic go with Heyting and Boolean algebras respectively

Anonymous

]]>added pointer (here) to

- Emily Riehl,
*On the $\infty$-topos semantics of homotopy type theory*, lecture at*Logic and higher structures*CIRM (Feb. 2022) $[$pdf$]$

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).

]]>