About Me

I am a lecturer in computer science at the University of Birmingham. I grew up in Los Angeles, studied in Charlottesville, and presently live in Paris.

Research Interests

My main interests are higher category theory and homotopy theory, and applications of these subjects to computer science, particularly formal methods in software development and computer-assisted mathematics.

My formal training in mathematics was in homotopy theory, and I have worked extensively on the connection between this area of topology the theory of types, a discipline which goes by the name Homotopy Type Theory.

I will be teaching a course on Homotopy Type Theory at the Midlands Graduate School 2023.

Publications

1. Homotopy Type Theory: Univalent Foundations of Mathematics
   • Collaborative Book 2013 link
2. Eilenberg-MacLane Spaces in Homotopy Type Theory
   • LICS Proceedings 2014 pdf/journal
3. A Mechanization of the Blakers-Massey Theorem in Homotopy Type Theory
   • LICS Proceedings 2016 pdf/journal
4. A Type Theoretic Definition of Weak ω-Categories
   • LICS Proceedings 2017 pdf/journal
5. Goodwillie’s Calculus of Functors and Higher Topos Theory
   • Journal of Topology 2018 arXiv/journal
6. A Generalized Blakers-Massey Theorem
   • Journal of Topology 2020 arXiv/journal
7. Types are Internal oo-Groupoids
   • LICS Proceedings 2021 pdf/cmu seminar notes
8. A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory
   • Mathematical Foundations of Programming Semantics arXiv
9. A Type Theory for Strictly Unital oo-Categories
   • LICS Proceedings 2022 arXiv
10. Left-Exact Localizations of oo-Topoi I: Higher Sheaves
    • Advances in Mathematics journal

Notes, Preprints and Work in Progress

1. A Note on Left Exact Modalities in Type Theory pdf
2. A Type Theory for Strictly Associative oo-Categories arXiv
3. Synthetic Spectra via a Monadic and Comonadic Modality arXiv
4. Globular Weak oo-Categories as Models of a Type Theory arXiv
5. Left-Exact Localizations of oo-Topoi II: Grothendieck Topologies arXiv

Videos

1. Cohomology in Homotopy Type Theory ias
2. The Calculus of Opetopes ias
3. A Survey of Univalent Foundations youtube
4. A Type Theoretic View of Goodwillie Calculus part one/part two
5. Weak Structures from Strict Ones youtube
6. Higher Algebra in Computer Science youtube

Code

1. opetopic - A web-based opetope editor (temporarily down)
2. opetopic-types - A library for opetopic types and higher structures in Agda
3. catt.io - An implementation of a type theory for weak ω-categories

My Thesis

1. Stabilization of Homotopy Limits pdf
   • University of Virginia, 2010
   • Supervised by Dr. Gregory Arone