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

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: $$$$f(\mathsf{N}) := \mathsf{b'}$$$$ $$$$f(\mathsf{S}) := \mathsf{b'}$$$$

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: $$$$m(\mathsf{b}) := \mathsf{refl_{b'}}$$$$ $$$$\mathsf{ap}_m(\mathsf{loop}) := \mathsf{surf}$$$$ 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: $$$$g(\mathsf{b'}) := \mathsf{N}$$$$ 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?

• I'm a bit confused about what your definition of $\Sigma S^1$ is. I would have expected it to be generated by one point, one 1-loop, and two 2-paths trivializing the 1-loop. But you seem to have two points. Could you clarify your notation a little? – Noah Snyder Feb 17 '15 at 20:29
• @NoahSnyder The suspension of a type $T$ is defined as the higher inductive type $\Sigma T$ generated by two point constructors $\mathrm{N} : \Sigma T$ and $\mathrm{S} : \Sigma T$ and one 1-path constructor $\mathrm{merid} : T \to \mathrm{N} = \mathrm{S}$. This is the definition 11Kilobytes is using. – Ptharien's Flame Feb 18 '15 at 23:03

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.