Postdoctoral Researcher
Department of Mathematics, Johns Hopkins University
Pronouns: he/him
HoTTEST Summer School 2022. Online course on homotopy type theory and formalization of mathematics in Agda. July–August 2022. Summer school website website
This summer school was organized by Carlo Angiuli, Dan Christensen, Martín Hötzel Escardó, Chris Kapulkin, Dan Licata, Emily Riehl, and myself to promote diversity within the field of Homotopy Type Theory. With over 2000 participants, it was a huge success.
I am a postdoctoral researcher in the Department of Mathematics at Johns Hopkins University in Baltimore, MD. My research focuses on the formalization of mathematics and homotopy type theory. I am the lead developer of the agda-unimath library, the largest library of formalized mathematics in the Agda proof assistant, and author of the forthcoming book, Introduction to Homotopy Type Theory (ArXiv).
I have been part of the Homotopy Type Theory community since its inception. As a member of the Univalent Foundations Program during the special year on univalent mathematics at the Institute for Advanced Study, I co-authored the book Homotopy Type Theory: Univalent Foundations of Mathematics. From 2014 to 2018 I did my PhD under Steve Awodey at Carnegie Mellon University. I have held postdoctoral positions at the University of Illinois at Urbana-Champaign with Dan Grayson and at the University of Ljubljana with Andrej Bauer. I am currently working under Emily Riehl at Johns Hopkins University.
The agda-unimath library was founded during the Univalent Foundations for Daily Applications meeting organized by Marc Bezem and Bjørn Ian Dundas in Bergen, in November 2021. The formalization for my book Introduction to Homotopy Type Theory had grown substantially., and it contained an up-to-date foundation for univalent mathematics. Therefore I suggested to also formalize the Symmetry book. Elisabeth Stenholm, Jonathan Prieto-Cubides, and Pierre Cagne joined the cause, and helped transforming the book formalization into a library that could be used effectively for other projects.
It soon became clear that we wanted the library to serve a more general purpose, containing any kind of mathematics from a univalent point of view, and that the best format was that of a formalized wiki. Thus the idea was born to have a one-concept-per-file organization, which to our knowledge was new for formalization, and have each file read like an nLab page with additional resources and links included in each page. The agda-unimath project has since grown to a project with over 400K lines of code, over 2000 pages, and over 40 contribibutors. It is the largest library of formalized mathematics of any kind in the Agda proof assistant, including the widely used standard library and the cubical agda library. I remain one of the most active contributors to the library, with over 1200 commits and 800K modifications.
However, far more important is the community that we have been growing. At the start of the agda-unimath project we also created the Univalent Agda Discord server, which hosts discussion forums for all Agda libraries, including the 1Lab, the cubical agda library, TypeTopology, and the Agda standard library. This is a diverse and welcoming community with a lively discussion and active contributors from all ages and all walks of life. You are very welcome to join too!
I am currently working as a postdoctoral researcher with Emily Riehl. With Emily, we are studying and formalizing synthetic higher categories, and I am teaching Introduction to Proofs, and undergraduate course following my friend Clive Newstead’s book Infinite Descent into Pure Mathematics.
After my postdoc in Urbana-Champaign I returned to my academic roots, the University of Ljubljana. In 2011-2012 I had already spent a year here to write my masters thesis on homotopy type theory under Andrej Bauer. Now I returned to write my book, and open up new directions of research within homotopy type theory. As a member of the Tydiform project I took a great interest in univalent combinatorics, which is an approach to combinatorics that takes advantage of the univalence axiom in order to count things up to isomorphism, and I founded the agda-unimath library there. I have advised several students on topics related to the formalization of mathematics.
I held my first postdoctoral fellowship with Dan Grayson and Charles Rezk at the University of Illinois at Urbana-Champaign. During this time I shifted my research interests towards formalization of mathematics, and started with the formalization of the lecture notes for my course Introduction to Homotopy Type Theory. I also secured a publisher for the course notes, Cambridge University Press. The formalization of these notes would later serve as the foundation of the agda-unimath library.
After completing my masters thesis in 2012 I work for one year as research assistant for Bas Spitters at the Radboud Universiteit of Nijmegen. The approach I took in my masters thesis to informal homotopy type theory had been well received, and we pursued further topics related to higher topos theory and descent. During this year, I also participated in the Univalent Foundations Program at the Institute for Advanced Study, even though I didn’t have a PhD yet. Here I participated in the writing of the HoTT book, and eventually I would end up becoming Steve Awodey’s grad student.
Carnegie Mellon University
Advisor: Steve Awodey
Thesis: Classifying Types
Thesis Committee: Steve Awodey, Jeremy Avigad, Ulrik Buchholtz, Michael Shulman
Awards: Presidential Fellowship Award, 2016
Utrecht University
Thesis: Homotopy Type Theory
Thesis Committee: Jaap van Oosten, Benno van den Berg, Andrej Bauer
Utrecht University
Thesis: Dimensional and Topological Properties of Attractors
Advisor: Karma Dajani
office: Krieger Hall 213
email: [first initial][last name][the terminal category][that symbol in every email address][first two initials of employer’s name][a punctuation symbol][abbreviation for equivariant directed univalence]