The n-Category Café

To kick things off, here’s one thing I learned from Mike’s really excellent talk: the univalence axiom is what allows us to form the (synthetic) $\infty$-groupoid of (synthetic) $\infty$-groupoids.

Mike,

The notions of “synthetic” and “analytic” are quite interesting here, though I only understood one tenth of your slides. Still, it reminds me of Tarski’s representation theorem for the (first-order) axiom system $EG_2$ of 2-dimensional synthetic Euclidean geometry, in Tarski’s 1959 paper “What is elementary geometry?”, which is available here:

http://www.corelab.ntua.gr/studygroup/Tarski_ElGeom.pdf

The primitive concepts of Tarski’s geometry are

$x = y$

$Bet(x,y,z)$: “$y$ lies between $x$ and $z$”

$Cong(x,y,z,w)$: “the segment $xy$ is congruent to the segment $zw$”

The representation theorem is:

$\mathcal{M} \models EG_2$ iff $\mathcal{M} \cong \mathcal{C}_2(\mathbb{F})$, where $\mathbb{F}$ is a real-closed field.

Here $\mathcal{C}_2(\mathbb{F})$ is what Tarski calls the 2-dimensional “Cartesian space over the field $\mathbb{F}$”. That is, its carrier set is $\mathbb{F}^2$, and its distinguished relations are Betweenness ($\subseteq \mathbb{F}^3$) and Congruence ($\subseteq \mathbb{F}^4$), defined using $\mathbb{F}$ instead of $\mathbb{R}$. So, the standard case–for standard 2-dimensional $\mathbb{R}^2$–is:

$\mathcal{C}_2(\mathbb{R}) = (\mathbb{R}^2, Bet_{\mathbb{R}}, Cong_{\mathbb{R}})$.

But the models $\mathcal{C}_2(\mathbb{F})$ of geometry can be non-standard, e.g., if $\mathbb{F}$ is the countable real-closed field of algebraic reals.

So, considering $HoTT$ is to be a “synthetic” theory, then what you’d like is some kind of representation theorem for $HoTT$.

Jeff

Oh good! I was going to ask for these too…

Can you say about more about the last slide in the first section? How would this give a recipe for computing unstable homotopy groups of spheres? And could you remind me what you said about the dependency of this on the meaning of “small”?

I’m not sure if Mike mentioned this in his talk, but the “almost” next to Guillaume Brunerie’s proof that pi4(S^3) = Z2 is an intriguing first example of how we might actually “compute” homotopy groups in an algorithmic sense.

For most of the proofs we’ve done, we need to know the answer, and then we prove it’s correct—e.g., we need to know that pi_1(S^1) should turn out to be Z, and then we do a proof of this fact.

What Guillaume proved is that there exists a k such that pi4(S^3) = Zk. But, assuming univalence and higher inductives can be made constructive (currently a big open problem, but many people think it will turn out to be true), the proof is constructive. So we can run the proof and check that k is indeed 2. This is the first example we have where an algorithm would be computing some of the information.

The meaning of “synthetic” is by contrast with “analytic”, as in Euclid’s synthetic geometry (with undefined notions of points, lines, etc. satisfying axioms) versus cartesian analytic geometry (where points and lines are defined using pairs of real numbers).

The striking thing about Book I of The Elements as we read it today is that notions of points and lines are defined.

Definition 1. A point is that which has no part.

Definition 2. A line is breadthless length.

Definition 3. The ends of a line are points.

With Hilbert, we lose the definitions.

But you can’t keep a good concept down, and there on our nLab point entry is

As a topological space, the point is the usual point from geometry: that which has no part. In more modern language, we might say that it has no structure – except that something exists.

I would imagine that there’s an interesting history to the analytic/synthetic distinction. At the nLab page, we have Klein drawing attention to figures, rather than implicit definitions:

Synthetic geometry is that which studies figures as such, without recourse to formulas, whereas analytic geometry consistently makes use of such formulas as can be written down after the adoption of an appropriate system of coordinates.

He’s thinking of the likes of Jakob Steiner. Was it he who taught his students geometry in pitch darkness?

This in itself is a change from Greek conceptions of analysis and synthesis. I remember Lakatos had an interesting paper on the ‘Method of Analysis-Synthesis’ (in Vol. 2 of his Collected Papers). It was conceived originally more as a process, where one used both analysis and synthesis.

I rather suspect that your use here of the analytic/synthetic distinction marks a further development.