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

## April 12, 2015

### The Structure of A

#### Posted by David Corfield

I attended a workshop last week down in Bristol organised by James Ladyman and Stuart Presnell, as part of their Homotopy Type Theory project.

Urs was there, showing everyone his magical conjuring trick where the world emerges out of the opposition between **$\emptyset$** and **$\ast\;$** in Modern Physics formalized in Modal Homotopy Type Theory.

Jamie Vicary spoke on the Categorified Heisenberg Algebra. (See also John’s page.) After the talk, interesting connections were discussed with dependent linear type theory and tangent (infinity, 1)-toposes. It seems that André Joyal and colleagues are working on the latter. This should link up with Urs’s Quantization via Linear homotopy types at some stage.

As for me, I was speaking on the subject of my chapter for the book that Mike’s *Introduction to Synthetic Mathematics* and John’s *Concepts of Sameness* will appear in. It’s on reviving the philosophy of geometry through the (synthetic) approach of cohesion.

In the talk I mentioned the outcome of some further thinking about how to treat the phrase ‘the structure of $A$’ for a mathematical entity. It occurred to me to combine what I wrote in that discussion we once had on The covariance of coloured balls with the analysis of ‘the’ from The King of France thread. After the event I thought I’d write out a note explaining this point of view, and it can be found here. Thanks to Mike and Urs for suggestions and comments.

The long and the short of it is that there’s no great need for the word ‘structure’ when using homotopy type theory. If anyone has any thoughts, I’d like to hear them.

## April 7, 2015

### Information and Entropy in Biological Systems

#### Posted by John Baez

I’m helping run a workshop on Information and Entropy in Biological Systems at NIMBioS, the National Institute of Mathematical and Biological Synthesis, which is in Knoxville Tennessee.

I think you’ll be able to watch live streaming video of this workshop while it’s taking place from Wednesday April 8th to Friday April 10th. Later, videos will be made available in a permanent location.

To watch the workshop live, go **here**. Go down to where it says

Investigative Workshop: Information and Entropy in Biological Systems

Then click where it says **live link**. There’s nothing there *now*, but I’m hoping there will be when the show starts!

## April 6, 2015

### Five Quickies

#### Posted by Tom Leinster

I’m leaving tomorrow for an “investigative workshop” on Information and Entropy in Biological Systems, co-organized by our own John Baez, in Knoxville, Tennessee. I’m excited! And I’m hoping to learn a lot.

A quick linkdump before I go:

## March 14, 2015

### Split Octonions and the Rolling Ball

#### Posted by John Baez

You may enjoy these webpages:

because they explain a nice example of the Erlangen Program more tersely — and I hope more simply — than before, with the help of some animations made by Geoffrey Dixon using WebGL. You can actually get a ball to roll in way that illustrates the incidence geometry associated to the exceptional Lie group $\mathrm{G}_2$!

Abstract.Understanding exceptional Lie groups as the symmetry groups of more familiar objects is a fascinating challenge. The compact form of the smallest exceptional Lie group, $\mathrm{G}_2$, is the symmetry group of an 8-dimensional nonassociative algebra called the octonions. However, another form of this group arises as symmetries of a simple problem in classical mechanics! The space of configurations of a ball rolling on another ball without slipping or twisting defines a manifold where the tangent space of each point is equipped with a 2-dimensional subspace describing the allowed infinitesimal motions. Under certain special conditions, the split real form of $\mathrm{G}_2$ acts as symmetries. We can understand this using the quaternions together with an 8-dimensional algebra called the ‘split octonions’. The rolling ball picture makes the geometry associated to $\mathrm{G}_2$ quite vivid. This is joint work with James Dolan and John Huerta, with animations created by Geoffrey Dixon.

## March 11, 2015

### A Scale-Dependent Notion of Dimension for Metric Spaces (Part 1)

#### Posted by Simon Willerton

Consider the following shape that we are zooming into and out of. What dimension would you say it was?

At small scales (or when it is very far away) it appears as a point, so seems zero-dimensional. At bigger scales it appears to be a line, so seems one-dimensional. At even bigger scales it appears to have breadth as well as length, so seems two-dimensional. Then, finally, at very large scales it appears to be made from many widely separated points, so seems zero-dimensional again.

We arrive at an important observation:

The perceived dimension varies with the scale at which the shape is viewed.

Here is a graph of my attempt to capture this perceived notion of dimension mathematically.

