Paper: [The James construction and $\pi_4(S^3)$ in homotopy type theory](https://arxiv.org/abs/1710.10307)