Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

April 26, 2018

What Is an n-Theory?

Posted by Mike Shulman

A few weeks ago at the homotopy type theory electronic seminar I spoke about my joint work with Dan Licata and Mitchell Riley on a “generic” framework for type theories. I briefly mentioned how this fits into a hierarchy of “nn-theories” for n=0,1,2,3n=0,1,2,3, but I didn’t have the time in the talk to develop that idea in detail. However, since that short remark has generated some good discussion and questions at the nnForum, and also the question of “nn-theories” has a substantial history here at the nn-Category Cafe (e.g. this post from 10 years ago), I thought I would expand on it somewhat here.

Let me clarify at the outset, though, that there may be many possible notions of “nn-theory”. This is just one such notion, which gives a convenient way to describe what I see happening in our general framework for type theories. Notable features of this notion of nn-theory include:

  1. It identifies 2-theories with a certain kind of doctrine, for those who know that word. (If that’s not you, don’t worry: I’ll explain it).
  2. It definitively expects the models of an nn-theory to form an nn-category, and not just an nn-groupoid.
  3. It helps clarify the somewhat confusing question of “what is a type theory?”, by pointing out that the phrase “type theory” (and also “internal language”) is actually used in two distinct ways: sometimes it refers to a 1-theory and sometimes to a 2-theory.

Let’s start with a simple example of a theory: the theory of monoids. This is a 1-theory, as you might guess from the fact that monoids form a 1-category. Each individual monoid (like (,+,0)(\mathbb{N},+,0), for instance) is called a model of this theory; thus in general a 1-theory has a 1-category of models. More generally, we can define a monoid object in any category with finite products (say); thus a 1-theory has a 1-category of models internal to any sufficiently structured 1-category.

So far so good, but what exactly is a 1-theory in general? As discussed in this post and its comments, there are several “levels of realization” at which we might consider a theory, but for now I want to focus on the two extreme ends: the fully syntactic and the fully semantic. In a fully syntactic presentation, the theory T MonT_{Mon} of monoids looks like this:

  • One generating type MM.
  • Two generating terms (x:M),(y:M)(m(x,y):M)(x:M), (y:M) \vdash (m(x,y) : M) and (e:M)\vdash (e:M).
  • Three generating equalities (x:M),(y:M),(z:M)(m(m(x,y),z)=m(x,m(y,z)):M)(x:M),(y:M),(z:M) \vdash (m(m(x,y),z) = m(x,m(y,z)) : M) and (x:M)(m(x,e)=x:M)(x:M) \vdash (m(x,e)=x : M) and (x:M)(m(e,x)=x:M)(x:M) \vdash (m(e,x)=x : M).

The fully semantic presentation of the theory of monoids is its Lawvere theory L MonL_{Mon} or walking model: the category with finite products freely generated by a monoid object MM. This has the universal property that for any category CC with finite products, functors L MonCL_{Mon}\to C that preserve finite products are equivalent to monoid objects in CC.

The connection between the syntactic and semantic presentations is the following:

  • The objects of L MonL_{Mon} are the types obtained by starting with the generating type and freely adding finite product types A×BA\times B and the nullary product 11.
  • The morphisms of L MonL_{Mon} are represented by the terms obtained by starting with the generating terms m(x,y)m(x,y) and ee and allowing arbitrary substitutions for variables (i.e. composites of morphisms), such as m(m(x,x),m(y,m(z,y)))m(m(x,x),m(y,m(z,y))).
  • These terms are then quotiented by the congruence generated by the generating equalities of associativity and unitality.

(The intermediate stages of “realization” I referred to are what you get by, e.g., closing up the generating equalities into a congruence but retaining the special status of the generating terms m(x,y)m(x,y) and ee, and similarly for other places of drawing the line. I want to ignore these not just for expositional clarity, but because when you get to dependent type theory it’s no longer clear to me that there is anywhere “in the middle” to draw the line; see here.)

Now we can say more generally what a 1-theory is (at least, one kind of 1-theory). A syntactic 1-theory has a set of generating types, a set of generating terms (which may involve not only the generating types but those obtained from them by applying finite products), and a set of generating equalities (which may involve not only the generating terms but those obtained from them by substitutions). And a semantic 1-theory is just a category with finite products. Every syntactic 1-theory generates a semantic 1-theory, which is “freely generated by a model”. And every semantic 1-theory can be generated by at least one syntactic 1-theory, such as the “tautological” one whose generating types are all the objects, whose generating terms are all the morphisms, and whose generating axioms are all the equalities. (I’m not being precise about any of this, but it can be made precise.)

[A brief digression]: Note that a given semantic 1-theory can have many different syntactic presentations. For instance, the semantic 1-theory of monoids can be presented either as above in “biased” form with one binary and one nullary operation, or in an “unbiased” form with one nn-ary operation for all nn (and also in many other ways). Nevertheless, the relationship between syntax and semantics is often formulated as an equivalence of categories. Personally, I’m not as fond of such formulations, because in order to make them true one has essentially to define “morphisms of syntactic theories” just so as to make such an equivalence hold, rather than in the “natural” way consisting of functions between the generating types, generating terms, and generating axioms. It’s certainly important that the biased notion of monoid agrees with the unbiased version, but I think it’s also important that the two notions are different in some sense, and to me the natural way to express this is to say that they are two different syntactic theories that generate the same semantic theory. [End of digression]

Now, so far, all of this is only about “finite-product 1-theories”: the syntactic types are generated only by the finite-product constructors A×BA\times B and 11, the semantic theories are categories with finite products, and the internal models likewise happen in categories with finite products. The notion such as “category with finite products” that we fix in order to give rise to this whole structure is sometimes called its doctrine.

We can then consider other doctrines, such as “monoidal categories”. In this doctrine, the internal models happen in monoidal categories, the semantic theories are monoidal categories, and the syntactic types are generated by tensor product constructors ABA\otimes B and II. In a much more highly structured doctrine like “locally cartesian closed categories” or “toposes”, the semantic theories are such categories, and the syntactic types are generated by higher-order constructors such as dependent products, power-types, universes, and so on. Each choice of doctrine determines a notion of “syntactic 1-theory in that doctrine”, a notion of “semantic 1-theory in that doctrine”, and the above sort of relation between them.

But, how do we define a “doctrine” in general? We have lots of examples, but without a general structure for them we have to develop the general theory for each such doctrine separately. This is clearly an undesirable state of affairs.

