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

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

  • Bus: It is called '28X' and its stop is found by following the Ground Transportation' signs. You have to pay $2.75 in cash when you enter the bus and there is no change. If you want to the Shadyside Inn, you should get off the 28X about one hour into the bus ride at the crossing of Fifth Avenue and South Aiken Avenue. If you need to take another bus, you will have to pay $2.75 again on entering.
  • The 'Ground Transportation' signs also lead you to taxis, ubers and lyfts. Uber and lyft work well in Pittsburgh. You need a smartphone to use the latter two.
  • A more convenient way which is likely to be cheaper than uber/lyft/taxis is the 'Super Shuttle'. There is a counter for it in the terminal and it is payable by credit card. It means a big car will drive you and others directly to your destinations in pittsburgh. You might have to wait a bit, maybe even a long time. You do not need a smartphone or app to use it.

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:

  • At the university center, at least the Schatz Dining Hall (google-maps) is open during the lunch breaks.
  • There are noodle and rice bowls at iNoodle (google-maps). Best ask a local how to get there.
  • In the university center, you can buy snacks at a shop called entropy.

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:

  • The Phipps Conservatory is very close to campus, just in Shenley Park (the Park behind Baker Hall). It costs around $17 and you can relax watching lots of exotic plants.
  • On the other side of campus, you can walk down Forbes to get to the Carnegie Museum of Natural History.
  • Shenley Park looks a bit like it is supposed to be enjoyed from the inside of a car when you enter it coming from campus, but if you go further in, there are some trails you can use for a walk.
  • If you want a longer walk and a bigger Park, you can go through Squirrel Hill to Frick Park.


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.

Date: 2018-11-13 Tue 00:00

Author: Felix Wellen

Created: 2019-03-18 Mon 12:47