School and Workshop on Univalent Mathematics

sponsored by the John Templeton Foundation and the Ramsay fund

December 11-15, 2017, University of Birmingham, United Kingdom

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 +33 6 52 25 77 87 or by email.

Lecture material

The introductory material

• Slides on Spartan Type Theory and link to the Github repository
• Exercises on Spartan Type Theory (.pdf)
• Exercises on Spartan Type Theory (.v)
• Solutions to exercises on Spartan Type Theory (.v)
• Fundamentals of Coq (.v file)
• Fundamentals of Coq - Exercises (.v file)
• Fundamentals of Coq - Solutions (.v file)
• Lecture including exercises on univalent foundations (.pdf)
• Tactics in UniMath (long version) (.v) - Dec 13
• Tactics in UniMath (.v) - Dec 13
• Tactics (long) (.pdf) - Dec 13
• Tactics (.pdf) - Dec 13
• Tactics in UniMath (long version) (.html) - Dec 13
• Tactics in UniMath (.html) - Dec 13
• Exercises on tactics (.v)
• Exercises on tactics, with solutions (.v)
• Exercises on equivalences (.v)
• Lecture on set-level mathematics (.pdf)
• Exercises on set-level mathematics (.v)
• Solutions to exercises on set-level mathematics (.v)
• Exercises on category theory (.v)
• Solutions to exercises on category theory (.v)
• UniMath - its origins, present, and future (.v)

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

Location

Internet access

Mailing lists and other means of communication

• To contact the organizers with any inquiries, you can use unimath-bham2017-orga@googlegroups.com
• For discussion with other participants of the school, you can sign up to the UniMath 2017 Café mailing list. To sign up, send an email to unimath-bham2017-cafe+subscribe@googlegroups.com
• You can also discuss on a Slack server (thanks to Bram Geron!).

Schedule

UniMath install party

Application and funding

To apply for the workshop, please fill out the application form. The deadline to apply is October 15, 2017. Decisions will be made by the end of October.

Financial support is available to cover participants' travel and lodging expenses. Please indicate your funding needs in the application form.

Information for funded participants: Please collect your receipts for flight tickets, rail tickets, hotel bill, etc. Also keep your boarding passes. You will need to provide them for reimbursement of your costs.

Mentors

• Benedikt Ahrens (University of Birmingham)
• Andrej Bauer (University of Ljubljana)
• Martín Escardó (University of Birmingham)
• Daniel Grayson (University of Illinois Urbana-Champaign)
• Joseph Helfer (Stanford University)
• Kuen-Bang Hou (Favonia) (Institute for Advanced Study, Princeton)
• Chris Kapulkin (University of Western Ontario)
• Peter Lumsdaine (Stockholm University)
• Ralph Matthes (CNRS, University Toulouse)
• Anders Mörtberg (Carnegie Mellon University and University of Gothenburg)
• Vladimir Voevodsky (Institute for Advanced Study, Princeton)
• Matthew Weaver (Princeton University)

Accommodation

The school/workshop takes place at the University of Birmingham, located at Edgbaston, Birmingham. We recommend choosing accommodation in the city centre of Birmingham, and taking the train to University. The area around the University campus accommodates mostly students and might, accordingly, be less calm or well-maintained than desired. We advise against booking accommodation there.

The New Street train station is in the newly renovated Grand Central, which besides the station features many restaurants and shops, and which is not run-down as one might expect a train station to be. Birmingham city centre is lively and features many restaurants. You can start your search using this Google Maps search link. We have personal experience only with the following hotel:

• Premier Inn Birmingham City Centre New St Station: directly next to New Street train station, not very beautiful but modern and functional. Breakfast not included. The free wifi requires frequent re-logins, better wifi available at extra cost.

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. Be aware that there are "Anytime" (GBP 3) and "Off-Peak" (GBP 2.60) return tickets; the latter do not allow travel from New Street to University before 9:30am.

If you will 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 GBP 11.20 (compared to GBP 15 for 5 return tickets).

Buses in Birmingham give no change - if you turn up with a GBP 20 note, you'll lose it. You need exact change. The single fare is GBP 2.40 and the "day saver" is GBP 4. This gets you on any National Express bus (but not the independent companies) in the West Midlands.

Before the event

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

Tourism

Organisers

• Benedikt Ahrens
• Martín Escardó
• Achim Jung
• Chris Kapulkin
• Vladimir Voevodsky

Sponsors

• This School and Workshop was made possible through the support of a grant from the John Templeton Foundation. The opinions expressed by the organizers of this School and Workshop are those of the organizers and do not necessarily reflect the views of the John Templeton Foundation.
• The Ramsay fund by Dr Paul Ramsay and his wife Yuanbi