Along the way to answering this question, note first that the semantic 1-theories in any doctrine form a 2-category — for instance, the 2-category of categories with finite products, or the 2-category of monoidal categories, or the 2-category of toposes. Thus, it is natural to guess that a doctrine will be a sort of “2-theory” which has a 2-category of “models”, and that these models coincide with semantic 1-theories in that doctrine/2-theory. We might even leap to a general principle such as:

The models of an (n+1)(n+1)-theory are the semantic nn-theories in that (n+1)(n+1)-theory (regarded as an “nn-doctrine”, i.e. a language in which to write nn-theories).

To see whether this makes sense, let’s do a bit of negative thinking. In what sense can we consider the models of a 1-theory as “semantic 0-theories”? In particular, what is a syntactic 0-theory?

Well, note that a syntactic 1-theory can be regarded as a kind of presentation of a semantic 1-theory: we specify the generating objects, generating morphisms, and relations that they have to satisfy. So a syntactic 0-theory should be a suitable kind of presentation of a semantic 0-theory, i.e. of a model.

For instance, in the 1-theory (= 0-doctrine) of monoids, a syntactic 0-theory is a monoid presentation: a set of generating elements together with relations between formal products of generators. Every monoid presentation (G,R)(G, R) presents a monoid L G,RL_{G,R} in the usual way, i.e. every syntactic 0-theory gives rise to a semantic 0-theory. Moreover, this presented monoid has a universal property: monoid homomorphisms L G,RML_{G,R} \to M, for any monoid MM, are equivalent to “internal models” of (G,R)(G,R) in MM, i.e. interpretations of each generator xGx\in G as an element of MM such that the relations in RR hold in MM.

Note that although we are speaking of internal models of a syntactic 0-theory in an arbitrary semantic 0-theory (in the same 0-doctrine = 1-theory), these semantic 0-theories are not themselves arbitrary internal models of the 1-theory in question, but specifically models in the “canonical” 1-category SetSet. Thus our principle above should really be refined a bit to

The models of an (n+1)(n+1)-theory in the (n+1)(n+1)-category nCatn Cat are the semantic nn-theories in that (n+1)(n+1)-theory.

How low can we go? Well, the canonical 0-category is (1)Cat(-1)Cat, i.e. the (po)set Ω\Omega of truth values. This is, indeed, a monoid under the operation “and” (the decategorification of the cartesian product in SetSet). Thus, given a 0-theory MM (a monoid), the semantic (1)(-1)-theories in MM (regarded as a (1)(-1)-doctrine) are the models of MM in (1)Cat(-1)Cat, i.e. the monoid homomorphisms MΩM\to \Omega.

Since Ω\Omega is the subobject classifier (in SetSet), a function MΩM\to \Omega is the same as a subset of MM. And asking that such a function is a monoid homomorphism says precisely that this subset is a submonoid, i.e. contains the identity element eMe\in M and is closed under the multiplication. Thus, the semantic (1)(-1) theories in the 0-theory MM are the submonoids of MM; a statement which, if not obviously correct, is at least not obviously incorrect.

(As usual, the ladder bottoms out here: the “canonical” (1)(-1)-category is (2)Cat(-2)Cat, namely the truth value “true”, which is the terminal object; thus there are no nontrivial (2)(-2)-theories.)

Since negative thinking seems to justify our principle, let’s go back to climbing upwards: what is a 2-theory? We should expect to have both syntactic and semantic 2-theories. A semantic 2-theory will be, in particular, a 2-category, just as a semantic 1-theory (e.g. a Lawvere theory) is, in particular a 1-category. But it will be a structured 2-category, and a syntactic 2-theory will be a way of “presenting” such a structured 2-category in terms of generating objects, morphisms, 2-morphisms, and relations.

