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.

November 22, 2017

Internal Languages of Higher Categories II

Posted by Emily Riehl

Guest post by Chris Kapulkin

Two years ago, I wrote a post for the n-Cafe, in which I sketched how to make precise the claim that intensional type theory (and ultimately HoTT) is the internal language of higher category theory. I wrote it in response to a heated discussion on Michael Harris’ blog Mathematics Without Apologies about what (if anything) HoTT is good for, with the goal of making certain arguments mathematically precise, rather than taking a side in the discussion. Back then, I had very little hope that we will be able to carry out the work necessary to prove these conjectures in any foreseeable future, but things have changed and the purpose of this post is to report on the recent progress.

First off, a tl;dr version.

  • Shortly after my post, Mike Shulman posted a paper describing a new class of models of the Univalence Axiom, this time in categories of simplicial presheaves over what he calls EI-categories.
  • Peter Lumsdaine and I figured out how to equip the category of type theories with a left semi-model structure and were able to give a precise statement of the internal language conjectures.
  • Mike Shulman proposed a tentative definition of an elementary \infty-topos, which, conjecturally, gives the higher-categorical counterpart of HoTT.
  • A few weeks ago, Karol Szumiło and I proved a version of the first of the conjectures, relating type theories with Id\mathrm{Id}- and Σ\Sigma-types with finitely cocomplete \infty-categories.
  • And maybe the most surprising of all: Michael Harris and I are organizing a conference together (and you should attend it!).

Mike posted on the HoTT blog about his paper shortly after it appeared, so I will not be summarizing it again, but let me mention that we now know many models of the Univalence Axiom, although there is still way more to be done.

Peter and I tried to answer the question: what is the right notion of a weak equivalence between type theories? You can think of two different answers to this question, depending on the background you came to HoTT with. If you are more logically-minded, you would think of properties such conservativity and bi-interpretatibility, and indeed, these motivate one of our definitions: a weak equivalence of theories is a translation that allows lifting of types up to equivalence and terms up to propositional equality (Def. 3.1 in the linked paper). If on the other hand, you are a homotopy theorist and you know that each (intensional) type theory has a classifying fibration category, then you would expect that a weak equivalence will be a map between theories that induces an equivalence of the underlying fibration categories. Now here is a great thing about HoTT: these two notions coincide (Prop. 3.3)!

So since a category with weak equivalences is just a presentation of an \infty-category (or a homotopy theory), we obtain several \infty-categories of type theories: Th Id,Σ\mathrm{Th}_{\mathrm{Id},\Sigma} of type theories with Id\mathrm{Id}-types and dependent sums, Th Id,Σ,Π\mathrm{Th}_{\mathrm{Id},\Sigma, \Pi} of those that also carry dependent product structure and yet-to-be-defined Th HoTT\mathrm{Th}_{\mathsf{HoTT}}. We next construct functors from these \infty-categories to various \infty-categories of \infty-categories. And thus there are maps Th Id,ΣLex \mathrm{Th}_{\mathrm{Id},\Sigma} \to \mathrm{Lex}_\infty (\infty-categories with finite limits), Th Id,Σ,ΠLCCC \mathrm{Th}_{\mathrm{Id},\Sigma, \Pi} \to \mathrm{LCCC}_\infty (locally cartesian closed \infty-categories), and conjecturally Th HoTTElTop \mathrm{Th}_{\mathsf{HoTT}} \to \mathrm{ElTop}_\infty (elementary \infty-toposes). We conjecture that these functors are \infty-equivalences (see Sec. 3). At that point, neither Th HoTT\mathrm{Th}_{\mathsf{HoTT}} nor ElTop \mathrm{ElTop}_\infty was a well-defined concept, so in this case our conjecture was really only a conjectural conjecture (joke credit: Tom Hales’ talk at Big Proof). (Note to experts: to be independent of the Initiality Conjecture, we formulated everything in the language of contextual categories instead, but one ultimately wants the conjectures to hold for syntactically-presented type theories.)

We then move on to equip both Th Id,Σ\mathrm{Th}_{\mathrm{Id},\Sigma} and Th Id,Σ,Π\mathrm{Th}_{\mathrm{Id},\Sigma, \Pi} with a left semi-model structure. I won’t spell out the details here, but the construction itself feels really natural to me. All classes of maps have explicit description and in fact ended up being exactly our first guesses. And all the nice things that you could ask for hold in our setting. For instance, the cofibrant type theories (which should be thought of as the free ones) end up being precisely the theories that are extensions by types and terms, without any equations.

