Week 1, June 4 – 10, 2017, Homotopy Type Theory

Organizers:
J. Daniel Christensen (University of Western Ontario)
Chris Kapulkin (University of Western Ontario)
Daniel R. Licata (Wesleyan University)
Emily Riehl (Johns Hopkins University)
Michael Shulman (University of San Diego)

The Mathematics Research Community workshop on Homotopy Type Theory will take place from June 4 - 10, 2017 in Snowbird, Utah.

The goal of this workshop is to bring together advanced graduate students and postdocs having some background in one (or more) areas such as algebraic topology, category theory, mathematical logic, or computer science, with the goal of learning how these areas come together in homotopy type theory, and working together to prove new results. Basic knowledge of just one of these areas will be sufficient to be a successful participant.

At the workshop, in addition to mentors and some participants sharing background knowledge about their areas of expertise, the participants will devote substantial time to working together on a variety of interesting problems in synthetic and abstract homotopy theory and higher category theory, as well as mathematical logic, theoretical computer science, and formalization of mathematics.

Topics

Sample topics that participants may work on include:

1. Synthetic homotopy theory
   • Importing techniques from classical homotopy theory, such as spectral sequences, Toda brackets, localization and completion at a prime, etc.
   • Importing results from classical homotopy theory, such as the finite-generation of the homotopy groups of spheres, the universal coefficient theorems and the Hurewicz theorem.
   • Developing the synthetic theory of (infinity,1)-categories.
2. Formalization of mathematics
   Some possible topics for computer formalization of mathematics include:
   • 2-category theory.
   • Algebraic curves.
   • Constructive real analysis.
   • Synthetic homotopy theory, including known but not-yet-formalized results and also new results obtained in topic 1.
3. Categorical and higher categorical semantics
   • Higher-categorical semantics of univalent type theory, including hoped-for equivalences between certain homotopy type theories and certain classes of (infinity,1)-categories.
   • Semantics of extensions to type theory, such as resizing rules, strict equality, and cofibrations.
   • Homotopy theory of cubical sets and relation to cubical type theory.
   • New category-theoretic definitions (e.g. elementary higher toposes) to match known type-theoretic structures.

Background reading

All participants will be expected to study Chapters 1–3 of the Homotopy Type Theory book and encouraged to look at Chapters 6 and 7 as well. Here are some additional readings depending on what topic(s) you are interested in working on (though it is certainly not necessary to have mastered all of this material before the workshop!).

1. For those interested in formalization, we suggest in addition:
   • Licata-Shulman, Calculating the fundamental group of the circle in homotopy type theory, arXiv:1301.3443.
   • Ahrens-Kapulkin-Shulman, Univalent categories and the Rezk completion
   • Avigad-Kapulkin-Lumsdaine, Homotopy limits in type theory
   • Chapters 10 and 11 of the Homotopy Type Theory book
   • Bauer-Gross-Lumsdaine-Shulman-Sozeau-Spitters, Formalizing homotopy type theory in Coq [forthcoming]
2. For those interested in working on synthetic homotopy theory, we suggest:
   • Chapter 8 of the Homotopy Type Theory book
   • Licata-Finster, Eilenberg-MacLane Spaces in Homotopy Type Theory
   • Cavallo, Synthetic Cohomology in Homotopy Type Theory
   • Brunerie, On the homotopy groups of spheres in homotopy type theory, arXiv:1606.05916
   • Licata-Brunerie, A Cubical Approach to Synthetic Homotopy Theory
   • Hou-Finster-Licata-Lumsdaine, A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
3. For those interested in working on homotopy-theoretic semantics of type theory and higher-categorical aspects of the theory, we suggest:
   • Shulman, Univalence for inverse diagrams and homotopy canonicity, arXiv:1203.3253.
   • Kapulkin-Lumsdaine, The Simplicial Model of Univalent Foundations (after Voevodsky), arXiv:1211.2851.
   • Shulman, The univalence axiom for elegant Reedy presheaves, arXiv:1307.6248.
   • Bezem-Coquand-Huber, A model of type theory in cubical sets, TYPES 2013.
   • Kapulkin, Locally cartesian closed quasicategories from type theory, arXiv:1507.02648.
   • Shulman, Univalence for inverse EI diagrams, arXiv:1508.02410.
   • Lumsdaine-Warren, The local universes model: an overlooked coherence construction for dependent type theories, arXiv:1411.1736

Preliminary schedule

Monday morning will begin with a few introductory lectures. Monday afternoon will continue with workshops introducing both computer proof assistants and informal reasoning in Homotopy Type Theory.

On Tuesday through Friday, the bulk of time will be spent working on research problems in small groups. Sometime on Wednesday all participants will reconvene to report progress, and have an opportunity to switch problems if desired.

On Friday each working group will give a short presentation. Then all participants will convene to discuss future research directions and plans to stay in touch.

Details to follow!

Mentors

J. Daniel Christensen is a Professor in the Department of Mathematics at the University of Western Ontario. He obtained his PhD from MIT in 1997 in the area of homotopy theory, did postdoctoral work at Johns Hopkins University and the IAS, and is currently working on projects in homotopy theory, homotopy type theory, representation theory and geometry.

Chris Kapulkin is a Postdoctoral Fellow in the Department of Mathematics at the University of Western Ontario. He obtained his PhD from the University of Pittsburgh in 2014 under the supervision of Thomas C. Hales. His work focuses on Homotopy Type Theory and its connections and applications to other areas, especially higher category theory.

Dan Licata is an Assistant Professor in the Department of Mathematics and Computer Science at Wesleyan University. He obtained his PhD in computer science from Carnegie Mellon University in 2011 under the supervision of Robert Harper. His work in homotopy type theory has focused on the development and formalization of synthetic homotopy theory, and on new type theories inspired by higher categorical/homotopy-theoretic semantics, such as cubical, adjoint, and directed type theories.

Emily Riehl is an Assistant Professor in the Department of Mathematics at Johns Hopkins University. She obtained her PhD from the University of Chicago in 2011 under Peter May and then was a Benjamin Peirce and NSF Postdoctoral Fellow at Harvard University. She works on a variety of topics in category theory related to homotopy theory, including, in particular, a project using 2-categorical techniques to produce a "synthetic" development of the theory of infinite-dimensional categories.

Michael Shulman is an Assistant Professor in the Department of Mathematics at the University of San Diego. He obtained his PhD from the University of Chicago in 2009 under Peter May, in the area of category theory and its applications to fields such as algebraic topology. His work in homotopy type theory focuses on synthetic homotopy theory and higher-categorical semantics.

Registration

Full information and how to apply can be found here.

Contact Information

Here is a list of individuals who participated in this conference:

Further web info for 2017 participants.

Top of Page