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!

Posted at 3:30 AM UTC | Permalink | Followups (23)

July 19, 2015

Category Theory 2015

Posted by John Baez

Just a quick note: you can see lots of talk slides here:

Category Theory 2015, Aveiro, Portugal, June 14-19, 2015.

The Giry monad, tangent categories, Hopf monoids in duoidal categories, model categories, topoi… and much more!

Posted at 9:19 AM UTC | Permalink | Followups (1)

July 8, 2015

Mary Shelley on Invention

Posted by Tom Leinster

From the 1831 introduction to Frankenstein:

Invention, it must be humbly admitted, does not consist in creating out of void, but out of chaos; the materials must, in the first place, be afforded: it can give form to dark, shapeless substances, but cannot bring into being the substance itself. […] Invention consists in the capacity of seizing on the capabilities of a subject, and in the power of moulding and fashioning ideas suggested to it.

She’s talking about literary invention, but it immediately struck me that her words are true for mathematical invention too.

Except that I can’t think of a part of mathematics I’d call “dark” or “shapeless”.

Posted at 12:54 PM UTC | Permalink | Followups (5)