The n-Category Café

guest post by Mike Stay

Way back in 2006 when this blog started, we had a discussion about cartesian closed categories and the lambda calculus. There we learned about Lawvere’s invention of categorical semantics and how modern programming languages use his ideas for defining and implementing datatypes. Basically, a datatype declaration is a presentation of a cartesian closed category. Implementations of the datatype are cartesian closed functors from that category to Set; these pick out a set of values for the datatype along with functions that act on those values and satisfy the given relations. The datatype declaration is “syntax”, and the implementation functor assigns “semantics” in Set to the syntax.

In Robin Milner’s 1991 Turing Award lecture, he explained how Set doesn’t work as a target for implementing concurrent programs. He showed how the two programs

{A: x = 1; x = x + 1;}

and

{B: x = 2;}

when run individually, assign to x the same value. But if we run them concurrently, x may be either 2 or 3 depending on whether program A completes before or after the first statement in program B. So we need to look elsewhere for a categorical semantics for concurrent programs.

Horribly late — sorry, Fernando! — I just sent in a review of The Colours of Infinity, a popular book on fractals. It’s for the online reviews of the Mathematical Association of America.

It’s not entirely complimentary. You could also call it unfair: I’ve judged the book by its interest to mathematicians (because that’s what I was asked to do), whereas it plainly wasn’t written for that readership. You can read my review here, and for balance you can read some much more positive reviews at Amazon.

For the first time ever, I’ve used a Creative Commons licence. I’ve been interested for a while in finding out about Creative Commons licences, and I thought I’d take the plunge by using one on something of relatively low importance. Call it jumping in at the shallow end.

Creative Commons has a range of licences, depending on factors such as whether you want to allow commercial use of your work and whether you want to allow other people to modify it. They have a handy licence chooser. For this review, I decided to use the most liberal licence: so in the unlikely event that you want to rewrite my review and sell it, you’re free to do so.

This will be the last post in this introductory sequence, although I will probably continue to post about new developments in homotopy type theory from time to time. (If you’re interested in the subject, you should also follow the HoTT blog.) Today I want to talk about a new, somewhat more radical idea, which we are currently calling higher inductive types.

The version of this I’m going to present below arose at Oberwolfach in discussions between Peter Lumsdaine, Andrej Bauer, Michael Warren, and myself, and since then Chris Kapulkin has also joined us in thinking about them. Peter did the initial implementation in Coq and noticed many of the applications below; a couple are my own inventions. (He also simultaneously wrote a post for the HoTT blog on the same subject.) I’m also told that Dan Licata and Steve Awodey have independently been working on related ideas. We all believe that this idea has the potential to solve many of the problems of homotopy type theory in a clean way, and one which moreover accords well with both type-theoretic and homotopy-theoretic intuition.

In May there is the following workshop in Cardiff:

• Workshop on Higher Gauge Theory, TQFT and Categorification

  Monday 9th - Tuesday 10th May 2011

  School of Mathematics, Cardiff University

  website

organized by WIMCS, more precisely by the Mathematical Physics Cluster of the Wales Institute of Mathematical and Computational Sciences. Timothy Porter is doing the organisation of the programme whilst the hard work is being done by Mathew Pugh and David Evans down in Cardiff.

Below are some of the speakers, talk titles and abstracts. The list is incomplete. If you are a speaker and would like more information about your talk be visible here, please send me an email.

I missed the first one, but not this:

• Higher structures in China II, August 8-10, 2011, Jilin University, Changchun. Organized by Yunhe Sheng, Chenchang Zhu and Zhangju Liu.

There’s a conference on quantum gravity in Zurich this summer:

• Quantum Theory and Gravitation, ETH Zurich, June 14–24, 2011. Local organizers: Jürg Fröhlich and Matthias Gaberdiel. Scientific advisory board: John Barrett, Harald Grosse, Hermann Nicolai, Roger Picken and Carlo Rovelli.

Guest post by Aaron Smith on Freyd’s lecture – An Anti-Philosophy of Mathematics