What kind of 2-categorical structure will semantic 2-theories have? Well, that depends on the 3-theory in which they live. (-: (-: (-:

The simplest thing to do would be to categorify our running example. In this case, the 3-theory would have as its models (in 2Cat2 Cat) 2-categories with finite products. These are then the semantic 2-theories in this 3-theory (= 2-doctrine). And a syntactic 2-theory in this 3-theory is a presentation of a particular such 2-category.

Below we’ll mention some other possible 3-theories, but first I want to talk some more about syntax. So far, this discussion has been mainly semantic, with comments about the syntax limited to the vague term “presentation”. But we can be more explicit about what the syntax looks like, especially when we consider varying two adjacent levels simultaneously, such as n=1n=1 and n=2n=2.

A particular 2-theory specifies the “doctrine” in which we write 1-theories, which syntactically means the rules of the deductive system in which we formulate those 1-theories. For instance, the 2-theory of “categories with finite products” specifies rules like

AtypeBtypeA×Btype \frac{A \; type \qquad B \;type}{A\times B \; type}

saying that we can form cartesian product types, together with their usual introduction/elimination/computation rules, for instance the pairing rule

Γa:AΓb:BΓ(a,b):A×B \frac{\Gamma\vdash a:A \qquad \Gamma \vdash b:B}{\Gamma\vdash (a,b) :A\times B}

A particular 1-theory in this doctrine, on the other hand, specifies generating types, terms, and axioms without varying the rules. The theory of monoids, the theory of groups, the theory of rings, the theory of a module over a ring, and so on — all of these can be specified by generating types, terms, and axioms without varying the rules about finite product types.

A different 2-theory specifies a different doctrine, with corresponding different rules. For instance, the 2-theory of “symmetric monoidal categories” specifies rules like

AtypeBtypeABtype \frac{A \; type \qquad B \;type}{A\otimes B \; type}

for tensor product types, together with different introduction/elimination/computation rules, such as a “linear” pairing rule

Γa:AΔb:BΓ,Δ(a,b):AB \frac{\Gamma\vdash a:A \qquad \Delta \vdash b:B}{\Gamma,\Delta\vdash (a,b) :A\otimes B}

This corresponds to tensoring together two morphisms with different domains and codomains (the comma in “Γ,Δ\Gamma,\Delta” is a “judgmental” version of the tensor product \otimes), in contrast to how the pairing rule of cartesian products uses the universal property for a pair of morphisms with the same domain.

We can then formulate particular 1-theories in this doctrine, such as the theories of monoids, comonoids, bimonoids, Hopf algebras, etc. — but not the theories of groups or rings, since these require duplication of variables. (Note that the “same” theory of monoids can be formulated in both doctrines. Indeed, the theory of monoids in the doctrine of finite products is “freely extended” from the theory of monoids in the doctrine of monoidal categories. This sort of “change of doctrine” is another interesting direction to think about, but tangential to the point for now.)

Now I think we can see the last point I mentioned before the fold about the ambiguity in the noun phrase “type theory”. Sometimes when people say “theory” they mean something like the theory of monoids, i.e. a 1-theory consisting (syntactically) of generating types, terms, and axioms. For instance, when people say things like “the 2-category of Martin-Löf type theories is equivalent to the 2-category of locally cartesian closed categories”, they mean “type 1-theories”. But other times when people say “type theory” they are referring to a 2-theory, consisting (syntactically) of rules: for instance, the phrase “Martin-Löf type theory” (singular) has this meaning.

Similarly, the phrase “internal language” sometimes refers to the “tautological” syntactic 1-theory associated to a semantic 1-theory, e.g. “the internal language of the category of reflexive graphs” is a particular 1-theory with one generating type for each reflexive graph, etc.. But other times the phrase “internal language” is used to indicate a particular syntax/semantics adjunction, e.g. “extensional Martin-Lof type (2-)theory is an internal language for locally cartesian closed categories”.

So far so good… but unfortunately the world of syntax is not so simple. Even once we’ve fixed a particular doctrine, there can be many different ways to write down rules in which to formulate syntactic theories. In other words, it’s not really quite right to say that an (n+1)(n+1)-theory specifies the rules for a deductive system for nn-theories; it’s more correct to say that it specifies the intended categorical structure that such rules should represent. (A syntactic (n+1)(n+1)-theory gives a bit more information than a semantic one here, but still not enough.)

My favorite simple example of this is 0-theories in the 1-theory of monoids (so n=0n=0). The 1-theory of monoids specifies the intended structure on a set that a “deductive system for monoids” should represent — namely, a monoid structure. What is a “deductive system for monoids”? Roughly speaking, it’s a method of starting from a monoid presentation (G,R)(G,R) and generating the entire monoid. We have to first produce a collection of “words” from the generating elements gg, and then quotient them by the specified relations RR as well as the monoid axioms. But what is a “word”? There are many possible answers; here are a few:

  1. A word is a finite list of generating elements, like abcda b c d.
  2. A word is a finite list of generating elements bracketed in binary and nullary groups, such as (ab)((()c)d)(a b)((()c)d).
  3. A word is a finite list of generating elements bracketed in groups of arbitrary arity, such as (abc)()(d)(a b c)()(d).

Answer #1 is, of course, the simplest, and the one we normally use. But answer #3 is all we can produce “naturally” if we start from the semantic 1-theory of monoids, which has exactly one operation of each arity. If we start instead from the “biased” syntactic 1-theory of monoids, which has one binary and one nullary generating term, we can obtain answer #2. Answer #1 involves some deeper analysis of the notion of monoid, since it already incorporates the associativity axiom rather than imposing it afterwards as part of the quotienting. (The proof that answer #1 actually works is, essentially, a form of “cut-elimination”.) Note also that the choice of “notion of word” actually already has to be made before we specify the entire presentation (G,R)(G,R), since each relation in RR has to relate a pair of words.

Similarly up a level, once we fix a 2-theory, there are many different deductive systems that can present 1-theories in that doctrine. For instance, cartesian closed categories can be presented using lambda-calculus, but also combinatory logic. Monoidal categories can be presented as I described above using “intuitionistic linear type theory”, but also a “combinatory” version as in the rosetta stone paper, and even string diagram calculus can be regarded as a way to present monoidal categories.

Any such deductive system has advantages and disadvantages. However, for the purposes of computation — and also, arguably, for the purposes of informal usage as a foundation for mathematics, although that’s a discussion I don’t have space for right now — it’s important to look for a particular collection of advantages, notably the “admissibility” of operations such as cut and substitution, and computational properties such as normalization and canonicity. These sorts of metatheorems are what type theorists spend a lot of their time proving — about each doctrine separately.

Now I can finally describe the programme that Dan, Mitchell, and I are undertaking. Given a particular 3-theory, we aim to describe a particular deductive system for syntactic 2-theories in that 3-theory, and associate to any such syntactic 2-theory DD a specific deductive system for syntactic 1-theories in DD, such that the latter (1) indeed has the correct semantics, i.e. it presents the correct semantic 1-theories, and (2) has the good meta-theoretic properties that type theorists want, such as cut-elimination, normalization, and canonicity. For a particular syntactic 1-theory, the deductive system that we get is not usually identical to any existing deductive system for that 1-theory, but it is almost always related to it by a fairly direct translation (in general, rules of the existing system tend to translate into the successive applications of two or more “more basic” rules in our system).

To the extent that it succeeds, this has the potential to simplify our lives considerably: instead of treating each 2-theory separately, we can obtain them all automatically from a general theorem. Or, rather, from a small collection of general theorems, because (for the present, and also the foreseeable immediate future) we are treating each 3-theory separately.

  • The first paper by Dan and myself dealt with the 3-theory of (totally unstructured) 2-categories. Syntactically, this corresponds to “unary type (2-)theories” with judgments such as x:Ab:Bx:A \vdash b:B with exactly one type to both the left and the right of the turnstile.
  • The second paper, with Dan and Mitchell, dealt with the 3-theory of cartesian monoidal 2-categories (actually, for technical reasons we used cartesian 2-multicategories). Syntactically, this corresponds to “simple type (2-)theories” with judgments such as x:A,y:B,z:Cd:Dx:A, y:B, z:C \vdash d:D with a finite list of types to the left but exactly one type to the right, and no dependent types.
  • At the end of my HoTTEST talk, I reported on our current progress towards a 3-theory that corresponds syntactically to “dependent type (2-)theories”. The semantic version of this seems to be some kind of “comprehension 2-category”.

These three 3-theories are “cumulative”, i.e. any 2-theory in one of the first two can also be formulated in the more expressive ones below it, in the same way that the theory of monoids in the doctrine of monoidal categories can also be formulated in the more expressive doctrine of categories with finite products. So once our current work on dependent type 2-theories is complete, it will (to a certain extent) subsume the previous two papers. However, there are also other 3-theories that remain to be studied. Some, such as the 3-theory of first-order logic, live in between the 3-theories of simple type 2-theory and dependent type 2-theory. But another notable one is:

  • There should be a 3-theory that corresponds syntactically to “classical simple type (2-)theories” with judgments such as A,B,CD,EA,B,C \vdash D,E that allow finite lists of types on both sides of the turnstile. For instance, the 2-theory of *\ast-autonomous categories (classical linear logic), and also of Boolean algebras (classical nonlinear logic), live in this 3-theory.

We have some ideas about this latter 3-theory, but it’s still rather up in the air. It should subsume the 3-theory of simple type 2-theories, but is incomparable with the 3-theory of dependent type 2-theories (neither subsumes the other), and it’s unclear to me whether there is any 3-theory that subsumes both of them.

Since this is the nn-Category Café, someone is going to ask the question “what about 4-theories?” or even “what about \infty-theories?”, so let me go ahead and answer it preemptively.

In principle, the sort of “interaction between adjacent levels” that we’re interested in — using a 2-theories in a particular 3-theory to describe a deductive system for syntactic 1-theories in such 2-theories — could be generalized to any adjacent levels. For instance, we could imagine using 7-theories in a particular 8-theory to describe a deductive system for syntactic 6-theories in such 7-theories. However, in practice, when dimensions get beyond 2 or 3, human beings seem to do better with some sort of “encoding” of the higher-dimensional structure in terms of lower-dimensional structure.

Homotopy type theory is a good example: despite being ostensibly a theory of (,1)(\infty,1)-categories, as a type theory it is actually just a 2-theory, or a deductive system for a certain class of 1-theories. Syntactically, this is roughly because it doesn’t include any basic 2-cell judgments; its 2-cells and higher cells are all encoded implicitly using 1-morphisms into path objects. Semantically, this corresponds to the fact that its most “direct” notion of model is actually a kind of structured 1-category (a comprehension category, category with families, etc.); a coherence theorem then (hopefully) relates these to the intended (,1)(\infty,1)-categorical models.

So, while in principle one could go on to talk about 4-theories, nn-theories, and \infty-theories, it’s not clear to me that anyone will.

To conclude, let me say a bit about how this project relates to modal logic. In a syntactic 2-theory with multiple generating types, the objects of the resulting semantic 2-category are not single structured categories, but diagrams of several categories with functors and natural transformations between them. Thus, the corresponding syntactic 1-theories have several “classes” of types, one for each category. These classes of types are generally called “modes”, type theory or logic with multiple modes is called “modal”, and the functors between these categories are called “modalities”. Thus, modal logics are particular 2-theories, to which our framework applies.

Traditional modal logic involves “logical” modalities such as \Box (“it is necessary that…”) and \lozenge (“it is possible that…”). More recently, in cohesive type theory (first here) we have introduced modalities denoted ʃ,,ʃ,\flat,\sharp that correspond to the monads and comonads on a cohesive topos. Other applications have also appeared or are in the works, such as this paper on internal universes, a type theory for parametrized spectra involving a self-adjoint modality \natural, and a type theory for “differential cohesion” involving six modalities ʃ,,,,,&ʃ,\flat,\sharp,\Re,\Im,\&. I fully expect that in the future such modal type theories will proliferate, so having a general framework to produce them will be very useful.

Posted at April 26, 2018 9:50 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3034

40 Comments & 0 Trackbacks

Re: What is an n-theory?

This is great to see such work coming to fruition, Mike. To think it was around 14 years ago that John Baez was telling me about his idea of modal logic as a form of categorified logic. The only glimpse I can see of some ideas we were knocking about back then is in this comment. The idea of a dependency through two indexing layers was there, as is the idea that there is something modal about this.

Anyway, I’m really looking forward to seeing modal type theory get properly worked out. There should be many uses for philosophy.

Posted by: David Corfield on May 2, 2018 3:57 PM | Permalink | Reply to this

Re: What is an n-theory?

I agree, it’s exciting to see vague ideas from long ago start to find precise expression! It would be great to work out how some of the discussion back then corresponds to the picture I presented. But I had a bit of trouble following that old discussion, perhaps partly because it referred to older ones (perhaps some offline) that I didn’t have at hand. Where would be a good place to start?

Posted by: Mike Shulman on May 2, 2018 4:59 PM | Permalink | Reply to this

Re: What is an n-theory?

Well perhaps we didn’t get too far. There’s a snatch of discussion from the ‘2-toposes’ thread here. Then further in the ‘Worrying about 2-logic’ thread, there is John here.

Oh, I see a very neglected nLab page Philosophy has this:

There ought to be a categorified logic, or 2-logic. There are some suggestions that existing work on modal logic is relevant. Blog discussion: I, II, III, IV, V. Mike Shulman’s project: 2-categorical logic.

I think that idea of two layers of dependency was only really discussed verbally.

No doubt Jim Dolan was heavily involved in the initial ideas. I wonder what there is in their ‘doctrines’ work: Doctrines of algebraic geometry and Doctrines.

Posted by: David Corfield on May 3, 2018 10:01 AM | Permalink | Reply to this

Re: What is an n-theory?

Thanks for all those links! Here’s a “number 0” that’s good to start with. I’d forgotten that I was a part of some of those conversations.

(As an aside, I noticed this comment and ensuing discussion, which in hindsight foreshadows the notion of h-level and the Σ/\Sigma/\exists distinction in HoTT.)

A lot of that earlier discussion seems to focus on groupoids rather than categories. Perhaps one reason is the fact mentioned by Todd at the bottom of this post that for a first-order theory TT in classical logic with no function symbols, the category TModT Mod is automatically a groupoid. But generalizing to other doctrines, we shouldn’t expect this to remain true.

Posted by: Mike Shulman on May 3, 2018 7:48 PM | Permalink | Reply to this

Re: What is an n-theory?

One more glimpse of this early work is at the end of my Categorification as a heuristic device. It’s a shame I have nothing better than a garbled Word document. The book it appeared in was certainly not a bestseller.

Posted by: David Corfield on May 28, 2018 10:14 AM | Permalink | Reply to this

Re: What is an n-theory?

For the record, in the discussion on modal types, we had Neel pointing out adjunctions between categories of judgments.

Posted by: David Corfield on June 10, 2018 10:33 AM | Permalink | Reply to this

Re: What is an n-theory?

This is almost the answer to your other question

Can you give us a sense of the form of these ‘serious restrictions’?

Basically our approach is that all type-forming operations are required to be given by adjunctions (of some generalized/dependent/multivariable sort). You can omit some of the adjoints if you want (e.g. to describe monoidal categories that aren’t closed, or modal operators that don’t have adjoints), but the adjoints are always potentially there within the formalism.

Moreover, all the adjunctions are, as Neel says, internalizations of judgmental structure, which in categorical terms means that they have universal properties. For instance, the tensor product internalizes the judgmental comma:

A,BCABC \frac{ A,B \vdash C} {A\otimes B\vdash C}

which categorically means that instead of monoidal categories we talk about representable multicategories. Similarly, a modal operator like \Box or \flat internalizes a category of “valid/crisp judgment”:

x::ACx:AC \frac{ x::A \vdash C} { x:\flat A \vdash C}

which categorically means instead of pseudofunctors we are talking about (bi)fibrations. In fact, you can view our semantic construction as a somewhat idiosyncratic approach to “generalized multicategories” and their representability.

Posted by: Mike Shulman on June 11, 2018 10:46 AM | Permalink | Reply to this

Re: What is an n-theory?

Given your slide 20, could we also think in terms of (categorified) hyperdoctrines?

I guess given a 2-topos with nice behaviour of its fibrational slices, we might have something like that.

Posted by: David Corfield on May 2, 2018 4:50 PM | Permalink | Reply to this

Re: What is an n-theory?

Roughly speaking, I would say that hyperdoctrines (and indexed monoidal categories) are the kind of 1-categorical structures that correspond to 2-theories in the 3-theory of “first-order logic”, which I mentioned briefly as living between the 3-theory of simple type (2-)theories and the 3-theory of dependent type (2-)theories. By the Baez-Dolan microcosm principle (which apparently I forgot to mention in the post!), semantic 2-theories in this 3-theory should be a sort of “2-hyperdoctrine”, by analogy to “cartesian monoidal 2-categories” and “comprehension 2-categories”. Syntactically, this 3-theory has one layer of dependency: there is one layer of types which can’t depend on anything, and then there is a second layer of types (“propositions” in the logical reading) which can depend on types in the first layer, but not on each other.

Posted by: Mike Shulman on May 2, 2018 4:57 PM | Permalink | Reply to this

Re: What is an n-theory?

Cool post! As an outsider to HTT, it took me a long time to realize one of the points that you bring up: HTT is 22 theory which is meant to axiomatize the structure of a particular type of category (roughly the structure that one sees in the subcategory of fibrant objects + fibrations in a model category that “presents an \infty-topos”). In particular, it is not an \infty-theory that axiomatizes the structure of an \infty-topos– which is what the slogan “HTT is the internal language of \infty topoi” suggested to me at first.

It seems that one big tensions in higher category theory is that those of us who are algebraically or computationally oriented prefer syntactic theories like HTT which have relatively simple presentations. And now, even though we have the basic tools to talk about nn-theories, e.g. as nn Segal spaces with finite products, these tools are only semantic.

I guess that the reason for this is that the only presentation that exists uniformly is the “tautological one” you mentioned, and there is no reason for a mathematically interesting theory to have a simple presentation: For instance finding a simple syntactic presentation the (,1)(\infty,1) theory of E 2E_2 algebras is morally equivalent to finding simple CWCW decompositions for the configuration spaces

Posted by: Phil Tosteson on May 2, 2018 4:58 PM | Permalink | Reply to this

Re: What is an n-theory?

Yes, I think I agree. It’s not impossible to write down true \infty-theories, though. For instance, opetopic type theory is arguably a true syntactic (,)(\infty,\infty)-theory.

Cubical type theory is an interesting case. I’m inclined to regard it as still a 2-theory analogous to HoTT, although it does incorporate higher cells somewhat “judgmentally” by using interval variables. This sort of classification may not have a unique answer.

Posted by: Mike Shulman on May 2, 2018 5:07 PM | Permalink | Reply to this

Re: What is an n-theory?

– and finding those decompostitions is hard!

Unrelatedly, is there currently a 33 theory TT which does for \infty categories what HTT does for \infty groupoids? In other words, models of TT are structured 22 categories, one model should be the 22 category of quasi-categories, but which also includes other “\infty cosmoi.”Is this the sort of theory that your work with Emily Riehl is developing?

Posted by: Phil Tosteson on May 2, 2018 4:59 PM | Permalink | Reply to this

Re: What is an n-theory?

No, such a theory doesn’t yet exist. My work with Emily is actually a 2-theory whose models include the 1-category of Reedy fibrant bisimplicial sets, inside which one can describe the Segal types and Rezk types which form a model for (,1)(\infty,1)-categories.

Posted by: Mike Shulman on May 3, 2018 6:22 PM | Permalink | Reply to this

Re: What is an n-theory?

I was just wondering whether you have reflected upon taking say the 1-theory of monoids that you described, and replacing judgemental equality by intensional equality? Does this change the level of the theory?

Posted by: Richard Williamson on May 3, 2018 10:22 AM | Permalink | Reply to this

Re: What is an n-theory?

The 1-theory of monoids that I described lives in the 2-theory of cartesian monoidal categories, wherein there is no notion of “intensional equality”. You can also formulate a 1-theory of monoids inside the 2-theory of intensional type theory; the result is still a 1-theory although it lives in a different 2-theory.

Posted by: Mike Shulman on May 3, 2018 6:15 PM | Permalink | Reply to this

Re: What is an n-theory?

Yes, I meant that one replaces (x:M)(m(x,e)=x:M)(x:M) \vdash (m(x,e)=x:M) by (x:M)w x,e:Id M(m(x,e),x)(x:M) \vdash w_{x,e} : Id_{M}(m(x,e), x), and so on, in some 2-theory (?) in which one has identity types.

What prompted my question was that you wrote

A syntactic 1-theory has a set of generating types, a set of generating terms (which may involve not only the generating types but those obtained from them by applying finite products), and a set of generating equalities (which may involve not only the generating terms but those obtained from them by substitutions).

and wrote that in a 1-theory one formulates axioms

without varying the rules

whereas the intensional re-formulation of the axioms of a monoid are, to me, rules rather than axioms.

Perhaps you simply meant to restrict your statement to rules involving type constructors, introduction, elimination, and computation?

Posted by: Richard Williamson on May 3, 2018 6:49 PM | Permalink | Reply to this

Re: What is an n-theory?

I don’t know what you mean; your (x:M)w x,e:Id M(m(x,e),x)(x:M) \vdash w_{x,e} : Id_M(m(x,e),x) is a generating term, not a rule.

Posted by: Mike Shulman on May 3, 2018 7:01 PM | Permalink | Reply to this

Re: What is an n-theory?

What do you consider to be a rule? What if we write it as follows?

x:Mw x,e:Id M(m(x,e),x)\frac{\vdash x \colon M}{\vdash w_{x,e} : Id_{M}(m(x,e), x)}

What I mean by a rule is something that given a term in context, prescribes that we can form another term in some other context, and I distinguish this from an axiom by the fact that we are not asserting (judgemental) equality of anything.

Posted by: Richard Williamson on May 3, 2018 7:36 PM | Permalink | Reply to this

Re: What is an n-theory?

What I mean by a rule is something that given some judgments (the premises) prescribes that we can form some other judgment (the conclusion). Terms-in-context are particular judgments, as are judgmental-equality judgments.

One way to say what I mean by a “generating thingy” or “axiom” is a rule without premises. So generators/axioms can be regarded as rules (and, as such, can be frobnicated into other equivalent (modulo admissibility of substitution) forms that do have premises, such as yours), but not every rule can be regarded as a generator/axiom. From this perspective, “formulating axioms without varying the rules” means “adding only rules without premises”.

It’s helpful to distinguish axioms from (more general) rules; in particular, it’s the only way to distinguish the theory from the doctrine. However, the fact that axioms can be regarded as a degenerate case of rules is also important, and means you can always “build a theory into a doctrine”. In other words, instead of considering the 1-theory T Mon 1T^1_Mon of monoids inside the 2-theory T FP 2T^2_FP of categories with finite products, you could consider the 2-theory “Lift(T Mon 1)Lift(T^1_Mon)” of “categories with finite products containing a monoid object”. That is, the models of Lift(T Mon 1)Lift(T^1_Mon) are the models of T FP 2T^2_FP containing a model of T Mon 1T^1_Mon.

There is another interesting general fact here, namely that the monoid of global sections of the generic T Mon 1T^1_Mon-model internal to the initial Lift(T Mon 1)Lift(T^1_Mon)-algebra actually coincides with the initial T Mon 1T^1_Mon-model in SetSet. Which means that if you had a nice enough syntactic presentation for 2-theories, it could also function as your syntactic presentation of 1-theories by simply incorporating them into the 2-theory in this way. Dan, Mitchell, and I have considered going this route, but so far it’s been difficult to formulate a presentation of 2-theories for which this would approach the niceness of our presentations of 1-theories given a fixed 2-theory (and there are other issues too).

Posted by: Mike Shulman on May 3, 2018 8:02 PM | Permalink | Reply to this

Re: What is an n-theory?

Nice, thanks for the elaboration!

Which means that if you had a nice enough syntactic presentation for 2-theories, it could also function as your syntactic presentation of 1-theories by simply incorporating them into the 2-theory in this way.

That makes sense, and is a nice observation I think. By coincidence I have been contemplating, on the semantic side, a somewhat similar situation recently.

Posted by: Richard Williamson on May 4, 2018 12:49 AM | Permalink | Reply to this

Re: What is an n-theory?

That part about semantic (1)(-1)-theories of the 00-theory of a monoid being submonoids put me in mind of when you have a theory in propositional logic given by some atomic sentences and axioms. This gives rise to a Boolean algebra, where models of the theory are given by Boolean algebra morphisms to 2\mathbf{2}.

So say we have PP, QQ, RR, and one axiom PQRP \wedge Q \to R, then models pick out certain subsets of the set of atomic states satisfying the axiom.

So what kind of nn-theory is propositional logic? Since models are Boolean algebras, which form a category, does this make it a syntactic 1-theory? Then a specific presentation of a propositional theory is a 0-theory whose models form the set of semantic (-1) theories.

But isn’t that surprising that first-order logic is a 3-theory, two levels higher?

Posted by: David Corfield on May 3, 2018 12:08 PM | Permalink | Reply to this

Re: What is an n-theory?

There is indeed a 1-theory whose 1-category of models is the category of Boolean algebras, and such that a 0-theory in that 1-theory is a presentation of a specific Boolean algebra.

However, a single Boolean algebra is also a category in its own right, and so the collection of Boolean algebras is a 2-category (which happens to be a (1,2)-category). Thus there is also a 2-theory whose 2-category of models is the 2-category of Boolean algebras, and such that a 1-theory in that 2-theory is a presentation of a specific Boolean algebra.

The latter presentation corresponds better to what we think of as propositional logic. The 2-theory of Boolean algebras naturally lives in the 3-theory of “classical 2-theories” (mentioned briefly in the post as not yet having been studied), and as such can be presented with good type-theoretic properties such as cut-elimination.

Posted by: Mike Shulman on May 3, 2018 6:10 PM | Permalink | Reply to this

Re: What is an n-theory?

Also, I meant by “first-order logic is a 3-theory” is that there’s a 3-theory for 2-theories with the “dependency shape” of first-order logic. A specific such 2-theory, like the ordinary first-order classical logic that one learns in a first course on mathematical logic, is itself (like propositional logic) a 2-theory. Its models are some kind of hyperdoctrine. Other 2-theories in that same 3-theory are first-order intuitionistic logic, first-order linear logic, the type theory of indexed monoidal categories, first-order modal logic, etc.

Posted by: Mike Shulman on May 3, 2018 6:12 PM | Permalink | Reply to this

Re: What is an n-theory?

As you say “change of doctrine” is tangential to this post, but I wonder if we could have a brief glimpse of how things may go.

I imagine that when mapping from one nn-theory to another, you do so ‘within’ the n+1n+1-theory to which they both belong. So we might inject Th Mon 1Th^1_{Mon} into Th Grp 1Th^1_{Grp} within T FP 2T^2_{FP}.

On the syntactic side, presumably we should heed your warning about “morphisms of syntactic theories” as to how we should rely on

the “natural” way consisting of functions between the generating types, generating terms, and generating axioms.

Perhaps this gives rise to some Morita-equivalence issues.

You’ve already mentioned a map of 2-theories

the theory of monoids in the doctrine of finite products is “freely extended” from the theory of monoids in the doctrine of monoidal categories

So what happens generally with a syntactic morphism (within a 3-theory) between syntactic 2-theories? Such a morphism should act on all the 1-theories written in the domain 2-theory, right?

At some point we should make contact with the concept of a doctrinal adjunction which is taking ‘doctrine’ in the sense of 2-monad. (But note the warning that 2-monads aren’t the correct way to go for doctrines.) So that’s about lifting adjunctions of semantic 1-theories from one 2-theory to another?

Finally, we would have syntactic morphisms between 3-theories. You’ve already given us some idea of relations between five of these: unary, simple, first-order, dependent, classical simple. (Is that the best name for the latter?) So morphisms here bring about transformations of lower level theories.

Posted by: David Corfield on May 4, 2018 8:49 AM | Permalink | Reply to this

Re: What is an n-theory?

Comments are a great place for discussing tangential things! I haven’t thought about change-of-doctrine very deeply in this context, but I can shoot from the hip.

I imagine that when mapping from one nn-theory to another, you do so ‘within’ the n+1n+1-theory to which they both belong.

Yes, that’s definitely the most direct version. I could imagine some kind of “dependent mapping” that first extends an nn-theory along a map of (n+1)(n+1)-theories and then maps it into an nn-theory in a different (n+1)(n+1)-theory, but that decomposes into two same-theory mappings at different levels.

So what happens generally with a syntactic morphism (within a 3-theory) between syntactic 2-theories? Such a morphism should act on all the 1-theories written in the domain 2-theory, right?

Yes, I think so. For instance, the morphism from the 2-theory of monoidal categories to the 2-theory of cartesian monoidal categories is of the simplest sort that just “adds structure”, namely diagonals and projections, which syntactically corresponds to the structural rules of contraction and weakening. So any syntactic 1-theory in the doctrine of monoidal categories can almost without modification be interpreted in the doctrine of cartesian monoidal categories, simply be neglecting to make any use of these rules.

In general, a theory morphism doesn’t have to be injective. For instance, there is a 2-theory morphism from cohesive type 2-theory to ordinary type 2-theory that collapses the separate crisp and cohesive contexts into the one ordinary context. Thus, any 1-theory in cohesive type 2-theory can be interpreted as a 1-theory in ordinary type 2-theory by simply forgetting all the crispness annotations.

It’s an interesting fact (which has, of course, been noted by many people) that on the side of syntax, the “natural” action of doctrine morphisms is “covariant” in this sense, while on the side of semantics, the “natural” action is contravariant: any cartesian monoidal category is in particular a monoidal category, and any topos can be equipped with the identity cohesive structure over itself. In the semantic world, the covariant action is more complicated: you have to “build the free cartesian monoidal category on a monoidal one” by freely adding diagonals and projections. Similarly, in the syntactic world, the contravariant action is more complicated: you have to express a theory that uses contraction and weakening in a language that lacks them by “putting them in by hand” as generators. These two actions are presumably related in some way “over” the adjunction between syntax and semantics, which ought to be obvious but is too much for my brain on a Friday afternoon at the end of the semester.

Finally, we would have syntactic morphisms between 3-theories.

Right. When I talked about “cumulativity” of 3-theories “subsuming each other” in the post, I must formally have meant to refer to morphisms of 3-theories, allowing us to naturally extend 2-theories “up the ladder”.

Posted by: Mike Shulman on May 4, 2018 11:43 PM | Permalink | Reply to this

Re: What is an n-theory?

We could do with a clever notational device to specify trails of nn-theories. There you are giving a monoid presentation and we might want to know which 1-, 2- and 3-theory you’re working in.

What of the conversation we were having with Urs about what happens when we take a subcategory of a semantic nn-theory. As you pointed out, we may not be able to provide a corresponding syntactic nn-theory, at least not in the same n+1n+1-theory.

I wonder if there will be reasonably general things to say about when such a move is possible in the same n+1n+1-theory? Or when a shift depending on some morphism of n+1n+1 theories is possible. There could also be two step decompositions, as you mention.

Posted by: David Corfield on May 5, 2018 10:07 AM | Permalink | Reply to this

Re: What is an n-theory?

Well, one way of specifying a subcategory of a given semantic nn-theory is by adding axioms to its corresponding syntactic nn-theory. The objects of the subcategory will then be the models that satisfy the additional axioms.

Posted by: Mike Shulman on May 8, 2018 11:34 PM | Permalink | Reply to this

Re: What is an n-theory?

Could we add higher-order logic as a sixth 3-theory?

Then where would that sit? I see Bart Jacobs speaks of Translating dependent type theory into higher order logic. Perhaps this concerns specific 2-theories in their respective 3-theories, or is it possible to see the translation as resulting from a morphism of 3-theories?

Posted by: David Corfield on May 23, 2018 9:34 AM | Permalink | Reply to this

Re: What is an n-theory?

Higher-order logic is a funny beast from a doctrinal perspective. I’m not positive, but I think it can actually be expressed as (a class of) 2-theories within the 3-theory that I’m calling first order logic: just add rules specifying an a-la-Tarski universe Ω\Omega of propositions.

I think of a 3-theory as specifying the arity and dependency structure. The 3-theory of “first order logic” has a base whose arity is many-to-one with no internal dependency and then another layer that depends on that. (The upper layer could be many-to-one or many-to-many, so actually there are two different 3-theories for first-order logic, just as there are two different 3-theories for propositional logic / simple type theory. The many-to-one and many-to-many versions are traditionally called “intuitionistic” and “classical”, though that’s confusing too.) Higher-order logic has this same arity and dependency structure; it just happens to have a universe as well. (So maybe “first order logic” is a bad name for this 3-theory…)

Posted by: Mike Shulman on May 24, 2018 2:28 PM | Permalink | Reply to this

Re: What Is an n-Theory?

I seem to be full of questions about this work.

I wonder what we can make of our efforts to give a type theoretic account of necessity and possibility. As you know this concerns the use of a type of worlds, WW, in an (,1)(\infinity, 1)-topos, H\mathbf{H}, and the adjoint triple between the slice H/W\mathbf{H}/W and H\mathbf{H}, by pullback and right and left adjoints. Here we can talk about these two (,1)(\infinity, 1)-toposes via a modal dependent type theory.

So I guess these, and other triples generated by an H\mathbf{H}-morphism f:WVf: W \to V, are all models of a simple modal 2-theory, where the 2-category of modes, \mathcal{M}, contains an adjunction (slide 20). It could be a ‘walking’ such 2-category. Then these slices would provide a ready collection of models.

Working backwards, one might discover possible worlds semantics. I want an adjunction between a ‘necessity’ comonad and a ‘possibility’ monad, so I’m looking for models of a modal type theory for a 2-category of modes with a monad. One place to find them is between slices of (,1)(\infinity, 1)-toposes. What to make of the slicing objects? Well objects are varying over them, let’s call them ‘worlds’.

But perhaps the semantic theory comprised of pairs of slices of (,1)(\infty, 1)-toposes can be characterised syntactically.

Posted by: David Corfield on May 5, 2018 10:38 AM | Permalink | Reply to this

Re: What Is an n-Theory?

Continuing on the modal theme, you list some modalities, including those for “differential cohesion”, and then write

I fully expect that in the future such modal type theories will proliferate.

Of course, there’s quite a story as to why differential cohesion with the addition of the fermionic-bosonic modalities is special, how it all arises by a process of Aubhebung from the opposition between the \emptyset comonad and the monad 1\mathbf{1}, etc.

Can all of these requirements be expressed in the 2-category of modes?

Posted by: David Corfield on May 5, 2018 12:10 PM | Permalink | Reply to this

Re: What Is an n-Theory?

Yes, there is a 2-theory generated by an adjunction, which in the semantics becomes an adjoint triple if we have both p *p^\ast and p *p_\ast for each mode morphism. In this case, the left adjoint is not left exact, so we have to be careful with dependency and contexts, but there’ll be some kind of type theory for sure. Since the adjunction isn’t idempotent, the general framework will produce a type theory with infinitely many “context zones”, but you could try to simplify it in this case.

perhaps the semantic theory comprised of pairs of slices of (,1)(\infty, 1)-toposes can be characterised syntactically.

Interesting question; I don’t know a syntactic characterization of etale geometric morphisms.

I don’t really speak Aufhebung, so all I can say to your last question is maybe.

Posted by: Mike Shulman on May 8, 2018 11:41 PM | Permalink | Reply to this

Re: What Is an n-Theory?

I guess one could match a type theory with a different modal counterpart, e.g., dependent type theory with adjoint modalities, the later expressed in a unary type 2-theory of modes. But is the idea that its natural modal counterpart is a full dependent type 2-theory, as suggested by talk of the microcosm principle?

Have you given anywhere examples of constructions we might want to make which use the full resources of dependent type 2-theory?

Avoiding the off-putting Hegelianese, the question is whether some modal dependent type theory is expressive enough to specify 11 modalities, starting out from something like an adjoint comonad-monad 1\emptyset \dashv \mathbf{1}. Then we need a minimal pair \flat \dashv \sharp, such that \sharp \emptyset \simeq \emptyset, and such that \flat has a further left adjoint monad. This monad, call it shape, is such that the shape of a point is a point, and we may require a points-to-pieces transform. And so on, with all the demands up to the solid modalities.

Posted by: David Corfield on May 9, 2018 10:19 AM | Permalink | Reply to this

Re: What Is an n-Theory?

I guess one could match a type theory with a different modal counterpart.

I’m not sure what that would mean. The way our syntactic type theory has type judgments parametrized by mode judgments, the mode theory has to have the same context structure as the type theory. So with a unary mode 2-theory, it wouldn’t make sense to have a simple or dependent type theory over it.

the question is whether some modal dependent type theory is expressive enough to specify 11 modalities

We can certainly express any number of modalities, be it 6, 11, or 40 billion, and any algebraic relations between them like ʃ\flat \to ʃ or &\flat \subseteq \&. But not a property like minimality.

Posted by: Mike Shulman on May 9, 2018 5:25 PM | Permalink | Reply to this

Re: What Is an n-Theory?

It strikes me that it may be worth saying a bit about how our setup is related to logical frameworks.

Roughly, the idea of a logical framework is that by formulating an object theory in a weak enough metatheory, it becomes easier to represent or prove metatheorems about the object theory. For instance, by cutting the metatheory down to a dependent type theory with only Π\Pi-types (no inductive types), we can use higher-order abstract syntax to avoid dealing manually with variable binding in the object language.

This sort of logical framework is, by design, extremely general in what sorts of object theories it can represent. Thus, while the logical framework provides a convenient context in which to prove theorems like cut-elimination and normalization, it doesn’t guarantee their truth; you can represent all sorts of ill-behaved theories as well. One way to describe our approach is to impose serious restrictions on the logical framework such that all object languages will satisfy the desired semantic and syntactic metatheorems, which can then be proved once and for all.

The logical framework used by Twelf and its relatives is a dependent type theory; thus it corresponds roughly to our 3-theory of “dependent type theories”. But there could also be “unrestricted” logical frameworks corresponding to other 3-theories. For instance, while I don’t completely understand Isabelle, I believe that its base system “Isabelle/Pure” can roughly be described as an (unrestricted) logical framework for the 3-theory that I called “first-order logic”, with one simple type theory dependent on another simple type theory. Unlike Twelf, Isabelle is designed to be used as a practical proof assistant for working in its object languages (rather than for proving metatheorems about them). The object language that it’s most commonly used for is called Isabelle/HOL, which is I think an implementation of (classical) higher-order logic inside the 3-theory of “first-order logic” exactly as I suggested here.

Posted by: Mike Shulman on May 25, 2018 5:32 PM | Permalink | Reply to this

Re: What Is an n-Theory?

Can you give us a sense of the form of these ‘serious restrictions’?

Posted by: David Corfield on May 27, 2018 8:38 AM | Permalink | Reply to this

Re: What Is an n-Theory?

William Orton, President of Western Union, 1876:

This ‘telephone’ has too many shortcomings to be seriously considered as a means of communication.

Thomas Edison, inventor, 1889:

Fooling around with alternating current (AC) is just a waste of time. Nobody will use it, ever.

Thomas Watson, president of IBM, 1943:

I think there is a world market for maybe five computers.

Mike Shulman, homotopy type theorist, 2018:

So, while in principle one could go on to talk about 4-theories, nn-theories, and \infty-theories, it’s not clear to me that anyone will.

Luckily you were wise enough to be more cautious than some. The mere fact that you said this is going to make some young whippersnappers try to prove you wrong!

Posted by: John Baez on May 27, 2018 1:32 AM | Permalink | Reply to this

Re: What Is an n-Theory?

More power to them! In fact, as I mentioned in another comment, they’ve already gotten started: opetopic type theory could be argued to be a true (,)(\infty,\infty)-theory. (Of course, Eric Finster isn’t really any younger than me, so if he counts as a “young whippersnapper” then so should I.)

Posted by: Mike Shulman on May 27, 2018 4:06 AM | Permalink | Reply to this

Re: What Is an n-Theory?

The hard part is not being young: by now most people are young. The hard part is being a whippersnapper.

For me the fun would not be developing the general formalism, but finding a bunch of really compelling examples of nn-theories for high nn, and using them to think about math in new ways.

Posted by: John Baez on May 28, 2018 6:05 PM | Permalink | Reply to this

Re: What Is an n-Theory?

Note that in order to prove me wrong, I think one will also have to show that it’s better to treat such theories syntactically as “honest” nn-theories, rather than encoding them as lower-dimensional theories the way HoTT encodes (,1)(\infty,1)-theories as 1-theories.

Posted by: Mike Shulman on May 28, 2018 11:10 PM | Permalink | Reply to this

Post a New Comment