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?



How to proceed with a type-theoretic proof that $\Sigma \mathbb{S}^1 \simeq \mathbb{S}^2$?
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.