What follows is a quick-and-dirty summary of Peter Freyd’s talk “An Anti-philosophy of Mathematics” delivered April 11th at UPenn.

Professor Freyd’s talk, although interwoven with several anecdotes about his interactions with many bright lights of the field of logic/mathematical foundations, was mainly concerned with discussing characteristics of mathematics with a view toward giving some account of what mathematics is. (With regard to the provocative title, I was unable to make a lot of sense of the explanation he gave, or at least it’s relevance to the rest of the discussion. He pointed out that he wouldn’t be surprised if we eventually saw a Godel-like theorem stating that any sufficiently rich language will produce questions which are inherently unanswerable and perhaps even nonsensical within the language –perhaps to say that the question at hand “What is mathematics” is such a question?]

In any case, he brought out the main theme by focusing on the challenge of giving a definition of mathematics to an uninitiated person. He first drew a distinction between mathematics [what mathematicians do] and the mathematical [mathematical techniques], the former being what he was describing as mathematics –and the latter not. The existence of this distinction seemed to imply that mathematics was about something or concerned with something rather than merely being a methodology. But what is this something?

This May Graeme Segal will give the Felix Klein Lectures at the Hausdorff Center for Mathematics in Bonn.

Three roles of quantum field theory

• May 2 - 18

• website

Abstract Quantum field theory has many roles, and the lectures will be about three of them. The primary role is to provide a description of all of fundamental physics when gravity is firmly excluded. A second, at first surprising, role has emerged from string theory, which is a theory of gravitation: it turns out that a two-dimensional field theory can be regarded as a generalized manifold, and in particular can be a model for space-time. Thirdly, quite apart from physics, the concept of a field theory has taken on a new life as an organizing principle in other areas of mathematics - not only in geometry and representation theory, but even in connection with quantum computing.

The three roles can be seen together as aspects of noncommutative geometry, and that will be a central theme of the lectures. The talks will aim to show how powerful the field theory idea is by jumping between a variety of contexts, beginning from the origins of the structure in particle physics, with a little about so-called “Wick rotation”, and then moving towards more pure-mathematical applications to analysis, algebra, and the structure of manifolds.

If you’re tired of all this type theory and are longing for some good old 2-category theory, this post is for you. Today on the arXiv we have the long-awaited paper:

• Enhanced 2-categories and limits for lax morphisms, by Stephen Lack and Michael Shulman: arXiv.

The goal of this paper is to characterize the 2-categorical limits which exist in 2-categories of categories-with-structure and morphisms which preserve that structure laxly (up to a not-necessarily-invertible comparison map). However, it turns out that we can get a more useful theorem if instead of 2-categories, we work with richer structures called $\mathcal{F}$-categories (these are the “enhanced 2-categories” of the title).

I started this tale by pointing out two ‘problems’ with real and quaternionic quantum theory:

• Apparently you can’t get observables from symmetries. More precisely: 1-parameter unitary groups on real or quaternionic Hilbert spaces don’t have self-adjoint generators, as they do in complex quantum theory.
• Apparently you can’t tensor two quaternionic Hilbert spaces. More precisely, you can’t tensor two quaternionic Hilbert spaces (which are one-sided $\mathbb{H}$-modules) and get another one.

You may have heard me say before that I am fond of a notion called cohesive ∞-toposes . This is a rather minimalistic extra condition on an ∞-topos $\mathbf{H}$ that ensures that internal to $\mathbf{H}$ there is a good notion of differential geometry and differential cohomology.

For instance internal to every cohesive $\infty$-topos is an intrinsic notion of de Rham cohomology, where “intrinsic” means: it is described using nothing by $\infty$-(co)limits and adjoint $\infty$-functors. This has the nice effect that on the one hand a good deal of general abstract properties of de Rham cohomology such as, say, its role in Chern-Weil theory, can be derived in vast generality using nothing but basic abstract higher category theory, while on the other hand it means that we have a good handle on constructing and understanding concrete realizations (models of the axioms).

