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?

  • $\begingroup$ 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? $\endgroup$ – Noah Snyder Feb 17 '15 at 20:29
  • 3
    $\begingroup$ @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. $\endgroup$ – 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.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.