# About me

My name is Guillaume Brunerie and I’m a researcher in mathematics and in computer science working mainly in *homotopy type theory*, a field combining mathematics (in particular homotopy theory, category theory, and constructive mathematics) and theoretical computer science (in particular type theory, logic, and proof assistants).

# Curriculum Vitae, papers and talks

Here is my curriculum vitae, in reverse chronological order.

## Postdoc at the IAS (2016 — 2018)

Since September 2016, I have a two-year postdoctoral membership at the Institute for Advanced Study with Vladimir Voevodsky. I am mainly working on formalizing the content of my PhD thesis in Agda, and also on developping more invariant homotopy theory (synthetic homotopy theory) in homotopy type theory.

I gave a short talk at the beginning of the year:

*Invariant homotopy theory in the univalent foundations*, Short talks by postdoctoral members, IAS School of Mathematics, Princeton, NJ, USA

## PhD at the university of Nice (2013 — 2016)

From September 2013 to August 2016, I was a PhD student at the Laboratoire J.A. Dieudonné under the supervision of Carlos Simpson. I successfully defended my thesis on June 15th 2016.

- Guillaume Brunerie.
*On the homotopy groups of spheres in homotopy type theory*(187 pages, in English except for a 20-page summary in French at the end). You can also download the slides of the oral presentation and the poster.

During this time I also wrote two articles with Dan Licata:

- Dan Licata and Guillaume Brunerie.
. Certified Programs and Proofs (CPP 2013), volume 8307 of Lecture Notes in Computer Science (LNCS), pages 1–16. Springer. doi:10.1007/978-3-319-03545-1.*π*_{n}(*S*^{n}) in Homotopy Type Theory - Dan Licata and Guillaume Brunerie.
*A Cubical Approach to Synthetic Homotopy Theory*. Logic in Computer Science (LICS 2015), pages 92–103, IEEE. doi:10.1109/LICS.2015.19.

I gave a 7-hour long mini-course on homotopy type theory :

*Théorie des types dépendants et axiome d’univalence*, in the PhD Colloquim*Inter’Actions 2015*, Grenoble, France (26th, 27th and 28th of May 2015)

And I gave 16 other talks:

*Custom definitional equalities in Agda*, in the “Univalent Foundations and Proof Assistants” session of the International Congress on Mathematical Software (ICMS 2016), Berlin, Germany (on July 14th 2016)*Examples of closed natural numbers in homotopy type theory*, at the séminaire Chocola in Lyon, France (on June 9th 2016)*The fourth homotopy group of the three-dimensional sphere*(video), at the “Workshop on Homotopy Type Theory and Univalent Foundations of Mathematics, Toronto, Canada (on May 16th 2016)*A Cubical Approach to Synthetic Homotopy Theory*, at LICS 2015, Kyoto, Japan (on July 6th 2015)*Théorie des types cubiques*, at the “Séminaire Logique et Interactions”, Marseille, France (on December 11th 2014)*The fourth homotopy group of the three-sphere*, at the Homotopy Type Theory Workshop, Oxford, United Kingdom (on November 9th 2014)*Cubical homotopy type theory*, at the Agda Implementors’ Meeting XX, Tallinn, Estonia (on October 21st 2014)*Homotopy type theory*, at the conference “Homotopical Algebra, Operads and Grothendieck-Teichmüller groups”, Nice, France (on September 10th 2014)*Cubical homotopy type theory*, in the conference “Formalization of mathematics in proof assistant” during a thematic trimester on “Semantics of proofs and certified mathematics” at the Institut Henri Poincaré, Paris, France (on May 6th 2014)*Cubical homotopy type theory*, at the conference “Recent developements in Type Theory”, Lyon, France (on January 17th)*Homotopy Type Theory*, at the conference “Journées francophones des languages applicatifs”, Fréjus, France (on January 10th 2014)*Introduction à la théorie des types homotopiques*, in the working group “Algèbre supérieure”, Nice, France (on October 28th, December 2nd and December 9th 2013)*A type-theoretic definition of weak infinity-groupoids*, at the “Stockholm Logic Seminar”, Stockholm, Sweden (on October 23rd 2013)*Homotopy type theory and homotopy groups of spheres*, at the “Séminaire Chocola”, Lyon, France (on October 17th 2013)*The Hopf Fibration*, at the “Conference on Type Theory, Homotopy Theory and Univalent Foundations”, Barcelona, Spain (on September 23rd 2013)*What is missing for Agda to be suitable for Univalent Foundations?*, at the “Agda Implementors’ Meeting XVIII”, Gothenburg, Sweden (on September 16th 2013)