(And it seems to me – in view of the recent insights on Homotopy Type Theory – that it also means that much of differential geometry/cohomology could eventually be “put on a computer”, for whatever that’s worth. That wasn’t – and isn’t – my motivation for looking into this, but maybe around here there are more people who can relate to this motivation than to, say, the construction of twisted differential string structures.)

With this intrinsic notion of differential forms in any cohesive $\infty$-topos comes automatically an intrinsic account of the infinitesimal . Accordingly, there is some $\infty$-Lie theory in any cohesive $\infty$-topos. However, the axioms only provide access to a somewhat coarse form of actual infinitesimals: for instance there is a notion of de Rham schematic homotopy type of any object in any cohesive $\infty$-topos, but not of its de Rham space. For some applications one wants to have an intrinsic access to the latter, for instance because that induces immediately an intrinsic notion of D-modules.

But there is a simple add-on to the axioms of a cohesive $\infty$-topos that does provide all this, and more: infinitesimal cohesion. In the following I briefly sketch how this works, and then I point out that both the abstract formalization as well as a good chunk of worked applications is at least implicit in some work by Maxim Kontsevich and Alexander Rosenberg.

I am thankful to Zoran Škoda for pushing me to read that article.

I think posts I-IV have more or less covered the current state of the art in homotopy type theory. I omitted a few things, like the fact that univalence implies function extensionality (but see below). I also didn’t talk too much about what people have proven inside homotopy type theory so far, like the fact that Ω² is abelian. But overall I think I gave a relatively complete picture (although knowledgable readers should feel free to object!).

What’s next is necessarily more speculative. In a comment to the last post, Urs raised what I think is one of the central questions of current research in homotopy type theory. I would phrase it as what do we still need to add to homotopy type theory to obtain a complete internal language for $(\infty,1)$-topoi?

On Friday 13 May, the Scottish Category Theory Seminar will meet for the fourth time at the University of Glasgow. We’re delighted to have as our speakers:

• Eugenia Cheng (Sheffield): Distributive laws for Lawvere theories
• Ekaterina Komendantskaya (Dundee): Coalgebraic semantics for derivations in logic programming
• Phil Scott (Ottawa): Partially traced categories
• Bruno Vallette (Max Planck Institute, Bonn): Algebra + homotopy = higher structure.

See the seminar website for further information.

So far in this series we’ve described the correspondence between type theory and homotopy theory and defined some basic notions of homotopy theory in type theory, including equivalences in several ways. We’ve also mentioned a few axioms that we may want to add to intensional type theory, including “function extensionality”, a subobject classifier, and a truncation $\pi_{-1} = \tau_{\le -1}$ into (-1)-types.

However, nothing we’ve said so far excludes the possibility that all types are discrete (= 0-types = sets). Intensional type theory plus function extensionality has sound semantics in any locally cartesian closed 1-category; and if the category is regular, then $\tau_{\le -1}$ exists; while if it is a topos, then of course it has a subobject classifier. But today I’ll introduce Voevodsky’s univalence axiom, which is not valid in any 1-categorical semantics—or, indeed, in $n$-categorical semantics for any finite $n$! The univalence axiom is perhaps the easiest and most intuitive way to require that our homotopy type theory is honestly “homotopical”, and it also has other pleasant consquences (including, perhaps surprisingly, function extensionality).

I’ve mentioned before that it hasn’t been easy selling category theory to philosophers. At first glance this may be a little surprising when you consider what effects changes to the foundational language of mathematics circa 1900 had on philosophy over subsequent years via the influence of Bertrand Russell. Perhaps one of the most important factors was that predicate logic could be applied straightforwardly to natural language in a way that appeared to resolve certain metaphysical questions. Just look at the baldness of the present King of France.

Now something which is dearly beloved of analytic philosophers of the very purest kind is modal logic. So were category theory to become an indispensable tool in modal logic, we might be onto a winner. This has partially motivated a couple of posts of mine (here and here). Let me see if I can sum up the confused state of my mind at present. Even if you don’t want to think about modal logic, I’ve put in a couple of questions which I’d love to hear answers to.