Carnegie Mellon University

Current Events

Past Events

2022 HoTT Retreat, Claymont

Thursday, March 10th - Sunday, March 13th

This was a research meeting between HoTT researchers at CMU and Johns Hopkins university at the Claymont retreat center, WV.

 Group photo at Claymont

2021 CMU HoTT Graduate Student Workshop

Friday, February 26th (via zoom)
This event is a gathering of graduate students, to exchange ideas related to homotopy type theory, logic, and category theory. The workshop will consist of a series of presentations, with opportunities for discussion.  This event is meant to be friendly and informal, and talks on work in progress and unfinished ideas are welcome.   For more information, please visit the workshop website or contact Jonas Frey.

International Conference and Summer School on Homotopy Type Theory

12-17 August 2019


Ulrik Buchholtz (TU Darmstadt, Germany)
Dan Licata (Wesleyan University, USA)
Andrew Pitts (University of Cambridge, UK)
Emily Riehl (Johns Hopkins University, USA)
Christian Sattler (University of Gothenburg, Sweden)
Karol Szumilo (University of Leeds, UK)


There will also be an associated Homotopy Type Theory Summer School in the preceding week, August 7th to 10th. The instructors and topics will be:

  • Cubical methods: Anders Mortberg (Carnegie Mellon University, USA)
  • Formalization in Agda: Guillaume Brunerie (Stockholm University, Sweden)
  • Formalization in Coq: Kristina Sojakova (Cornell University, USA)
  • Higher topos theory: Mathieu Anel (Carnegie Mellon University, USA)
  • Semantics of type theory: Jonas Frey (Carnegie Mellon University, USA)
  • Synthetic homotopy theory: Egbert Rijke (University of Illinois, USA)

Geometry in Modal Homotopy Type Theory

March 11-15, 2019

Homotopy Type Theory (HoTT) is one of the tools to reason within a higher topos. The recent extensions of HoTT by Modalities has led to stronger relations to the use of higher toposes in Topology, Differential Geometry and Algebraic Geometry. This workshop is about the development of Modal HoTT and its applications to Geometry.


Peter Arndt
Ulrik Buchholtz
Eric Finster
Egbert Rijke
Urs Schreiber
Mike Shulman

The Ernest Nagal Lecture 2013: Per Martin-Löf

In March 2013 Per Martin-Löf presented a series of three lectures titled Invariance Under Isomorphism and Definability:

  1. Lecture I
  2. Lecture II
  3. Lecture III

See for futher information.