## Open problems ## * Similarly to the torus, consider the projective plane, Klein bottle, ... as discussed in the book (sec 6.6). Show that the Klein bottle is not orientable. (This requires defining "orientable".) * What is the [[loop space of a wedge of circles]] indexed by a set without decidable equality? * Calculate more [[homotopy groups of spheres]]. * Show that the [[homotopy groups of spheres]] are all finitely generated, and are finite with the same exceptions as classically. * Define the Toda bracket. * Prove that $n$-spheres are $\infty$-truncated. * Prove that $S^2$ is not an $n$-type. * Define the/a delooping of $S^3$. * Can we verify [computational algebraic topology](http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo/) using HoTT? * Bott periodicity * Develop synthetic stable homotopy theory ## Closed Problems ## * Prove that the [[torus]] (with the HIT definition involving a 2-dimensional path) is equivalent to a product of two circles. See Sojakova's proof: [[torus.pdf:file]]. A shorter formalized proof is [here](http://homotopytypetheory.org/2015/01/20/ts1s1-cubically/) * Construct the [[Hopf fibration]]. (Lumsdaine gave the construction in 2012 and Brunerie proved it was correct in 2013.) * Construct the "super [[Hopf fibration]]" (AKA [[nlab:quaternionic Hopf fibration]]) $S^3 \to S^7 \to S^4$. (Buchholtz and Rijke solved this early 2016 through a [homotopy version of the Cayley-Dickson construction](https://arxiv.org/abs/1610.01134).) * Prove the [[Seifert-van Kampen theorem]]. (Shulman did it in 2013.) * Construct [[Eilenberg-MacLane spaces]] and use them to define cohomology. (Licata and Finster did it in 2013, written up in [this paper](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) (pdf).) * Define the [[Whitehead product]]. Guillaume Brunerie did this in 2017, written up in [this paper](https://arxiv.org/abs/1710.10307). he also gives a constructive proof of $\pi_4( S^3)= Z/n Z$ for some $n$ and a construction of the [[James construction]] ([reduced James product](https://ncatlab.org/nlab/show/EHP+spectral+sequence#via_the_james_model)) as a HIT and a homotopy colimit. It is also proven that $\Omega \Sigma X \simeq J(X)$ for some pointed connected type $X$. ## Useful constructions ## * [[Homotopy pushout]] $Y \sqcup^X Z$ * [[Join]] * [[Suspension]] * [[Homotopy fiber]] * [[Smash product]] * [[James construction]] $J(X) \simeq \Omega \Sigma X$ * [[Hopf construction]] * [[Localization]] * [[Whitehead product]]