## 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.

### 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 $G$ be a planar finite graph, with each
edge $e$ regarded as a formal variable denoted $x_e$. Then the following
two polynomials are equal:

$\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.

## 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?

## 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.

## 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

$x y x = x$

for all $x$ and all $y$.

**Puzzle 1.** Prove that

$x y z = x z$

for all $x,y$ and $z$.

**Puzzle 2.** Prove that

$x x = x$

for all $x$.

## 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.

### 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:

## 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.

### 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.

## May 21, 2015

### The Origin of the Word “Quandle”

#### Posted by John Baez

A quandle is a set equipped with a binary operation with number of properties, the most important being that it distributes over itself:

$a \triangleright (b \triangleright c) = (a \triangleright b)\triangleright (a \triangleright c)$

They show up in knot theory, where the operation $\triangleright$ describes what happens when one strand crosses over another… and the laws are chosen so that the quandle gives an *invariant* of a knot, independent of how you draw it. Even better, the quandle is a complete invariant of knots: if two knots have isomorphic quandles, there’s a diffeomorphism of $\mathbb{R}^3$ mapping one knot to the other.

I’ve always wondered where the name ‘quandle’ came from. So I decided to ask their inventor, David Joyce—who also proved the theorem I just mentioned.

## May 18, 2015

### The Revolution Will Not Be Formalized

#### Posted by Mike Shulman

After a discussion with Michael Harris over at the blog about his book Mathematics without apologies, I realized that there is a lot of confusion surrounding the relationship between homotopy type theory and computer formalization — and that moreover, this confusion may be causing people to react negatively to one or the other due to incorrect associations. There are good reasons to be confused, because the relationship is complicated, and various statements by prominent members of both communities about a “revolution” haven’t helped matters. This post and its sequel(s) are my attempt to clear things up.

## May 13, 2015

### Categorifying the Magnitude of a Graph

#### Posted by Simon Willerton

Tom Leinster introduced the idea of the magnitude of graphs (first at the Café and then in a paper). I’ve been working with my mathematical brother Richard Hepworth on categorifying this and our paper has just appeared on the arXiv.

Categorifying the magnitude of a graph, Richard Hepworth and Simon Willerton.

The magnitude of a graph can be thought of as an integer power series. For example, consider the Petersen graph.

Its magnitude starts in the following way. $\begin{aligned} \#P&=10-30q+30q^{2}+90q ^{3}-450q^{4}\\ &\quad\quad+810q^{5} + 270 q^{6} - 5670 q^{7} +\dots. \end{aligned}$

Richard observed that associated to each graph $G$ there is a bigraded group $\mathrm{MH}_{\ast ,\ast }(G)$, the **graph magnitude homology** of $G$, that has the graph magnitude $# G$ as its graded Euler characteristic.
$\begin{aligned}
#G &= \sum _{k,l\geqslant 0} (-1)^{k}\cdot \mathrm{rank}\bigl (\mathrm{MH}_{k,l}(G)\bigr )\cdot q^{l}\\
&= \sum _{l\geqslant 0} \chi \bigl (\mathrm{MH}_{\ast ,l}(G)\bigr )\cdot q^{l}.
\end{aligned}$
So graph magnitude homology categorifies graph magnitude in the same sense that Khovanov homology categorifies the Jones polynomial.

For instance, for the Petersen graph, the ranks of $\mathrm{MH}_{k,l}(P)$ are given in the following table. You can check that the alternating sum of each row gives a coefficient in the above power series.

$\begin{array}{rrrrrrrrrr} &&&&&&k\\ &&0&1&2&3&4&5&6&7 \\ &0 & 10\\ & 1 & & 30 \\ &2 & && 30 \\ &3 &&& 120 & 30 \\ l &4 &&&& 480 & 30 \\ &5 &&&&& 840 & 30 \\ &6 &&&&& 1440 & 1200 & 30 \\ &7 &&&&&& 7200 & 1560 & 30 \\ \\ \end{array}$

Many of the properties that Tom proved for the magnitude are shadows of properties of magnitude homology and I’ll describe them here.

## April 30, 2015

### Breakfast at the n-Category Café

#### Posted by Emily Riehl

Michael Harris recently joined us for breakfast at the *n*-category café. Perhaps some readers here would be interested in following the postprandial discussion that is underway on his blog: Mathematics Without Apologies.

## April 28, 2015

### Categories in Control

#### Posted by John Baez

To understand ecosystems, ultimately will be to understand networks.- B. C. Patten and M. Witkamp

A while back I decided one way to apply my math skills to help save the planet was to start pushing toward green mathematics: a kind of mathematics that can interact with biology and ecology just as fruitfully as traditional mathematics interacts with physics. As usual with math, the payoffs will come slowly, but they may be large. It’s not a substitute for doing other, more urgent things—but if mathematicians don’t do this, who will?

As a first step in this direction, I decided to study *networks*.

This May, a small group of mathematicians is meeting in Turin for a workshop on the categorical foundations of network theory, organized by Jacob Biamonte. I’m trying to get us mentally prepared for this. We all have different ideas, yet they should fit together somehow.

Tobias Fritz, Eugene Lerman and David Spivak have all written articles here about their work, though I suspect Eugene will have a lot of completely new things to say, too. Now I want to say a bit about what I’ve been doing with Jason Erbele.

## April 24, 2015

### A Synthetic Approach to Higher Equalities

#### Posted by Mike Shulman

At last, I have a complete draft of my chapter for Elaine Landry’s book *Categories for the working philosopher*. It’s currently titled

**Homotopy Type Theory: A synthetic approach to higher equalities**. pdf

As you can see (if you read it), not much is left of the one fragment of draft that I posted earlier; I decided to spend the available space on HoTT itself rather than detour into synthetic mathematics more generally. Although the conversations arising from that draft were still helpful, and my other recent ramblings did make it in.

Comments, questions, and suggestions would be very much appreciated! It’s due this Sunday (I got an extension from the original deadline), so there’s a very short window of time to make changes before I have to submit it. I expect I’ll be able to revise it again later in the process, though.