# How can one define “punctured torus” in Homotopy Type Theory? Is its fundamental group the free product of the integers with themselves?

Questions.

1. Has the beautiful old idea, in part already known to Gauß, of a punctured torus surface (take, if you will, the classical set-theoretic definition as the meaning of the latter three words) been defined in Homotopy Type Theory already? If yes, how? If not, are there any choices in doing so or is one more or less forced towards a definition of "punctured surface"?
2. More specifically, has the classical isomorphism1

$\pi_1(\text{punctured torus})\cong \mathbb{Z}\ast\mathbb{Z}$

been proved in Homotopy Type Theory already?

1. Can one somehow 'conceptually' predict 'how' different from $\mathbb{Z}\ast\mathbb{Z}$ the answer could at worst be?

Remarks.

• Homotopy Type Theory has of course reached tori already (see Chapter 6 herein), more generally, arbitrary finite CW-complexes. But he punctured torus is not compact.

• Part of my motivation for asking this question is that I had occasion to explain to someone what it means that $S_{1,1}$ is not simply connected. Moreover, I try to teach myself a little Homotopy Type Theory. So I tried to find out what Homotopy Type Theory has to say on punctured surfaces, yet found myself at a loss to even define 'punctured torus'. This may very well be due to my inexperience with Homotopy Type Theory.

• As a needless ornament to round out this question, here is an animation of first puncturing an immersion (torus surface)$\to$ $\mathbb{R}^3$, then running through a 1-parameter indexed family of regular homotopies of said immersion, and finally mending the puncture again:

(source: adapted by myself from this German Wikpedia page, which, incidentally, wrongly calls this an 'eversion' of the torus: while eversion of a torus is possible, by utilizing one of the famous eversions of the sphere, this is not one, I think, for the crude reason that here the non-continuous operations of puncturing and un-puncturing are part of the animated gif; incidentally, someone with a Wikipedia account should perhaps correct this, if it is correct that calling this an eversion is wrong.)

1 Usually proved, needless to say, via homotopy-invariance of $\pi_1$, by simply describing, in one way or the other, a homotopy-equivalence between $S_{1,1}$ and $S^1\vee S^1$, then combining three things: homotopy-invariance of $\pi_1$, the fact that $\pi_1(S^1)\cong\mathbb{Z}$, and (a corolllary of) van Kampen's theorem. My understanding is that a suitable van Kampen theorem has already been proved in Homotopy Type Theory, and, as is widely known, two pioneers of this theory have proved that $\pi_1(S^1)$ is isomorphic to $\mathbb{Z}$.I also take it that homotopy-invariance of $\pi_1$ is not an issue at all in Homotopy Type Theory; holds by design. Also, Homotopy Type Theory already offers pushouts of spans in the category of groups, so it seems that the (hoped-for) result $\mathbb{Z}\ast\mathbb{Z}$ has been constructed in the theory, already, so somehow it seems that all what is missing is a definition of the punctured torus.

• There is no way to define "puncturing" as an operation in HoTT, since it is not a homotopy-invariant thing. And as you note, the homotopy type of the punctured torus is $S^1\vee S^1$, which has been defined and its homotopy group computed in HoTT. So I'm not sure what more one could ask for. – Mike Shulman Aug 26 '17 at 22:08
• @MikeShulman: thank you very much. Thinking about it, it indeed seems rather misguided to ask how to define an operation which changes the homotopy type in Homotopy Type Theory. If you make your comment an answer, I for one would accept it. – Peter Heinig Aug 27 '17 at 6:03
• In principle one could ask for a homotopy pushout involving the wedge of two circles resulting in a torus and see that one gets the correct analogue as in the topological model. – David Roberts Aug 27 '17 at 10:01
• @PeterHeinig That's not quite it; any nontrivial operation will change the homotopy type! What's misguided is to ask about operations that are not invariant with respect to homotopy type of the input. – Mike Shulman Aug 27 '17 at 20:51
• @DavidRoberts There is such a homotopy pushout: the description of the torus as a HIT with one point-constructor, two path-constructors, and one 2-path-constructor. The first three constructors are a wedge of two circles; the last constructor glues in the 2-cell wrapping around each of them twice that makes it a torus. I suppose, based on this example, one might consider "puncturing" as the non-operation of exhibiting a space as obtained by attaching a single cell to another space (the "punctured" one). – Mike Shulman Aug 27 '17 at 20:54