On the homotopy groups of spheres in homotopy type theory G Brunerie
arXiv preprint arXiv:1606.05916, 2016
89 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
55 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
37 2021 π n (S n ) in Homotopy Type TheoryDR Licata, G Brunerie
Certified Programs and Proofs: Third International Conference, CPP 2013 …, 2013
35 2013 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, 2018
20 2018 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
14 2022 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 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 De l’espace de Teichmüller des surfaces G Brunerie, S Bach