A few months later, Mike gave a tentative definition of an elementary \infty-topos, thus making our conjectural conjecture less conjectural. Mike blogged about this definition and his post led to some interesting exchanges in the comments, so I encourage you to take a look if you haven’t yet. During the HoTT MRC, Jonas Frey, Tamara von Glehn, Nima Rasekh, Inna Zakharevich worked with this definition, trying to prove analogues of some results from 11-topos theory, including: stability under gluing and redundancy of including existence of finite colimits in the axioms. Their results constitute a basis of the theory of elementary \infty-toposes and I hope they will appear soon.

Once these conjectures were properly formulated, Karol and I decided to attack the first one of them, i.e. the equivalence Th Id,ΣLex \mathrm{Th}_{\mathrm{Id},\Sigma} \simeq \mathrm{Lex}_\infty. One can decompose the functor Th Id,ΣLex \mathrm{Th}_{\mathrm{Id},\Sigma} \simeq \mathrm{Lex}_\infty into a composite:

Th Id,ΣTrbFibCatLex \mathrm{Th}_{\mathrm{Id},\Sigma} \to \mathrm{Trb} \to \mathrm{FibCat} \to \mathrm{Lex}_\infty

where Trb\mathrm{Trb} is the category of tribes (which are models of type theory studied by Joyal) and FibCat\mathrm{FibCat} is the category of fibration categories (in the sense of Brown). Why is it something desirable? First, tribes are very closely related to comprehension categories, a well-studied notion of a model for type theory, and we prove in the paper that the \infty-category of comprehension categories with Id\mathrm{Id}- and Σ\Sigma-types is equivalent to that of tribes. Second, Karol had previously proven that the map FibCatLex \mathrm{FibCat} \to \mathrm{Lex}_\infty is an equivalence. Thus in order to relate comprehension categories and \infty-categories, one needs to show an equivalence between tribes and fibration categories.

And although both of these notions feel really similar, this is not an easy task! Our initial idea was to construct a functor FibCatTrb\mathrm{FibCat} \to \mathrm{Trb} and show that both composites are weakly equivalent to identity functors. There is a canonical way of doing it, namely by taking a fibration category to the tribe of representable \infty-presheaves on it, which can be realized on the 11-categorical level in many ways, but we couldn’t make any of them strictly 11-functorial (or even weakly in any well-defined and useful sense). The second thought was to use Waldhausen’s Approximation Properties (Def. 2.8 + Thm. 2.9 in the linked paper), which is a criterion for equivalence of fibration categories, similar to the criterion for Quillen equivalence in terms of adjoint transposes of weak equivalences. And although our inverse-on-objects construction would be sufficient here, the Approximation Properties require the fibration category structure on the categories Trb\mathrm{Trb} and FibCat\mathrm{FibCat}. The latter had been previously constructed by Karol, but there seem to be fundamental obstacles to the existence of such a structure on the category of tribes. Indeed, tribes are in some sense more rigid than fibration categories and what we would consider a natural candidate for a path object in Trb\mathrm{Trb} did not satisfy the necessary conditions.

So what did we do in the end? We considered semi-simplicially enriched versions of both fibration categories and tribes (Def. 3.1 and 3.2) and showed that they both carry the fibration category structure (which required a slight modification of Karol’s previous results, see Sec. 4). Then, by explicitly constructing inverses, we proved that they are in fact equivalent to their respective unenriched analogues (Prop 3.12). Finally, we verified that the functor from semi-simplicial tribes to semi-simplicial fibration categories satisfies the Approximation Properties, and so the result now follows by 2-out-of-3. Oh, and in order to verify the Approximation Properties for the enriched version, we first check it for the unenriched version, so it’s really easy to get confused. Btw our notion of a semi-simplicial tribe was inspired by Joyal’s theory of simplicial tribes, but we had to modify the enriching category to ensure the equivalence between the enriched and the unenriched setting.

That’s what out there right now. So… what’s next? Last summer, Simon Cho, Cory Knapp, Clive Newstead, and Liang Ze Wong worked on comparing different categories of models of type theory, including contextual categories, categories with attributes, and comprehension categories. Hopefully they will bridge the gap between comprehension categories and contextual categories left by Karol and myself.

One should also try attacking the second conjecture, although it is going to be a much harder task. The main difficulty is that there is no known presentation, via some 11-categories with extra structure, of locally cartesian closed \infty-categories, and so one would need to compare π\pi-tribes (a.k.a. type-theoretic fibration categories) with locally cartesian closed \infty-categories directly. Another thing to look into are new models of the Univalence Axiom following a series of papers by Mike, since we still don’t know too many such models.

