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

Question

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 isomorphism¹

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

been proved in Homotopy Type Theory already?

3. 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.)

¹ _{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.}