Hopefully you can see that, moving from the left, you start off at zero, then move into a region where the function takes value around one, then briefly moves up to two then drops down to zero again.

The ‘shape’ that we are zooming into above is actually a grid of $3000\times 16$ points as that’s all my computer could handle easily in making the above picture. If I’d had a much bigger computer and used say $10^{7}\times 10^{2}$ points then I would have got something that more obviously had both a one-dimensional and two-dimensional regime.

In this post I want to explain how this idea of dimension comes about. It relies on a notion of ‘size’ of metric spaces, for instance, you could use Tom’s notion of magnitude, but the above picture uses my notion of $2$-spread.

I have mentioned this idea before at the Café in the post on my spread paper, but I wanted to expand on it somewhat.

## March 9, 2015

### HITs and the Erlangen Program

#### Posted by Mike Shulman

Last week I had a minor epiphany, which I would like to share. If it holds up, it’ll probably end up somewhere in my chapter for Landry’s book.

I was fortunate during my formal education to have the opportunity to take a fair number of physics classes in addition to mathematics. Over that time I was introduced to tensors (more specifically, tensor fields on manifolds) several times in a row: first in special relativity, then in differential geometry, and then again in general relativity and Riemannian geometry.

During all those classes, I remember noticing that mathematicians and physicists tended to speak about tensors in different ways. To a mathematician, a tensor (field) was a global geometric object associated to a manifold; upon choosing a local chart it could be expressed using local coordinates, but fundamentally it was a geometric thing. By contrast, physicists tended to talk about a tensor as a collection of coordinates labeled by indices, with its “tensorial” nature encoded in how those coordinates transformed upon changing coordinates.

(To be sure, most physicists nowadays are aware of the mathematician’s perspective, and many even use it. But I still got the sense that they found it easier, or at least expected that we students would find it easier, to think in coordinates.)

Here is my epiphany: the symbiosis between these two viewpoints on tensors is closely related to the symbiosis between HITs and univalence in homotopy type theory. I will now explain…

## March 5, 2015

### Mathematics Without Apologies

#### Posted by David Corfield

Since I had reviewed the manuscript for Princeton University Press eighteen months ago, this week I received my complementary copy of Mathematics Without Apologies by Michael Harris.

Michael, as most people here will know, is a number theorist whose successes include, with Richard Taylor, the proof of the local Langlands conjecture for the general linear group $GL_n(K)$ in characteristic 0. But alongside being a prize-winning mathematician, he also likes to think hard about the nature of mathematics. He spoke at a conference I co-organised, Two Streams in the Philosophy of Mathematics, and I’ve met up with him on a number of other occasions, including the Delphi meeting with John. He’s extremely well placed then to give an account of the life of a current mathematician with, as suggested by the book’s subtitle, *Portrait of a problematic vocation*, all its peculiarities.

I’ll be re-reading the book once term is over, and say more then, but for now those wanting to find out more can read a Q&A with the author, and drafts of some chapters available here. Michael has also set up an associated blog, named after the book.

## February 27, 2015

### Concepts of Sameness (Part 4)

#### Posted by John Baez

This time I’d like to think about three different approaches to ‘defining equality’, or more generally, *introducing* equality in formal systems of mathematics.

These will be taken from old-fashioned logic — before computer science, category theory or homotopy theory started exerting their influence. Eventually I want to compare these to more modern treatments.

If you know other interesting ‘old-fashioned’ approaches to equality, please tell me!

## February 26, 2015

### Introduction to Synthetic Mathematics (part 1)

#### Posted by Mike Shulman

John is writing about “concepts of sameness” for Elaine Landry’s book *Category Theory for the Working Philosopher*, and has been posting some of his thoughts and drafts. I’m writing for the same book about homotopy type theory / univalent foundations; but since HoTT/UF will also make a guest appearance in John’s and David Corfield’s chapters, and one aspect of it (univalence) is central to Steve Awodey’s chapter, I had to decide what aspect of it to emphasize in my chapter.

My current plan is to focus on HoTT/UF as a *synthetic theory of $\infty$-groupoids*. But in order to say what that even means, I felt that I needed to start with a brief introduction about the phrase “synthetic theory”, which may not be familiar. Right now, my current draft of that “introduction” is more than half the allotted length of my chapter; so clearly it’ll need to be trimmed! But I thought I would go ahead and post some parts of it in its current form; so here goes.

## February 25, 2015

### Concepts of Sameness (Part 3)

#### Posted by John Baez

