Geometry in Modal Homotopy Type Theory

Carnegie Mellon University
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.

Invited speakers

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

Preliminary schedule

All talks are in the Steinberg Auditorium, A53 in Baker Hall (google-maps).

Time Monday Tuesday Wednesday Thursday Friday
9:30-10:30 Rijke I Schreiber I Buchholtz I Schreiber II Buchholtz II
10:30-11:00 Coffee Coffee Coffee Coffee Coffee
11:00-12:00 Shulman I Myers I Finster I Rijke III Finster II
12:00-14:00 Lunch break Lunch break Lunch break Lunch break Lunch break
14:00-15:00 Arndt I Shulman II Free Arndt II Myers II
15:00-15:30 Coffee Coffee Free Coffee Coffee
15:30-16:30 Lessard Rijke II Free Frey Wellen
18:30 Dinner


Most talks were recorded and uploaded to youtube. The sound is not good, but you should be able to understand everything if you turn up the volume (internal notebook speakers might not be sufficient).
There are links to the recordings on the abstracts page.
Here is a description of how the recording and live-streaming was done.

Online Participation (outdated)

If you can't come to the workshop, it is possible to join the workshop online via zoom. This means you can view a live stream of the talks and ask questions. The url to join the meeting is
If you want to participate via zoom, it is a good idea to install the software on your computer (there is also a browser based version) and test video and audio (as far as I know, this is only possible with the installed version).
If you are not asking a question, please mute your microphone.
If you zoom in from Germany, please take note that the time difference right now is 5 hours.

Practical information

All talks will be in the Steinberg Auditorium (Room A53) in Baker Hall.
Here is some official information on how to get to the campus.
And here is a campus map.

Getting around in Pittsburgh

The bus fare is paid on entering the bus and is $2.75 if you pay in cash (there is no change). If you need to change the bus to get somewhere, you have to pay again. It is possible to get a bus card and load it using a credit card at bus stations (≠ bus stop). A bus station in Shadyside is Negley station (google-maps). You can also get a bus card from a machine at the airport. It is close to the exit where the bus '28X' leaves.

Getting from the airport to the city

Meet-up Sunday evening

I made a reservation (Felix Wellen) in a pub called "the Yard" in Shadyside (google-maps) for 6pm.

Workshop Dinner

The workshop dinner will be on Tuesday at 6:30pm (18:30) at Chengdu Gourmet (location in google maps).
The price will be below $20 without tip (it depends a bit on how many people will decide to join).
It is essentially like a buffet only that it will be served directly at your table;)
The food will be mostly traditional Chinese. There will be enough vegetarian options. If you hate spicy food, it might get a bit difficult.
Please let us know on Monday the 11th, if you want to join the dinner!

Lunch options

Since it is Spring Break at CMU, most places will be closed. Here are some exceptions:

For an overview on campus, see cmu dining locations page. You can also walk to craig street (google-maps), which has a lot of options.

Free afternoon

Wednesday afternoon will be free. Here are some recommendations what you could do:


Mathieu Anel Carnegie Mellon University
Peter Arndt University of Düsseldorf
Steve Awodey Carnegie Mellon University
Bruno Bentzen Carnegie Mellon University
Ulrik Buchholtz Technische Universität Darmstadt
Eric Finster University of Birmingham
Jonas Frey Carnegie Mellon University
Harry Gindi University of Regensburg
Jesse Han University of Pittsburgh
Joseph Helfer Stanford University
Matthew Hilty -
Joe Johnson Mary Baldwin University
Nachiket Karnick Indiana University Bloomington
Alex Kavvos Wesleyan University
Greg Langmead Carnegie Mellon University
Paul Lessard University of Colorado Boulder
David Myers John Hopkins University
Alexander Gietelink Oldenziel -
Robert Rennie University of Illinois at Urbana-Champaign
Egbert Rijke University of Illinois at Urbana-Champaign
Mitchell Riley Wesleyan University
Justin Scarfy University of British Columbia
Urs Schreiber NYU Abu Dhabi and Czech Academy of Science
Mike Shulman University of San Diego
Maxim Sokhatsky National Technical University of Ukraine
Jon Sterling Carnegie Mellon University
Zhenyu Sun Renmin University of China
Koundinya Vajjha University of Pittsburgh
Floris van Doorn Univeristy of Pittsburgh
L. S. Wang McGill University
Felix Wellen Carnegie Mellon University
Colin Zwanziger Carnegie Mellon University

More details about the topic of the workshop

While Modal HoTT is about both, monadic and comonadic modalities, most talks will be about monadic modalities. Also, it is quite likely that the majority of the talks will freely use and reason in HoTT. Details about both, HoTT and (monadic) modalities, may be found in the HoTT-Book.
Topology may be studied in a concise and natural way using what we know about homotopy types in HoTT. This is done in Mike Shulman's article Brouwer's fixed-point theorem in real-cohesive homotopy type theory. The introduction may also be helpful in understanding the general idea of applying Modal HoTT to Geometry.
Some ideas of Urs Schreiber of applying Modal HoTT are linked and explained here.

Since it is my (Felix Wellen) research topic, there is also some information on applying Modal HoTT on my personal website.


The workshop is supported by the Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053.