π n (S n ) in Homotopy Type Theory. - Daniel R. Licata; Guillaume Brunerie (CPP, 2013)

A Cubical Approach to Synthetic Homotopy Theory. - Daniel R. Licata; Guillaume Brunerie (LICS, 2015)

On the homotopy groups of spheres in homotopy type theory. - Guillaume Brunerie (CoRR, 2016)

The James Construction and π4(S3) in Homotopy Type Theory. - Guillaume Brunerie (J. Autom. Reason., 2019)

Syntax and models of Cartesian cubical type theory. - Carlo Angiuli; Guillaume Brunerie; Thierry Coquand; Robert Harper 001; Kuen-Bang Hou (Favonia); Daniel R. Licata (Math. Struct. Comput. Sci., 2021)

Synthetic Integral Cohomology in Cubical Agda. - Guillaume Brunerie; Axel Ljungström; Anders Mörtberg (CSL, 2022)