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.

August 31, 2015

Wrangling generators for subobjects

Posted by Emily Riehl

Guest post by John Wiltshire-Gordon

My new paper arXiv:1508.04107 contains a definition that may be of interest to category theorists. Emily Riehl has graciously offered me this chance to explain.

In algebra, if we have a firm grip on some object X X , we probably have generators for X X . Later, if we have some quotient X/ X / \sim , the same set of generators will work. The trouble comes when we have a subobject YX Y \subseteq X , which (given typical bad luck) probably misses every one of our generators. We need theorems to find generators for subobjects.

Posted at 5:33 PM UTC | Permalink | Followups (4)

August 17, 2015

A Wrinkle in the Mathematical Universe

Posted by John Baez

Of all the permutation groups, only S 6S_6 has an outer automorphism. This puts a kind of ‘wrinkle’ in the fabric of mathematics, which would be nice to explore using category theory.

For starters, let Bij nBij_n be the groupoid of nn-element sets and bijections between these. Only for n=6n = 6 is there an equivalence from this groupoid to itself that isn’t naturally isomorphic to the identity!

This is just another way to say that only S 6S_6 has an outer isomorphism.

And here’s another way to play with this idea:

Given any category XX, let Aut(X)Aut(X) be the category where objects are equivalences f:XXf : X \to X and morphisms are natural isomorphisms between these. This is like a group, since composition gives a functor

:Aut(X)×Aut(X)Aut(X) \circ : Aut(X) \times Aut(X) \to Aut(X)

which acts like the multiplication in a group. It’s like the symmetry group of XX. But it’s not a group: it’s a ‘2-group’, or categorical group. It’s called the automorphism 2-group of XX.

By calling it a 2-group, I mean that Aut(X)Aut(X) is a monoidal category where all objects have weak inverses with respect to the tensor product, and all morphisms are invertible. Any pointed space has a fundamental 2-group, and this sets up a correspondence between 2-groups and connected pointed homotopy 2-types. So, topologists can have some fun with 2-groups!

Now consider Bij nBij_n, the groupoid of nn-element sets and bijections between them. Up to equivalence, we can describe Aut(Bij n)Aut(Bij_n) as follows. The objects are just automorphisms of S nS_n, while a morphism from an automorphism f:S nS nf: S_n \to S_n to an automorphism f:S nS nf' : S_n \to S_n is an element gS ng \in S_n that conjugates one automorphism to give the other:

f(h)=gf(h)g 1hS n f'(h) = g f(h) g^{-1} \qquad \forall h \in S_n

So, if all automorphisms of S nS_n are inner, all objects of Aut(Bij n)Aut(Bij_n) are isomorphic to the unit object, and thus to each other.

Puzzle 1. For n6n \ne 6, all automorphisms of S nS_n are inner. What are the connected pointed homotopy 2-types corresponding to Aut(Bij n)Aut(Bij_n) in these cases?

Puzzle 2. The permutation group S 6S_6 has an outer automorphism of order 2, and indeed Out(S 6)= 2.Out(S_6) = \mathbb{Z}_2. What is the connected pointed homotopy 2-type corresponding to Aut(Bij 6)Aut(Bij_6)?

Puzzle 3. Let BijBij be the groupoid where objects are finite sets and morphisms are bijections. BijBij is the coproduct of all the groupoids Bij nBij_n where n0n \ge 0:

Bij= n=0 Bij n Bij = \sum_{n = 0}^\infty Bij_n

Give a concrete description of the 2-group Aut(Bij)Aut(Bij), up to equivalence. What is the corresponding pointed connected homotopy 2-type?

Posted at 9:45 AM UTC | Permalink | Followups (49)

August 9, 2015

Two Cryptomorphic Puzzles

Posted by John Baez

Here are two puzzles. One is from Alan Weinstein. I was able to solve it because I knew the answer to the other. These puzzles are ‘cryptomorphic’, in the vague sense of being ‘secretly the same’.

