| On the homotopy groups of spheres in homotopy type theory G Brunerie arXiv preprint arXiv:1606.05916, 2016 | 93 | 2016 |
| A cubical approach to synthetic homotopy theory DR Licata, G Brunerie 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 92-103, 2015 | 54 | 2015 |
| Syntax and models of Cartesian cubical type theory C Angiuli, G Brunerie, T Coquand, R Harper, KB Hou, DR Licata Mathematical Structures in Computer Science 31 (4), 424-468, 2021 | 40 | 2021 |
| π n (S n ) in Homotopy Type Theory DR Licata, G Brunerie Certified Programs and Proofs: Third International Conference, CPP 2013 …, 2013 | 36 | 2013 |
| Synthetic integral cohomology in cubical agda G Brunerie, A Ljungström, A Mörtberg 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), 2022 | 17 | 2022 |
| Evan Cavallo, Tim Baumann, Eric Finster, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et al G Brunerie, KB Hou Homotopy type theory in Agda, 2021 | 15 | 2021 |
| Robert Harper, and Daniel R C Angiuli, G Brunerie, T Coquand, KB Hou Licata. Syntax and Models of Cartesian Cubical Type Theory. Draft available …, 2017 | 14 | 2017 |
| Hou (Favonia), K.-B C Angiuli, G Brunerie, T Coquand 13th International Workshop on Logical Frameworks and Meta-Languages: Theory …, 2019 | 13 | 2019 |
| Computer-generated proofs for the monoidal structure of the smash product G Brunerie Homotopy Type Theory Electronic Seminar Talks, 2018 | 11 | 2018 |
| The James Construction and in Homotopy Type Theory G Brunerie Journal of Automated Reasoning 63, 255-284, 2019 | 10 | 2019 |
| A cubical type theory, November 2014 DR Licata, G Brunerie URL http://dlicata. web. wesleyan. edu/pubs/lb14cubical/lb14cubes-oxford …, 2014 | 9 | 2014 |
| Robert Harper, and Daniel R. Licata. Cartesian cubical type theory C Angiuli, G Brunerie, T Coquand, KB Hou Preprint, December, 2017 | 8* | 2017 |
| A cubical infinite-dimensional type theory G Brunerie, DR Licata Talk at Oxford Workshop on Homotopy Type Theory, 2014 | 8 | 2014 |
| A formalization of the initiality conjecture in Agda G Brunerie, M de Boer, PL Lumsdaine, A Mörtberg Slides from a talk about joint work with Menno de Boer, Peter Lumsdaine, and …, 2019 | 6 | 2019 |
| Evan Cavallo, Tim Baumann, Eric Finster, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et al. Homotopy Type Theory in Agda. 2018 G Brunerie, KB Hou | 6 | |
| A cubical type theory DR Licata, G Brunerie URL: http://dlicata. web. wesleyan. edu/pubs/lb14cubical/lb14cubes-oxford …, 2014 | 4 | 2014 |
| Synthetic cohomology theory in cubical agda G Brunerie, A Ljungström, A Mörtberg URL: https://staff. math. su. se/anders. mortberg/papers/zcohomology. pdf, 2021 | 3 | 2021 |
| Initiality for martin-löf type theory G Brunerie, PL Lumsdaine Talk at the Homotopy Type Theory Electronic Seminar Talks (HOTTEST), 2020 | 3 | 2020 |
| Homotopy Type Theory: Univalent Foundations of Mathematics P Aczel, B Ahrens, T Altenkirch, S Awodey, B Barras, A Bauer, Y Bertot, ... Aucun, 2013 | 2 | 2013 |
| A Cubical Approach to Synthetic Homotopy Theory G Brunerie, DR Licata | | 2015 |
