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.
Sample topics that participants may work on include:
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!).
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!
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.
Full information and how to apply can be found here.
Further web info for 2017 participants.