Posted at 7:21 AM UTC | Permalink | Followups (10)

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 (22)

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 (4)

June 29, 2015

What is a Reedy Category?

Posted by Mike Shulman

I’ve just posted the following preprint, which has apparently quite little to do with homotopy type theory.

The notion of Reedy category is common and useful in homotopy theory; but from a category-theoretic point of view it is odd-looking. This paper suggests a category-theoretic understanding of Reedy categories, which I find more satisfying than any other I’ve seen.

Posted at 6:33 PM UTC | Permalink | Followups (20)

Feynman’s Fabulous Formula

Posted by Simon Willerton

Guest post by Bruce Bartlett.

There is a beautiful formula at the heart of the Ising model; a formula emblematic of all of quantum field theory. Feynman, the king of diagrammatic expansions, recognized its importance, and distilled it down to the following combinatorial-geometric statement. He didn’t prove it though — but Sherman did.

Feynman’s formula. Let GG be a planar finite graph, with each edge ee regarded as a formal variable denoted x ex_e. Then the following two polynomials are equal:

H evenGx(H)= [γ]P(G)(1(1) w[γ]x[γ])\displaystyle \sum_{H \subseteq_{even} G} x(H) = \prod_{[\vec{\gamma}] \in P(G)} \left(1 - (-1)^{w[\vec{\gamma}]} x[\vec{\gamma}]\right)


I will explain this formula and its history below. Then I’ll explain a beautiful generalization of it to arbitrary finite graphs, expressed in a form given by Cimasoni.

Posted at 7:47 AM UTC | Permalink | Followups (19)

June 21, 2015

What’s so HoTT about Formalization?

Posted by Mike Shulman

In my last post I promised to follow up by explaining something about the relationship between homotopy type theory (HoTT) and computer formalization. (I’m getting tired of writing “publicity”, so this will probably be my last post for a while in this vein — for which I expect that some readers will be as grateful as I).

As a potential foundation for mathematics, HoTT/UF is a formal system existing at the same level as set theory (ZFC) and first-order logic: it’s a collection of rules for manipulating syntax, into which we can encode most or all of mathematics. No such formal system requires computer formalization, and conversely any such system can be used for computer formalization. For example, the HoTT Book was intentionally written to make the point that HoTT can be done without a computer, while the Mizar project has formalized huge amounts of mathematics in a ZFC-like system.

Why, then, does HoTT/UF seem so closely connected to computer formalization? Why do the overwhelming majority of publications in HoTT/UF come with computer formalizations, when such is still the exception rather than the rule in mathematics as a whole? And why are so many of the people working on HoTT/UF computer scientists or advocates of computer formalization?

Posted at 6:47 AM UTC | Permalink | Followups (10)

June 12, 2015

Carnap and the Invariance of Logical Truth

Posted by David Corfield

I see Steve Awodey has a paper just out Carnap and the invariance of logical truth. We briefy discussed this idea in the context of Mautner’s 1946 article back here.

Steve ends the article by portraying homotopy type theory as following in the same tradition, but now where invariance is under homotopy equivalence. I wonder if we’ll see some variant of the model/theory duality he and Forssell found in the case of HoTT.

Posted at 12:09 PM UTC | Permalink | Followups (2)

June 9, 2015

Semigroup Puzzles

Posted by John Baez

Suppose you have a semigroup: that is, a set with an associative product. Also suppose that

xyx=x x y x = x

for all xx and all yy.

Puzzle 1. Prove that

xyz=xz x y z = x z

for all x,yx,y and zz.

Puzzle 2. Prove that

xx=x x x = x

for all xx.

Posted at 2:30 PM UTC | Permalink | Followups (43)

May 26, 2015

A 2-Categorical Approach to the Pi Calculus

Posted by John Baez

guest post by Mike Stay

