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?