Posted at November 22, 2017 2:39 PM UTC

TrackBack URL for this Entry:

15 Comments & 0 Trackbacks

Re: Internal Languages of Higher Categories II

Thanks for this nice summary! It’s exciting that progress is being made here.

Do you believe my series of papers on models for strict univalent universes, of which you mentioned the latest, are going to be useful in the sort of approach to the problem that you, Peter, and Karol have been taking? All the work in those papers is essentially to produce fibration categories that have a very strict sort of universe object; a slightly weaker sort of universe object is easy to obtain. Presumably the contextual categories in the conjectural Th HoTT\mathrm{Th}_{\mathrm{HoTT}} will contain strict universes, which at some point in the “univalent” versions of the pathway through TrbTrb and FibCatFibCat will have to become the weak ones of ElTop ElTop_\infty. Is the sort of model-categorical wrangling that I’ve been doing going to be useful in constructing one of these equivalences, or is there going to be a slicker approach that avoids it entirely? (Don’t worry about hurting my feelings; I’ve always felt that the approach of those papers was basically a stopgap until we came up with something better.)

Posted by: Mike Shulman on November 23, 2017 8:50 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories II

Is the sort of model-categorical wrangling that I’ve been doing going to be useful in constructing one of these equivalences, or is there going to be a slicker approach that avoids it entirely?

I have to admit that I’m not as familiar with your results as I would like to. However, as far as I understand it is a promising approach. If it is possible to push your techniques to produce a universal injective fibration in the category of simplicial presheaves over a simplicial category, then we could try to understand how compatible this is with our constructions. If there is any slicker approach, then I’m not aware of it (which doesn’t say much since I haven’t spent any significant amount of time thinking about it).

Posted by: Karol Szumiło on November 23, 2017 9:43 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories II

Another question is whether your approach to these conjectures will work with HoTT as the metatheory (assuming a solution to the problem of defining internal (,1)(\infty,1)-categories in HoTT)? IIRC you’re using quasicategories as your model for (,1)(\infty,1)-categories, which are too “set-based” to use for defining internal (,1)(\infty,1)-categories in HoTT. But perhaps a similar theory could be developed using complete Segal spaces, which would then be more likely to internalize?

Posted by: Mike Shulman on November 23, 2017 8:52 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories II

In principle, the choice of a model of (,1)(\infty, 1)-categories shouldn’t matter at all. The reason why I used quasicategories in my comparison between fibration categories and finitely complete (,1)(\infty, 1)-categories is that I was able to provide a nice construction of the quasicategory associated to a fibration category in a way that allows for a direct comparison between homotopy limits in a fibration category and limits in the resulting quasicategory.

This construction also has a very natural enhancement to complete Segal spaces. If it is possible to introduce simplicial types in HoTT and internalize basic theory of complete Segal spaces, then this construction should also internalize.

On the other hand, I feel that perhaps many of the technical difficulties, that we had to fight with, boil down to the fact that we use a strict point set level representation of homotopy types in the form of simplicial sets. One could hope that once we understand the story well enough to internalize it in HoTT, we will discover that at least some of these difficulties go away just by the virtue of the synthetic approach to homotopy types.

Posted by: Karol Szumiło on November 23, 2017 10:08 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories II

Can we see how \infty-Gabriel-Ulmer duality could plausibly go?

Lex op LFP C Lex(C,Set) \begin{matrix} Lex^{op} & \to & LFP \\ C & \mapsto & Lex(C, Set) \end{matrix}

Your CompCat Id,Σ\mathrm{CompCat}_{Id,\Sigma} is equivalent to Lex Lex_{\infty}. So we’d expect a category of models, CLex (C,Grpd)C \mapsto Lex_{\infty}(C, \infty Grpd), of a locally-finitely presentable nature?

I get confused around type theory, the way it speaks of models and theories. E.g., CompCat Id,Σ\mathrm{CompCat}_{Id,\Sigma} is described as “the categorical models of type theory”.

There seems to be the need to speak of type theory in general; type theory with specified type formation; then perhaps a theory in this type of theory (involving postulation of some types).

Then will there a model theory for such things?

Posted by: David Corfield on November 24, 2017 9:01 AM | Permalink | Reply to this

Univerity of Kent

I see the suggestion of how to form an \infty-Gabriel-Ulmer duality is to

replace Lex with the \infty-category of finitely complete and idempotent complete \infty-categories…

What rests on the addition of the ‘idempotent complete’ condition?