Greg Meredith and I have a short paper that’s been accepted for Higher-Dimensional Rewriting and Applications (HDRA) 2015 on modeling the asynchronous polyadic pi calculus with 2-categories. We avoid domain theory entirely and model the operational semantics directly; full abstraction is almost trivial. As a nice side-effect, we get a new tool for reasoning about consumption of resources during a computation.

It’s a small piece of a much larger project, which I’d like to describe here in a series of posts. This post will talk about lambda calculus for a few reasons. First, lambda calculus is simpler, but complex enough to illustrate one of our fundamental insights. Lambda calculus is to serial computation what pi calculus is to concurrent computation; lambda calculus talks about a single machine doing a computation, while pi calculus talks about a network of machines communicating over a network with potentially random delays. There is at most one possible outcome for a computation in the lambda calculus, while there are many possible outcomes in a computation in the pi calculus. Both the lazy lambda calculus and the pi calculus, however, have as an integral part of their semantics the notion of waiting for a sub-computation to complete before moving onto another one. Second, the denotational semantics of lambda calculus in Set is well understood, as is its generalization to cartesian closed categories; this semantics is far simpler than the denotational semantics of pi calculus and serves as a good introduction. The operational semantics of lambda calculus is also simpler than that of pi calculus and there is previous work on modeling it using higher categories.

Posted at 9:28 PM UTC | Permalink | Followups (36)

SoTFoM III and The Hyperuniverse Programme

Posted by David Corfield

Following SoTFom II, which managed to feature three talks on Homotopy Type Theory, there is now a call for papers announced for SoTFoM III and The Hyperuniverse Programme, to be held in Vienna, September 21-23, 2015.

Here are the details:

The Hyperuniverse Programme, launched in 2012, and currently pursued within a Templeton-funded research project at the Kurt Gödel Research Center in Vienna, aims to identify and philosophically motivate the adoption of new set-theoretic axioms.

The programme intersects several topics in the philosophy of set theory and of mathematics, such as the nature of mathematical (set-theoretic) truth, the universe/multiverse dichotomy, the alternative conceptions of the set-theoretic multiverse, the conceptual and epistemological status of new axioms and their alternative justificatory frameworks.

The aim of SotFoM III+The Hyperuniverse Programme Joint Conference is to bring together scholars who, over the last years, have contributed mathematically and philosophically to the ongoing work and debate on the foundations and the philosophy of set theory, in particular, to the understanding and the elucidation of the aforementioned topics. The three-day conference, taking place September 21-23 at the KGRC in Vienna, will feature invited and contributed speakers.

I wonder if anyone will bring some category theory along to the meeting. Perhaps they can answer my question here.

Further details:

Posted at 2:50 PM UTC | Permalink | Followups (5)

May 22, 2015

PROPs for Linear Systems

Posted by John Baez

PROPs were developed in topology, along with operads, to describe spaces with lots of operations on them. But now some of us are using them to think about ‘signal-flow diagrams’ in control theory—an important branch of engineering. I talked about that here on the n-Café a while ago, but it’s time for an update.

Posted at 8:43 PM UTC | Permalink | Followups (3)

How to Acknowledge Your Funder

Posted by Tom Leinster

A comment today by Stefan Forcey points out ways in which US citizens can try to place legal limits on the surveillance powers of the National Security Agency, which we were discussing in the context of its links with the American Mathematical Society. If you want to act, time is of the essence!

But Stefan also tells us how he resolved a dilemma. Back here, he asked Café patrons what he should do about the fact that the NSA was offering him a grant (for non-classified work). Take their money and contribute to the normalization of the NSA’s presence within the math community, or refuse it and cause less mathematics to be created?

What he decided was to accept the funding and — in this paper at least — include a kind of protesting acknowledgement, citing his previous article for the Notices of the AMS.

I admire Stefan for openly discussing his dilemma, and I think there’s a lot to be said for how he’s handled it.

Posted at 2:28 PM UTC | Permalink | Followups (2)