Now I’d like to switch to pondering different approaches to equality. (Eventually I’ll have put all these pieces together into a coherent essay, but not yet.)

We tend to think of $x = x$ as a fundamental property of equality, perhaps the most fundamental of all. But what is it actually *used* for? I don’t really know. I sometimes joke that equations of the form $x = x$ are the only really *true* ones — since any other equation says that *different* things are equal — but they’re also completely *useless*.

But maybe I’m wrong. Maybe equations of the form $x = x$ are useful in some way. I can imagine one coming in handy at the end of a proof by contradiction where you show some assumptions imply $x \ne x$. But I don’t remember ever doing such a proof… and I have trouble imagining that you ever *need* to use a proof of this style.

If you’ve used the equation $x = x$ in your own work, please let me know.

## February 23, 2015

### Concepts of Sameness (Part 2)

#### Posted by John Baez

I’m writing about ‘concepts of sameness’ for Elaine Landry’s book *Category Theory for the Working Philosopher*. After an initial section on a passage by Heraclitus, I had planned to write a bit about Gongsun Long’s white horse paradox — or more precisely, his dialog *When a White Horse is Not a Horse*.

However, this is turning out to be harder than I thought, and more of a digression than I want. So I’ll probably drop this plan. But I have a few preliminary notes, and I might as well share them.

### Concepts of Sameness (Part 1)

#### Posted by John Baez

Elaine Landry is a philosopher at U. C. Davis, and she’s editing a book called *Categories for the Working Philosopher*. Tentatively, at least, it’s supposed to have chapters by these folks

- Colin McLarty (on set theory)
- David Corfield (on geometry)
- Michael Shulman (on univalent foundations)
- Steve Awodey (on structuralism, invariance, and univalence)
- Michael Ernst (on foundations)
- Jean-Pierre Marquis (on first-order logic with dependent sorts)
- John Bell (on logic and model theory)
- Kohei Kishida (on modal logic)
- Robin Cockett and Robert Seely (on proof theory and linear logic)
- Samson Abramsky (on computer science)
- Michael Moortgat (on linguistics and computational semantics)
- Bob Coecke and Aleks Kissinger (on quantum mechanics and ontology)
- James Weatherall (on spacetime theories)
- Jim Lambek (on special relativity)
- John Baez (on concepts of sameness)
- David Spivak (on mathematical modeling)
- Hans Halvorson (on the structure of physical theories)
- Elaine Landry (on structural realism)
- Andrée Ehresmann (on a topic to be announced)

We’re supposed to have our chapters done by April. To make writing my part more fun, I thought I’d draft some portions here on the $n$-Café.

## February 18, 2015

### Quantum Physics and Logic at Oxford

#### Posted by John Baez

There’s a workshop on quantum physics and logic at Oxford this summer:

- 12th International Workshop on Quantum Physics and Logic, Department of Computer Science, University of Oxford. Tutorials July 13–14 and Workshop July 15–17, 2015. Organized by Destiny Chen, Chris Heunen, Peter Selinger and Jamie Vicary.

## February 12, 2015

### Can a Computer Solve Lebesgue’s Universal Covering Problem?

#### Posted by John Baez

Here’s a problem I hope we can solve here. I think it will be fun. It involves computable analysis.

To state the problem precisely, recall that the **diameter** of a set of points $A$ in a metric space is

$diam(A)=\sup\{d(x,y) : x,y\in A\}$

Recall that two subsets of the Euclidean plane $\mathbb{R}^2$ are **isometric** if we can get one from the other by translation, rotation and/or reflection.

Finally, let’s define a **universal covering** to be a convex compact subset $K$ of the Euclidean plane such that any set $A \subseteq \mathbb{R}^2$ of diameter $1$ is isometric to a subset of $K$.

In 1914 Lebesgue posed the puzzle of finding the universal covering with the least area. Since then people have been using increasingly clever constructions to find universal coverings with smaller and smaller area.

My question is whether we need an unbounded amount of cleverness, or whether we could write a program to solve this puzzle.

There are actually a number of ways to make this question precise, but let me focus on the simplest. Let $\mathcal{U}$ be the set of all universal coverings. Can we write a program that computes this number to as much accuracy as desired:

$a=inf\{ area(K) : K \in \mathcal{U}\} \; ?$

More precisely, is this real number $a$ computable?

Right now all we know is that

$0.832 \le a \le 0.844115376859\dots$

though Philip Gibbs has a heuristic argument for a better lower bound:

$0.84408 \le a$