Posted by: David Corfield on February 22, 2018 4:07 PM | Permalink | Reply to this

Re: Univerity of Kent

The reason for including idempotent-complete is that to make the duality work you need a category CC to be determined by its presheaf category (or by some subcategory thereof), and this is only true in general when CC is Cauchy-complete, i.e. idempotent-complete. The reason for not including it in the 1-categorical case is that a finitely complete 1-category is automatically idempotent-complete, since idempotent-splitting in a 1-category is a finite limit, as opposed to in an (,1)(\infty,1)-category where it is not a finite limit.

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

Re: Univerity of Kent

Thanks! So can this property feature in the account of the main post? It wasn’t specified in Lex Lex_{\infty} above.

Posted by: David Corfield on February 22, 2018 7:01 PM | Permalink | Reply to this

Univerity of Kent

Oh, is it that type theory won’t be able to specify these non-finite limits?

Posted by: David Corfield on February 22, 2018 7:26 PM | Permalink | Reply to this

Re: Univerity of Kent

Right, the type theory with only Σ\Sigma and IdId-types that corresponds to Lex Lex_\infty can’t talk about infinite limits.

Interestingly, however, if our type theory also includes Π\Pi-types (with function extensionality) and \mathbb{N}, then we can prove internally that sufficiently coherent idempotents split. This (and more) is shown in my paper Idempotents in intensional type theory, by adapting Lurie’s quasicategorical methods. And because the splitting requires only a finite amount of coherence, I believe it should imply that externally coherent idempotents also split.

Type theory with Σ,Id,Π,\Sigma,Id,\Pi,\mathbb{N} should correspond to locally cartesian closed (,1)(\infty,1)-categories with natural numbers objects, which don’t figure directly in any kind of Gabriel-Ulmer duality that I know of. However, it might be possible to describe idempotent-complete finitely-complete (,1)(\infty,1)-categories type-theoretically by putting Π\Pi and \mathbb{N} types only in the non-fibrant part of a two-level type theory and then asserting axiomatically that fibrant types are closed under the “idempotent-splitting” construction.

Posted by: Mike Shulman on February 22, 2018 10:30 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories II

I said

I get confused around type theory, the way it speaks of models and theories… There seems to be the need to speak of type theory in general; type theory with specified type formation; then perhaps a theory in this type of theory (involving postulation of some types).

Fortunately Mike comes to the rescue in his HOTTEST talk from around slide 30, where first ‘doctrine’ is used for ‘kind of type theory’,and then numbered levels are brought in, so we have type 0-, 1- and 2-theories, and even 3-theories.

So we might choose to work in the type 3-theory which is dependent type theory, then choose to work in it with a specific type 2-theory with specific type constructors, say Martin-Löf dependent type theory.

Then we may choose to specify some types and axioms they satisfy for a 1-theory in our 2-theory. Finally we can choose an interpretation of our 1-theory as a model, which may be called a 0-theory.

At the nLab we have higher doctrine, which will need some updating.

Posted by: David Corfield on April 20, 2018 10:39 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories II

I am pleased to be working with Chris and with five other people on the basis of our shared admiration for Tom Hales, but one shouldn’t conclude that I am equipped to understand anything whatsoever in the parts of the conference that I didn’t help to organize. In particular, there’s no reason to think that I would understand anything in Chris’s post.

What’s surprising is that I did actually understand a little bit of the point of the post, though certainly not the details. I even have a vague understanding of the title, certainly more than I would have had I tried to read Chris’s first post under this title. At the time, the unfamiliar expression “the internal language” sounded to me doubly presumptuous: first by the use of the definite article, secondly by the implication that something like the essense of higher categories could only be revealed by the use of some sort of type theory.

What happened in the meantime: two homotopy theorists explained to me that “internal language” is just the name of a functor between something involving categories and something involving one of the branches of formal logic. Thanks to Tom Hales and a number of other people, I have become aware not only that model theory can be beneficial to progress in number theory, but also that the model theorists have things so well under control that one can simply quote the results they prove (like transfer principles for Fundamental Lemmas) without having to worry about understanding the proofs.

I am not yet convinced that type theories will be so beneficial to number theory, although I am open to changing my mind. In recent years homotopy theory has been invading number theory on several independent fronts, and type theories may follow in their wake. If that happens, however, I suspect, in view of the steep language barrier, that the influence will be limited to a handful of experts, and the rest of us will just be happy to use their theorems.

Posted by: Michael Harris on November 26, 2017 4:20 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories II

