School and Workshop on Univalent Mathematics

organised under the auspices of COST Action CA15123 EUTypes

April 01-05, 2019, University of Birmingham, United Kingdom

Feedback given by the participants

Emergency contact information

• For any emergency, call 999 or, equivalently, 112. The operator will route you to police, ambulance, or fire brigade as necessary.
• In less serious cases, Benedikt Ahrens can be reached on +44 7482 799962 or by email.

Overview

Univalent Type Theory is an emerging field of mathematics that studies a fruitful relationship between homotopy theory and (dependent) type theory. This relation plays a crucial role in Voevodsky's program of Univalent Foundations, a new approach to foundations of mathematics, based on ideas from homotopy theory, such as the Univalence Principle.

The UniMath library is a large repository of computer-checked mathematics, developed from the univalent viewpoint. It is freely available for everyone, as an open-source project, from the web. The workshop will give many young researchers an opportunity to familiarize themselves with the UniMath library and become contributors.

Format

• Beginners track
• Advanced track: suitable for participants with some experience in Univalent Foundations and the proof assistant Coq.

In the beginners track, you will receive an introduction to Univalent Foundations and to mathematics in those foundations, by leading experts in the field. In the accompanying problem sessions, you will formalize pieces of univalent mathematics in the UniMath library.

In the advanced track, you will work, in a small group, on formalizing a specific topic in UniMath, guided by an expert in univalent mathematics. Your code will become part of the UniMath library.

Application and funding

To participate, please fill out the application form. Some funding is available for suitable participants from institutions in COST member countries. Get in touch for more information.

Location

Transportation

The train ride from the city centre train station, called New Street, to the University station (see section Location) takes about 10 minutes, and trains run very frequently (usually from platform 12). A return ticket is GBP 3.20 if you travel to University before 9:30 ("Anytime" ticket) and GBP 2.70 if you travel to University after 9:30 ("Off-peak" ticket).

If you commute by train (e.g., from the city centre), weekly tickets are available. They are available only at a counter, not at the ticket machines, and require a photograph. A weekly ticket between New Street and University costs about GBP 12.

If you require a bus instead, see National Express West Midlands. Be aware that buses in Birmingham give no change!

Internet access

• Eduroam is available on the campus.
• If you do not have access to Eduroam, you can connect to WiFiGuest - you will need to fill out a web form to connect to the internet.

Social

• For discussion with other participants, use the UniMath Birmingham 2019 mailing list. To sign up, send an email to unimath-bham2019+subscribe@googlegroups.com.
• You can also discuss on a Slack server.

Schedule

• UniMath install party planned for the afternoon of Sunday 31 March 2019.
• School/Workshop Monday 01 April - Friday 05 April 2019.
• Wednesday afternoon is off - check the tourism website for a few pointers on what to do in and around Birmingham.

Timetable

Lecture material

Accommodation

Before the event

• Check recommended reading
• Install UniMath on your laptop

Recommended reading

• Coq in a hurry (by Yves Bertot) An introduction to vanilla Coq. It does not cover the univalent point of view, but gives a gentle introduction to Coq, the underlying proof assistant of UniMath.
• Introduction to the Coq proof-assistant for practical software verification (by Christine Paulin-Mohring) Another introduction with Coq, including screenshots. It is a bit outdated, but might still be useful.
• HoTT book Comprehensive overview of univalent foundations.
• An introduction to univalent foundations for mathematicians (by Dan Grayson) An gentle introduction to univalent foundations.

Installing UniMath

Mentors

• Benedikt Ahrens (University of Birmingham)
• Thorsten Altenkirch (University of Nottingham)
• Langston Barrett (Galois, Inc.)
• Andrej Bauer (University of Ljubljana)
• Tslil Clingman (Johns Hopkins University)
• Martín Escardó (University of Birmingham)
• Joseph Helfer (Stanford University)
• Tom de Jong (University of Birmingham)
• Marco Maggesi (University of Florence)
• Ralph Matthes (CNRS, University Toulouse)
• Anders Mörtberg (Stockholm University and Carnegie Mellon University)
• Brandon Shapiro (Cornell University)
• Niels van der Weide (Radboud University, Nijmegen)

Organisers

• Benedikt Ahrens
• Tom de Jong
• Marco Maggesi