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).

Recordings

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
https://cmu.zoom.us/j/892135990
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.
  

Participants

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.

Acknowledgment

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