The idea of the internal language of a category or higher category is not quite as scary as you’re making it sound. It’s just the language you’d speak if you lived there. For example, people who live in the category of sets — people who do lots of stuff with sets — say things like

xy(x,y)SyT \forall x \exists y \; (x,y) \in S \implies y \in T

and reason about these sentences using various well-known rules. But people visiting other categories, or higher categories, talk a bit differently, and use somewhat different rules.

The idea is that it’s very useful to think ‘inside’ a framework instead of just reasoning about it from outside. For this you need to speak the native language.

And luckily, the native languages of different mathematical structures are a lot simpler and more similar to each other than different natural languages.

I have an absurdly talented friend who learned Norwegian just because he was going to visit Oslo for a few weeks. He said it was easy because he already knew English, German and Swedish (and French, and Italian, and Greek, and Sanskrit, and Mandarin, and so on). With math, one doesn’t need to be such a genius: once you know set theory it’s pretty easy to pick up the internal languages of other theories.

Or it would be, if mathematicians weren’t so stuffy and stiff when it comes to explaining things! And if there weren’t so many other interesting things to do.

Taking those last facts into account: yeah, for a number theorist it’s probably best to wait and only learn the internal language of \infty-topos theory if enough of your friends start speaking it that it gets annoying to be left out of the conversations.

Posted by: John Baez on November 26, 2017 9:33 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories II

It’s great to have an update like this, thanks! I’ve previously been bewildered by the bits and pieces I’d heard about the semantics of (Ho)TT, lost as to the relationships between the various different formalisms. But I’m now getting the impression of something like a hierarchy of levels of strictness in the different formalisms, each one a natural stepping-stone in the gap between the syntax and the models of (Ho)TT. And moreover, the gaps between these stepping-stones are being bridged one at a time by comparison theorems. Excellent!

One thing that piques my interest is your (Chris’s) and Karol’s use of what sounds like some serious simplicial machinery in the form of “Waldhausen’s approximation properties” (Chris linked to this above, but since he linked to several different papers, here’s a direct link, see 2.8 and 2.9). A quick search of that paper also reveals usage in some form of both Quillen’s Theorems A and B, which I also tend to think of as powerful, heavy-duty tools.

I’m curious: how common is it to use these sorts of simplicial tools in the semantics of (Ho)TT? Maybe they’re already commonplace – if not, I suppose I’d expect them to become increasingly important as the field progresses and matures!

Posted by: Tim Campion on November 27, 2017 2:39 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories II

I suspect that my familiarity with recent work on homotopical semantics of type theory is a little lacking. However, I know a couple of papers such as this, this or this and they all use standard methods of abstract homotopy theory and simplicial homotopy theory. Our work is a direct continuation of this trend.

You brought up Waldhausen’s approximation properties and Quillen’s Theorems A and B. (BTW, I wouldn’t count the former as “simplicial homotopy theory”, it doesn’t really have anything to do with simplicial sets.)

Since interpretation of HoTT involves various fibration category-like structures, it is only natural that comparisons between them will use something like the approximation properties. If they didn’t show up before, it’s probably because most results so far concerned properties of particular models rather than relations between them. In our work we had to look at these relations very seriously and we used the tools that were already in place.

In case of Theorems A and B, I would say that their use is somewhat coincidental but not unexpected. After all, the crucial feature of homotopical interpretations of HoTT is that substitution in dependent types corresponds to homotopy pullbacks and Theorems A and B are very standard tools for computing homotopy pullbacks in simplicial homotopy theory. The reason why their appearance is coincidental is that it followed a particular choice of models of presheaves of \infty-groupoids over a fibration category (namely, simplicial presheaves over its hammock localization). Really, there is nothing about HoTT that would dictate this particular choice over a number of other possibilities. Yet, we tried many other models and couldn’t make them work for very technical reasons (and I still lack conceptual understanding of what exactly went wrong). In any case, the crucial point is Proposition 6.9 which asserts that homotopy pullbacks in a fibration category agree with homotopy pullbacks of representable presheaves. With our model of choice it seemed most natural to prove this using Theorems A and B, but with other models we would have used some other standard tools of homotopy theory.

In short: yes, I think we can expect more “heavy-duty” tools to be important in the study of semantics of HoTT. Eventually, perhaps we will study it in HoTT itself, as Mike envisions, in which case classical simplicial homotopy theory would become less relevant. But I expect that we should be able to make a lot of progress using classical methods before we figure out how to internalize it in HoTT.

Posted by: Karol Szumiło on November 27, 2017 5:02 AM | Permalink | Reply to this

Post a New Comment