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.

July 28, 2015

Internal Languages of Higher Categories

Posted by Mike Shulman

(guest post by Chris Kapulkin)

I recently posted the following preprint to the arXiv:

Btw if you’re not the kind of person who likes to read mathematical papers, I also gave a talk about the above mentioned work in Oxford, so you may prefer to watch it instead. (-:

I see this work as contributing to the idea/program of HoTT as the internal language of higher categories. In the last few weeks, there has been a lot of talk about it, prompted by somewhat provocative posts on Michael Harris’ blog.

My goal in this post is to survey the state of the art in the area, as I know it. In particular, I am not going to argue that internal languages are a solution to many of the problems of higher category theory or that they are not. Instead, I just want to explain the basic idea of internal languages and what we know about them as far as HoTT and higher category theory are concerned.

Disclaimer. The syntactic rules of dependent type theory look a lot like a multi-sorted essentially algebraic theory. If you think of sorts called types and terms then you can think of rules like Σ\Sigma-types and Π\Pi-types as algebraic operations defined on these sorts. Although the syntactic presentation of type theory does not quite give an algebraic theory (because of complexities such as variable binding), it is possible to formulate dependent type theory as an essentially algebraic theory. However, actually showing that these two presentations are equivalent has proven complicated and it’s a subject of ongoing work. Thus, for the purpose of this post, I will take dependent type theories to be defined in terms of contextual categories (a.k.a. C-systems), which are the models for this algebraic theory (thus leaving aside the Initiality Conjecture). Ultimately, we would certainly like to know that these statements hold for syntactically-presented type theories; but that is a very different question from the \infty-categorical aspects I will discuss here.

A final comment before we begin: this post derives greatly from my (many) conversations with Peter Lumsdaine. In particular, the two of us together went through the existing literature to understand precisely what’s known and what’s not. So big thanks to Peter for all his help!

Internal languages of categories

First off, what is the internal language? Without being too technical, let me say that it is typically understood as a correspondence:

(1){theories}LangCl{categories} \left\{\text{theories}\right\} \overset{\mathrm{Cl}}{\underset{\mathrm{Lang}}{\rightleftarrows}} \left\{\text{categories}\right\}

On the right hand side of this correspondence, we have a category of categories with some extra structure and functors preserving this structure. On the left hand side, we have certain type theories, which are extensions of a fixed core one, and their interpretations (which are, roughly speaking, maps taking types to types and terms to terms, preserving typing judgements and the constructors of the core theory). Notice that the core theory is the initial object in the category of theories in the above picture.

The functor Cl\mathrm{Cl} takes a theory to its initial model, built directly out of syntax of the theory: the objects are contexts and the morphisms are (sequences of) terms of the theory (this category is often called the classifying category, hence the notation Cl\mathrm{Cl}). The functor Lang\mathrm{Lang} takes a category to the theory whose types are generated in a suitable sense by the objects and whose terms are generated by the morphisms of the category. In particular, constructing Lang(C)\mathrm{Lang}(C) for some category CC from the right hand side is the same as establishing a model of the core theory in CC.

Finally, these functors are supposed to form some kind of an adjoint equivalence (with ClLang\mathrm{Cl} \dashv \mathrm{Lang}), be it an equivalence of categories, bi-equivalence, or \infty-equivalence, depending on whether the two sides of the correspondence are categories, 22-categories, or \infty-categories.

The cleanest example of this phenomenon is the correspondence between λ\lambda-theories (that is, theories in simply typed λ\lambda-calculus) and cartesian closed categories:

(2){theories in λ-calculus}LangCl{cartesian closed categories} \left\{\begin{array}{c}\text{theories in}\\ \lambda\text{-calculus}\end{array}\right\} \overset{\mathrm{Cl}}{\underset{\mathrm{Lang}}{\rightleftarrows}} \left\{\begin{array}{c}\text{cartesian closed}\\ \text{categories}\end{array}\right\}

which you can read about in Part I of the standard text by Jim Lambek and Phil Scott.

Extensional Martin-Löf Type Theory

Unfortunately, as soon as we move to dependent type theory, things are getting more complicated. Starting with the work of Robert Seely, it has become clear that one should expect Extensional Martin-Löf Type Theory (with dependent products, dependent sums, and extensional Identity types) to be the internal language of locally cartesian closed categories:

(3){Extensional Martin-Löf type theories}LangCl{locally cartesian closed categories} \left\{\begin{array}{c}\text{Extensional Martin-Löf}\\ \text{type theories}\end{array}\right\} \overset{\mathrm{Cl}}{\underset{\mathrm{Lang}}{\rightleftarrows}} \left\{\begin{array}{c}\text{locally cartesian}\\ \text{closed categories}\end{array}\right\}

Seely overlooked however an important coherence problem: since types are now allowed to depend on other types, we need to make coherent choices of pullbacks. The reason for that is that type-theoretically substitution (into a type) is a strictly functorial operation, whereas its categorical counterpart, pullback, without making any choices, is functorial only up to isomorphism. (If you find the last sentence slightly too brief, I recommend Peter Lumsdaine’s talk explaining the problem and known solutions.) The fix was later found by Martin Hofmann; but the resulting pair of functors does not form an equivalence of categories, only a biequivalence of 22-categories, as was proven in 2011 by Pierre Clairambault and Peter Dybjer.

Intensional Martin-Löf Type Theory and locally cartesian closed \infty-categories

Next let us consider Intensional Martin-Löf Type Theory with dependent products and sums, and the identity types; additionally, we will assume the (definitional) eta rule for dependent functions and functional extensionality.

Such type theory has been, at least informally, conjectured to be the internal language of locally cartesian closed \infty-categories and thus, we expect the following correspondence:

(4){Intensional Martin-Löf type theories}LangCl{locally cartesian closed -categories} \left\{\begin{array}{c}\text{Intensional Martin-Löf}\\ \text{type theories}\end{array}\right\} \overset{\mathrm{Cl}}{\underset{\mathrm{Lang}}{\rightleftarrows}} \left\{\begin{array}{c}\text{locally cartesian}\\ \text{closed } \; \infty\text{-categories}\end{array}\right\}

where the functors Cl\mathrm{Cl} and Lang\mathrm{Lang} should form an adjunction (an adjoint (,1)(\infty,1)-equivalence? or maybe even (,2)(\infty,2)-equivalence?) between the type-theoretic and categorical sides.

Before I summarize the state of the art, let me briefly describe what the two functors ought to be. Starting with a type theory, one can take its underlying category of contexts and regard it as category with weak equivalences (where the weak equivalences are syntactically-defined equivalences), to which one can then apply the simplicial localization. This gives a well-defined functor from type theories to \infty-categories. Of course, it is a priori not clear what the (essential) image of such a functor would be.

Conversely, given a locally cartesian closed \infty-category CC, one can look for a category with weak equivalences (called the presentation of CC) whose simplicial localization is CC and then try to establish the structure of a categorical model of type theory on such a category.

What do we know? The verification that Cl\mathrm{Cl} takes values in locally cartesian closed \infty-categories can be found in my paper. The other functor is known only partially. More precisely, if CC is a locally presentable locally cartesian closed \infty-category, then one can construct Lang(C)\mathrm{Lang}(C). As mentioned above, the construction is done in two steps. The first, that is presenting such an \infty-category by a type-theoretic model category (which is, in particular, a category with weak equivalences) was given by Denis-Charles Cisinski and Mike Shulman in these blog comments, and independently in Theorem 7.10 of this paper by David Gepner and Joachim Kock. The second step (the structure of a model of type theory) is precisely Example 4.2.5.3 of the local universe model paper by Peter Lumsdaine and Michael Warren.

What don’t we know? First off, how to define Lang(C)\mathrm{Lang}(C) when CC is not locally presentable and whether the existing definition of Lang(C)\mathrm{Lang}(C) for locally presentable quasicategories is even functorial? We also need to understand what the homotopy theory of type theories is (if we’re hoping for an equivalence of homotopy theories, we need to understand the homotopy theory of the left hand side!)? In particular, what are the weak equivalences of type theories? Next in line: what is the relation between Cl\mathrm{Cl} and Lang\mathrm{Lang}? Are they adjoint and if so, can we hope that they will yield an equivalence of the corresponding \infty-categories?

Univalence, Higher Inductive Types, and (elementary) \infty-toposes

Probably the most interesting part of this program is the connection between Homotopy Type Theory and higher topos theory (HoTT vs HTT?). Conjecturally, we should have a correspondence:

(5){Homotopy Type Theories}LangCl{elementary -toposes} \left\{\begin{array}{c}\text{Homotopy}\\ \text{Type Theories}\end{array}\right\} \overset{\mathrm{Cl}}{\underset{\mathrm{Lang}}{\rightleftarrows}} \left\{\begin{array}{c}\text{elementary}\\ \infty\text{-toposes}\end{array}\right\}

This is however not a well-defined problem as it depends on one’s answer to the following two questions:

  1. What is HoTT? Obviously, it should be a system that extends Intensional Martin-Löf Type Theory, includes at least one, but possibly infinitely many univalent universes, and some Higher Inductive Types, but what exactly may largely depend on the answer to the next question…
  2. What is an elementary \infty-topos? While there exist some proposals (for example, that presented by André Joyal in 2014), this question also awaits a definite answer. By analogy with the 11-categorical case, every Grothendieck \infty-topos should be an elementary \infty-topos, but not the other way round. Moreover, the axioms of an elementary \infty-topos should imply (maybe even explicitly include) that it is locally cartesian closed and that it has finite colimits, but should not imply local presentability.

What do we know? As of today, only partial constructions of the functor Lang\mathrm{Lang} exist. More precisely, there are:

  • Theorem 6.4 of Mike Shulman’s paper contains the construction of Lang(C)\mathrm{Lang}(C) if CC is a Grothendieck \infty-topos that admits a presentation as simplicial presheaves on an elegant Reedy category and HoTT is taken the extension of Intensional Martin-Löf Type Theory but as many univalent universes à la Tarski as there are inaccessible cardinals greater than the cardinality of the site.
  • Remark 1.1 of the same paper can be interpreted as saying that if one considers HoTT with weak (univalent) universes instead, then the construction of Lang(C)\mathrm{Lang}(C) works for an arbitrary \infty-topos CC.
  • A forthcoming paper by Peter Lumsdaine and Mike Shulman will supplement the above two points: for some reasonable range of higher toposes, the resulting type theory Lang(C)\mathrm{Lang}(C) will be also shown to possess certain Higher Inductive Types (e.g. homotopy pushouts and truncations), although the details remain to be seen.

What don’t we know? It still remains to define Lang(C)\mathrm{Lang}(C) outside of the presentable setting, as well as give the construction of Cl\mathrm{Cl} in this case (or rather, check that the obvious functor from type theories to \infty-categories takes values in higher toposes). The formal relation between these functors (which are yet to be defined) remains wide open.

Posted at July 28, 2015 3:30 AM UTC

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

23 Comments & 0 Trackbacks

Re: Internal Languages of Higher Categories

A naive question: if the goal is to construct a right adjoint to a known functor, is there any hope to accomplish this via some sort of adjoint functor theorem? I suppose the biggest issue would lie in resolving what exactly the \infty-category of “homotopy type theories” is?

Posted by: Tim Campion on July 29, 2015 6:11 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

if the goal is to construct a right adjoint to a known functor, is there any hope to accomplish this via some sort of adjoint functor theorem? I suppose the biggest issue would lie in resolving what exactly the ∞-category of “homotopy type theories” is?

Good thought! That’s certainly one big issue; not just what it is, but is it the sort of category to which an adjoint functor theorem can be applied. Moreover, I would guess that an even bigger issue would be showing that the known functor preserves colimits. Even showing that it preserves the initial object seems to be highly nontrivial. At present I don’t think we know any way of constructing maps out of ∞-categories of the form Cl(T)Cl(T), except by invoking a known construction of LangLang on the desired codomain!

Posted by: Mike Shulman on August 10, 2015 5:52 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

It should be said, of course, that one wouldn’t be satisfied with just applying the adjoint functor theorem – we’re building a syntactic object and we want explicit control over the syntax. And anyway, we eventually want to see we have an equivalence. It’s just that being in the situation of trying to understand an object which “exists by abstract nonsense” is a bit different from trying to construct an object which “morally should exist”, but might in principle not exist.

I suppose the natural “warm-up” question to ask is: does the adjoint functor theorem apply in the extensional case? Do the appropriate colimits exist in the 2-category of extensional Marin-Löf type theories, does an appropriate generating/solution set condition hold, and finally, is it possible to show directly that the semantics functor preserves colimits? To make it even easier, one might think about existence of colimits and a generating set on the other side of the equivalence to start with – does the 2-category of LCCC’s (resp. the 2-category of Grothendieck toposes) have colimits and a generating set?

(Actually, I’m realizing that I don’t actually know a biadjoint functor theorem. Size issues in particular seem to be potentially tricky. What’s a good reference?).

Posted by: Tim Campion on August 15, 2015 9:32 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

I wonder if the right warm-up here is rather to ask about the 2-category LogTopLogTop of elementary toposes and logical morphisms between them? Namely to try and think of the

HoTT \leftrightarrow \: Elementary \infty-topos

correspondence as a generalization of the

Intuitionistic Type Theory \leftrightarrow \: LogTop

correspondence established by Lambek and Scott. Of course, I understand that in moving from intensional MLTT to HoTT is like moving from \infty-LCCC to \infty-toposes and this also makes Grothendieck toposes a plausible “toy version”. But it still seems to me that the “elementariness” of the \infty-toposes corresponding to HoTT is the really important piece of information. (But there’s also probably fewer interesting things one can say about LogTop…)

Posted by: Dimitris on August 18, 2015 4:30 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

Because of some technical glitch, your equations are not being properly rendered.

Posted by: Jeffery Winkler on August 4, 2015 7:48 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

They look fine to me.

Posted by: Mike Shulman on August 4, 2015 7:53 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

Me too.

Posted by: Tom Leinster on August 6, 2015 12:04 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

They look better now. Maybe the problem was on my computer.

Posted by: Jeffery Winkler on August 11, 2015 7:38 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

Here are direct links to at least two of those ‘provocative’ posts on Michael Harris’s blog:

There may be others of which I am not aware.

Posted by: Todd Trimble on August 5, 2015 2:48 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

A very valuable summary of the state of the art!

In all the examples here, the domain of the map

Lang:{categories}{theories} Lang: \{categories\} \to \{theories\}

is an (,2)(\infty,2)-category of (,1)(\infty,1)-categories of some kind. What work has been done pushing up the numbers 11 and 22 here? For example, things of this general flavor:

Lang:{2categories}{2theories} Lang: \{2-categories\} \to \{2-theories\}

I know some work on Lawvere 2-theories, but Lawvere theories are so far down the ladder of expressiveness that you didn’t even mention them!

Posted by: John Baez on August 8, 2015 11:30 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

I’m almost certain you know this given the recent discussion on 22-categorical models of the Pi-calculus, but let me just mention that along similar lines you can consider even the λ\lambda-calculus as giving rise to a 22-category by interpreting conversions as 22-cells, e.g. as in Seely’s work here.

This would/should give you a correspondence between 33-categories of the general flavor you are after (though I’m not sure anyone ever wrote this down).

But I guess you don’t want to think of the λ\lambda-calculus as “inherently” a “22-theory” even though a 22-category can be defined out of its syntax?

Posted by: Dimitris on August 8, 2015 12:57 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

I’m personally happy to think of the conversions in the λ\lambda-calculus as 2-cells. I taught a course on this in 2007. My student Mike Stay took this course, and this was my attempt to learn enough λ\lambda-calculus to serve as his advisor. I tried to get him to work on this subject, but he said that the λ\lambda-calculus was old hat and decided to work on π\pi-calculus instead, using some of the same ideas.

Right now I’m wanting to take this opportunity to learn everything possible about work on pushing the ‘internal language of a category’ idea up to the case of higher categories where the higher cells aren’t equivalences… since Chris nicely summarized the case where they are.

Posted by: John Baez on August 9, 2015 8:16 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

Back in 2009-10 I was working on a sort of 2-categories that ought to be in the domain of such a functor for dependent type theory, but at the time I didn’t know enough type theory to be sufficiently precise about that side of things (and for the most part I didn’t even realize my ignorance). On the other side, in 2011 Dan Licata and Bob Harper wrote about a 2-dimensional directed type theory, but didn’t consider general categorical models. Both of our approaches had in common that there are two kinds of “dependent types”, covariant and contravariant. But I don’t know of anyone who’s pushed ideas like those any further, and I guess all of us have been too busy since then with the (,1)(\infty,1)-case to think much more about the 2-case.

Posted by: Mike Shulman on August 8, 2015 5:41 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

There is also Richard Garner’s work on (undirected) 2-dimensional type theory. Roughly, Garner’s 2DTT has equality reflection only for identity types. So it is intensional up to level 2, which allows natural 2-categorical models with terms of identity types interpreted as 2-cells. (Footnote 3 on p. 41 of that paper is probably the most explicit statement of the kind of result you were after that I am aware of.)

(Garner’s 2DTT is much closer to MLTT than the directed type theories that Mike and Licata-Harper were considering – at least as far as I can tell.)

Posted by: Dimitris on August 8, 2015 6:32 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

I don’t think undirected 2DTT is what John was asking about, because he mentioned pushing up the numbers 1 and 2. Undirected 2DTT would instead be pushing down the number \infty.

Posted by: Mike Shulman on August 8, 2015 6:42 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

On the subject of generalizing the locally-cartesian-closed-∞-category case beyond locally presentable ones, can we just use the Yoneda embedding?

That is, if CC is a small lcc ∞-category, then its presheaf ∞-category 𝒫C\mathcal{P}C is locally presentable and lcc, so we can construct Lang(𝒫C)Lang(\mathcal{P}C). Now since CC is lcc, its image in 𝒫C\mathcal{P}C should be closed under dependent products. Thus, the full subtheory of Lang(𝒫C)Lang(\mathcal{P}C) determined by the representable objects should be a theory of the right sort, and seems like a good candidate for Lang(C)Lang(C).

Of course, it’s no longer as small as CC, but that seems like a technical detail that it should be possible to work around. More seriously, it won’t inherit any colimity structure from CC, although I suppose we could try to fix that by looking at some kind of sheaves instead.

This seems too obvious to have been overlooked, however, so maybe I’m missing something…

Posted by: Mike Shulman on August 10, 2015 5:51 AM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

Regarding the homotopy theory of (homotopy) type theories. I understand that defining such an a thing is a meaningful mathematical problem and can be studied for its own sake. (All the more so if one replaces syntactically presented (homotopy) type theories with contextual categories as is the case above.) But is there also a meaningful logical interpretation of this problem?

Let me clarify. In the category of contextual categories the objects are meant to be theories (these theories are also the models of an essentially algebraic theory but that shouldn’t cause any confusion). Arrows between theories are best understood as interpretations. So an arrow between (homotopy) type theories should be an interpretation of some kind. And a functor between contextual categories preserving all the extra structure is just such a thing. In particular, given a contextual functor F:C 1C 2F \colon C_1 \rightarrow C_2 then any “judgment” that is “derivable” in a contextual category C 1C_1 will also be derivable in any other contextual category C 2C_2. (I’m putting scare quotes around the words judgment and derivable because of the issues around the Initiality Conjecture.)

So far so good. The mathematical structure of the 1-category of contextual categories has a direct logical meaning: arrows are interpretations. But does a similar logical interpretation exist for the (undefined) \infty-category of contextual categories? I don’t immediately see what the higher arrows would mean from a logical point of view. “Interpretations between interpretations between interpretations etc.” – ok, but what is an interpretation between an interpretation? Must not one have some indication about what this means in order to be guided in defining the homotopy theory of (homotopy) type theories? (If not, what is one guided by?)

To clarify: I’m not doubting the mathematical interest of the problem of finding a homotopy theory of (homotopy) type theories (which is obvious). I’m merely wondering whether there is a logical interpretation of the problem. Namely, I accept that a given type theory – viewed as a contextual category – can itself be treated mathematically as a “space” rather than just a theory of “spaces”. But is there a logical meaning to this “spatial” aspect?

(Disclaimer: I’m probably ignoring the “Disclaimer” above in asking this.)

Posted by: Dimitris on August 18, 2015 2:04 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

I would say that a “natural equivalence” between two interpretations F,G:C 1C 2F,G:C_1\to C_2 just says that if I have a judgment derivable in C 1C_1, and I use FF and GG to interpret it as judgments derivable in C 2C_2, then those two judgments in C 2C_2 are equivalent, in a way varying naturally with the judgment.

Posted by: Mike Shulman on August 18, 2015 8:25 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

But would one be able to motivate or explain this notion of “natural equivalence of judgments” to someone who lived only in the syntactically presented part of (intensional) MLTT?

Posted by: Dimitris on August 18, 2015 8:55 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

C 2C_2 classifies models of a theory, say “C 2C_2-models”, and similarly for C 1C_1. The two “interpretations” F,G:C 1C 2F, G : C_1 \rightarrow C_2 determine two different “semantic” functors from C 2C_2-models to C 1C_1-models, and a map between them, say, an equivalence h:FGh : F \simeq G, determines a natural map (resp. equivalence) between these semantic functors.
Posted by: Steve Awodey on August 18, 2015 9:39 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

Once one agrees to view interpretations as functors (of any kind) of course I agree that it makes sense to have arrows between interpretations. But what I’m asking is whether there is a concept comprehensible purely in terms of the syntactic presentation of type theories to which these natural transformations between interpretation functors correspond? (Of course there is one in a loose sense, since we can simply reverse-engineer the kind of reasoning you or Mike outline back to the syntax and we’ll end up with some notion – is this notion then something that we care/know about in logic? This is what I’m asking.)

Let me illustrate with a crude, non-type-theoretic analogy. Some first-order theories TT will have a category of models Mod(T)Mod(T) that also has a natural (in the non-technical sense) 22-categorical structure. The obvious example is the theory of categories T catT_{cat}. Does the 22-categorical structure of Mod(T cat)Mod(T_{cat}) encode something syntactic about T catT_{cat} as a first-order theory? It does not: the 22-categorical structure of Mod(T cat)Mod(T_{cat}) is not in any meaningful sense “definable” out of the syntactic presentation of T catT_cat. On the other hand (as you, of course, are well aware) there are other structures one can place on the category of models of a first-order theory that are directly definable in terms of the syntax, e.g. topological or ultracategorical structure.

So my question can be rephrased as follows: is the (sought-after) homotopy theoretic structure of the category Con=Mod(T contextual)Con=Mod(T_{contextual}) of the first or of the second kind? Is it supposed to reflect a property of the syntax, or is it merely a structure on the category of models of the syntax not directly definable out of the syntax? And if the latter, presumably there will be non-equivalent homotopy theories on ConCon – is there a “logical” way to distinguish between them? Or would one simply have to rely on the homotopy theory of the semantic side (quasicategories) to try and find something (homotopically) equivalent to it?

Posted by: Dimitris on August 18, 2015 11:05 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

Thanks to the work of Barwick and Kan, a higher category can be equivalently described as a category with weak equivalences (a.k.a. a relative category). Thus maybe we can reformulate your question and ask about the logical meaning of weak equivalences between type theories.

Peter Lumsdaine and I recently posted the following preprint to the arXiv:

We show there that the category of type theories can be equipped with a left semi-model structure in the sense of Spitzweck. In particular, the class of weak equivalences that we consider is closely related to the notion of conservativity, as studied by Martin Hofmann in his PhD thesis (written in 1995, so way before HoTT!).

Posted by: Chris Kapulkin on October 19, 2016 11:52 PM | Permalink | Reply to this

Re: Internal Languages of Higher Categories

is this notion then something that we care/know about in logic?

My guess is that it’s something we should care about in logic, but that hasn’t been studied much or at all before.

I do think that in order to make ClLangCl\dashv Lang an equivalence (rather than just an adjunction or something weaker), there is often an element of “proof by definition” in the construction of the higher category of theories on the LHS. So maybe the right attitude is that because we know there is this connection between theories and categories, we conclude that it may be fruitful to import categorical concepts into the study of theories.

Posted by: Mike Shulman on August 20, 2015 3:55 AM | Permalink | Reply to this

Post a New Comment