## Studies at the ENS Ulm (2009 — 2013)

From September 2009 to August 2013, I was a student in the Département de Mathématiques et Applications of the École Normale Supérieure de la rue d’Ulm.

### Special year at the IAS (2012 — 2013)

From September 2012 to June 2013, a special year on the univalent foundations of mathematics, was coorganized at the Institute for Advanced Study by Steve Awodey, Thierry Coquand and Vladimir Voevodsky. Thanks to the organizers of the special year and to the ENS, I was able to participate for the full year.

During that year, I gave 9 talks:

*An elementary definition of weak ∞-groupoids*, in the session “Progress in Higher Categories” of the CMS Summer Meeting, Halifax, Nova-Scotia, Canada (on June 5th 2013)*A type-theoretic definition of weak ∞-groupoids*, in the session “Univalent Foundations” of the ASL North American Annual Meeting, Waterloo, Ontario, Canada (on May 9th 2013)*Homotopy Theory in Type Theory*(video), with Dan Licata and Peter Lumsdaine, at the seminar of the Institute for Advanced Study, Princeton, New Jersey, USA (on April 11th 2013)*The James construction and*(video), at the seminar of the special year of the IAS, Princeton, New Jersey, USA (on March 27th 2013)*π*_{4}(*S*^{3})(video), at the seminar of the special year of the IAS, Princeton, New Jersey, USA (on February 20th 2013)*π*_{2}(*S*^{2}) in HoTT*Weak infinity-groupoids, part II*, at the seminar of the special year of the IAS, Princeton, New Jersey, USA (on February 1st 2013)*Weak infinity-groupoids, part I*(video), at the seminar of the special year of the IAS, Princeton, New Jersey, USA (on January 30th 2013), at the seminar of the special year of the IAS, Princeton, New Jersey, USA (on November 16th 2012)*π*_{k}(*S*^{n}) for*k*<*n**Higher inductive types*, tutorial of the special year of the IAS, Princeton, New Jersey, USA (on October 15th 2012)

Before the special year at the IAS, I gave 4 sequences of talks in Paris:

*Théorie des types homotopiques, fondations univalentes et types inductifs supérieurs*, mini course in the “Séminaire d’Analyse Algébrique”, Paris, France (on May 15th and May 16th 2012)*Introduction à la théorie des types homotopiques, fondations univalentes des mathématiques*, in the working group “Algèbre et topologie homotopiques”, Paris, France (on April 4th and April 11th 2012)*Théorie des types homotopiques*, in the “groupe de travail d’élèves de logique de l’ENS”, Paris, France (on January 19th and January 26th 2012)*Introduction à la théorie des types homotopiques*, in the working group “Catégories supérieures, polygraphes et homotopie”, Paris, France (on September 30th, October 7th and October 14th 2011)

## Studies at the lycée Louis-le-Grand (2007 — 2009)

From September 2007 to June 2009, I was a student in classes préparatoires (MPSI and MP*) at the lycée Louis-le-Grand. I did my TIPE on the relation between the complement of the trefoil knot in *S*^{3} and the space of unitary lattices of ℝ^{2}:

*Structure topologique de l’espace des réseaux unitaires*, rapport de TIPE

And I gave a talk on Gödel’s completeness theorem:

*Le théorème de complétude de Gödel*, in the “Séminaire de mathématiques des élèves du lycée Louis le Grand”, Paris, France (on February 4th 2009)

# Other interests

I’m also interested in programming and free software, and I have some experience with various programming languages like OCaml, Javascript, C, Lua, Python, shell scripting. Some of my projects are available on my page on GitHub.