27 citations · 28 across the 2 of their papers we have counts for
2 papers
cs.LO2017★ 1 cited
The James construction and in homotopy type theory
Guillaume Brunerie
In the first part of this paper we present a formalization in Agda of the James construction in homotopy type theory. We include several fragments of code to show what the Agda cod…
math.AT2016★ 27 cited
On the homotopy groups of spheres in homotopy type theory
Guillaume Brunerie
The goal of this thesis is to prove that in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. W…