natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
In classical algebraic topology we have four Hopf fibrations (of spheres):
These can be constructed in homotopy type theory as part of a more general construction:
An H-space structure on a pointed type $A$ gives a fibration over $\Sigma A$ via the Hopf construction. This fibration can be written classically as: $A \to A\ast A \to \Sigma A$ where $A\ast A$ is the join of $A$ and $A$. This is all done in the HoTT book. Note that $\Sigma A$ can be written as a homotopy pushout $\Sigma A \coloneqq \mathbf 1 \sqcup^A \mathbf 1$, and there is a lemma in the HoTT book allowing you to construct a fibration on a pushout (the equivalence $A \to A$ needed is simply the multiplication from the H-space $\mu(a,-)$).
Thus the problem of constructing a Hopf fibration reduces to finding a H-space structure on the spheres: the $S^1$, $S^3$ and $S^7$.
The space $S^0=\mathbf 2(\equiv Bool)$ is not connected so we cannot perform the construction from the book on it. However it is very easy to construct a family $S^1 \to \mathcal{U}$ with fiber $Bool$ by induction on $S^1$. (Note: loop maps to $ua(neg)$ where $neg$ is the equivalence of negation and $ua$ is the univalence axiom.
For $S^1$ Peter Lumsdaine gave the construction in 2012 and Guillaume Brunerie proved it was correct in 2013. By induction on the circle we can define the multiplication: $\mu(base)\equiv id_{S^1}$, and $ap_\mu(loop)\equiv funext(h)$ where $h : (x : S^1) \to (x = x)$ is also defined by circle induction: $h(base) = loop$ and $ap_h(loop) = refl$. $funext$ denotes functional extensionality.
For $S^3$ Buchholtz-Rijke 16 solved this through a homotopy theoretic version of the Cayley-Dickson construction. This has been formalised in Lean.
For $S^7$ this is still an open problem.
It is still an open problem to show that these are the only spheres to have a H-space structure. This would be done by showing these are the only spheres with Hopf invariant $1$ which has been defined in Brunerie 2016
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Guillaume Brunerie, On the homotopy groups of spheres in homotopy type theory $[$arxiv:1606.05916$]$
Ulrik Buchholtz, Egbert Rijke, The Cayley-Dickson Construction in Homotopy Type Theory (arXiv:1610.01134)
Last revised on June 15, 2022 at 16:55:16. See the history of this page for a list of all contributions to it.