The torus is the product of two circles, cubically

But I guess it's cool you can prove the same thing with over-abstract gobbledygook

We can start with geometry, which is pretty intuitive and understandable: squares, circles, triangles, lines, points, cubes, etc. In general we can talk about geometric spaces; shapes are then the boundaries between their "inside" space and their "outside" space. Geometry is obviously useful for all kinds of problems.

We can generalise geometry to get topology. Essentially we pretend that everything's made of elastic, so instead of talking about exact shapes and angles, we're allowed to bend, stretch and squash everything, which I'll call "transformations". We're not allowed to cut holes in things, or to glue things together, since our transformations must be smooth and reversible.

For example, a cube and a sphere are different geometrically, but they are the same topologically, since we can transform one to get the other. Hence topology is a way of grouping together geometric shapes.

This may sound abstract and silly, but it has some very direct applications. For example, when we're wiring up a network, other than the length of wire required, we don't really care about it's geometry. We'd like to treat our network in a way which ignores the literal shape of the wires, and just tells us what the connections are. That's what topology does: two networks have the same topology if we can transform the wires of one to get the wires of another. Disconnecting is "cutting a hole", adding connections is "gluing together", so doing either will change the topology. That makes topological spaces a great model for networks.

If we go up another layer of abstraction, we get homotopy. Instead of dealing with the transformation of spaces, homotopy deals with the transformation of transformations! If we can smoothly (ie. without "cutting" or "sticking") transform one transformation into another, then they're homotopically the same. For example, we can consider transformations to take place over the space of 1 second: at time 0 we have our original shape and at time 1 we have our final shape, with a smooth progression of shapes in-between. In the same way, we can consider transforming our transformations over a period of 1 second; eg. at time 0 we have a transformation which squashes a shape to half its length, and at time 1 we have a transformation which stretches a shape to twice its length. In-between we have a smooth progression of transformations; in particular, at time 0.5 we have a transformation which does nothing (half-way between squashing and stretching).

Now this all sounds really abstract and really silly, with no possible applications. But the truly amazing thing is, homotopy theory turns out to be a great way to model computer programs!

It works like this: we can use spaces from topology to model types in computer programs. Each point in a space is a value of the type corresponding to that space. Computation is the transformation of input values (points) to output values (points). Higher-order functions (like `map` and `reduce`) are transformations-of-transformations, like in homotopy.

In particular we can use this model to gain insights into equality (when two values are "the same") and isomorphism (when two values are "equivalent"; we transform from one to the other). This is hugely important, because a whole load of computing effort is spent transforming between equivalent values (parsing, pretty-printing, serialising, etc.). Homotopy Type Theory uses the idea of "univalence", which basically says "if you can transform back and forth between two things, then you can use them interchangably". If our programming languages allowed this, it would be huge. We could write all of our programs using nice, high-level data structures, and the compiler would automatically transform them into any equivalent representation we like. For example, we could doing a bunch of manipulation to lists of booleans, concatenating them, splicing them, etc. and our compiler could emit code which performed bit-wise operations on machine words. All it would take to make two programs communicate is to show how to transform the datatypes of one into the datatypes of the other, and the compiler would automatically apply those transformations wherever necessary.

Unfortunately, an exact algorithm for univalence hasn't been discovered yet. Most researchers think it's possible though.

So what's this result? Basically, they've taken the topological space containing circles, and turned it into a type `Circle`; they've then made a tuple type containing two of them `(Circle, Circle)`. They've then turned this type back into a topological space and shown that it's a torus. If you think about it, that makes sense: a "circle of circles" is a torus.