How to proceed with a type-theoretic proof that $\Sigma \mathbb{S}^1 \simeq \mathbb{S}^2$?

Question

The circle in homotopy type theory $\mathbb{S}^1$ is a higher inductive type freely generated by the following constructors: $\mathsf{b} : \mathbb{S}^1$ and $\mathsf{loop} : \mathsf{b} = \mathsf{b}$.

The sphere $\mathbb{S}^2$ is freely generated by the following constructors $\mathsf{b'} : \mathbb{S}^2$ and $\mathsf{surf} : \mathsf{refl_{b'}} = \mathsf{refl_{b'}}$.

We could also define the sphere as the suspension of the circle i.e. $\Sigma \mathbb{S}^1$. I want to show that these two definitions of the sphere, define the same shape up to homotopy i.e. $\Sigma \mathbb{S}^1 = \mathbb{S}^2$ .

I plan to do this by univalence, specifically by defining two quasi-inverse functions $f : \Sigma \mathbb{S}^1 \rightarrow \mathbb{S}^2$ and $g : \mathbb{S}^2 \rightarrow \Sigma \mathbb{S}^1$.

First I have to construct the functions using the recursor on their respective types. I will first define $f$ using recursion on $\Sigma \mathbb{S}^1$, in order to do this I need to map $\mathsf{N} : \Sigma \mathbb{S}^1$ to some point in $\mathbb{S}^2$ and I have to do the same with $\mathsf{S}$. Finally I have to define a function $m : \mathbb{S}^1 \rightarrow (f(\mathsf{N}) = _{\mathbb{S}^2} f(\mathsf{S}))$.

Let's start with the simple definitions first: \begin{equation} f(\mathsf{N}) := \mathsf{b'} \end{equation} \begin{equation} f(\mathsf{S}) := \mathsf{b'} \end{equation}

We then have to define $m : \mathbb{S}^1 \rightarrow (\mathsf{b'} =_{\mathbb{S}^2} \mathsf{b'})$, we define it by circle recursion such that: \begin{equation} m(\mathsf{b}) := \mathsf{refl_{b'}} \end{equation} \begin{equation} \mathsf{ap}_m(\mathsf{loop}) := \mathsf{surf} \end{equation} Since we require $\mathsf{ap}_m(\mathsf{loop}) : \mathsf{refl_{b'}} = \mathsf{refl_{b'}}$ and $\mathsf{surf}$ has exactly this type.

We have now defined all the data require to have a function $f : \Sigma \mathbb{S}^1 \rightarrow \mathbb{S}^2$.

Where I get stuck is in defining $g$. What I've tried is the following definition by sphere recursion: \begin{equation} g(\mathsf{b'}) := \mathsf{N} \end{equation} but then I need a path of the type $\mathsf{refl_{N}} = \mathsf{refl_{N}}$ and I have no idea how to define a non-trivial path of this type. I can get a non-trivial two-dimensional path like this $\mathsf{ap}_{\mathsf{merid}}(\mathsf{loop}) : \mathsf{merid}(\mathsf{b}) =_{\mathsf{N} =_{\Sigma \mathbb{S}^1} \mathsf{S}} \mathsf{merid(b)}$ but I have really no idea, how to turn this path into a path of the type $\mathsf{refl_{N}} = \mathsf{refl_{N}}$. I guess I could use path induction but that seems it would be inelegant and tedious.

So I have two questions: 1) Is the $f$ I've defined a good way to prove that $\Sigma \mathbb{S}^1 \simeq \mathbb{S}^2$ via the approach I've outlined above? 2) If so how I define $f$'s quasi-inverse $g$ in the most elegant way?

Answer 1

I'm not sure if it is the most elegant way, but it is certainly the most direct. So, we need to define the image of $\mathrm {surf}$ as an element of $refl_{\mathrm N} = refl_{\mathrm N}$. We proceed as follows. Let $p \equiv m(\mathrm b) : \mathrm N = \mathrm S$. Consider the inverse path $p^{-1}$. We have a proof (via path induction) that $\psi: p^{-1} \circ p = refl_{\mathrm N}$. We define $g(\mathrm {surf}) \equiv \psi \circ \mathrm{transport}_{p^{-1}} (\mathrm{surf}) \circ \psi^{-1}$. Here $\mathrm{transport}_{p^{-1}}$ maps $p=p$ to $p^{-1} \circ p = p^{-1} \circ p$. Thus by sphere recursion $g$ is defined.

It is a bit more tricky to construct the homotopies. As usual, we define them by higher induction. They are trivial to define on points and paths. I denote the corresponding homotopy by $h : g\circ f = \mathrm{id}_{\Sigma S^1}$. We define $h(\mathrm N) \equiv refl_{\mathrm N}$, $h(\mathrm S) = p^{-1}$. We also choose $h(p) \equiv \psi$ (note that the types are correct). Now we need to construct a 2-path lying over $p^{-1}$ and $\psi$ between $m(\mathrm {loop})$ and $g \circ f( m(\mathrm {loop}) )$. Note that by definition $g \circ f( m(\mathrm {loop}) )$ is constructed from $m(\mathrm {loop})$ by transport along $p^{-1}$ and $\psi$ (for loops transport by paths and conjugation by paths is the same) and an element is always connected to its transport by any path by a path lying over it (by definition 6.2.2, essentially). Thus $h$ is constructed.

To construct $t: f\circ g = \mathrm{id}_{S^2}$ we define $t(\mathrm b^{\prime}) \equiv refl_{b^\prime}$ and $t(refl_{b^\prime}) \equiv refl_{refl_{b^\prime}}$. To construct a 2-path between $\mathrm{surf}$ and $f\circ g(\mathrm{surf})$, note that $\mathrm{surf} \equiv f(m(\mathrm{loop}))$ and that we have a correctly defined 2-path between $g(\mathrm{surf})$ and $m(\mathrm{loop})$ by construction as above. We define the required 2-path by application of $f$. It is easy to check that its type is indeed correct.

Q.E.D.