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

Lecture material

The introductory material

Notice that the following files reflect the state of affairs during the school, for later updates see the relevant workshop repository of UniMath.

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

During the school/workshop, the participants will be working either individually or in small groups, mentored by experienced UniMath developers. The problems will be designed to be of practical importance in the development of the UniMath library as well as of pedagogical value to participants.

Location

The school/workshop takes place at the University of Birmingham, UK. The address is Learning Centre, Birmingham B15 2FG, UK. The map below indicates the walking path from the nearby train station 'University' to the Learning Center.

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.

Mailing lists and other means of communication

Schedule

The following is a rough schedule, to be refined in the near future. Important: Wednesday afternoon is off. Also, the lab session on Friday afternoon should be considered optional, so participants can travel home after lunch. The schedule is also available as a Google calender.
Sunday, 10 December
16:00-19:00 UniMath install party (see below for info)
Monday, 11 December
11:00-11:30 Coffee break
12:30-14:00 Lunch
14:00-15:00 Lecture 1: Spartan Martin-Löf Type Theory (Andrej Bauer)
15:30-16:30 Lecture 2: Fundamentals of Coq (Anders Mörtberg)
17:15-18:00 Complete semi-Segal types (Nicolai Kraus)
Tuesday, 12 December
10:00-11:00 Lecture 3: Univalent Foundations (Martin Escardo)
11:00-11:30 Coffee break
11:30-12:30 Lecture 4: Tactics in UniMath (Ralph Matthes)
12:30-14:00 Lunch
14:00-17:00 Lab session (incl. coffee break)
17:15-18:00 The simplicial set model of type theory (Joseph Helfer)
Wednesday, 13 December
10:00-12:30 Lab session (incl. coffee break)
12:30-14:00 Lunch
Afternoon free time
Thursday, 14 December
10:00-11:00 Lecture 5: Set-level mathematics (Joseph Helfer)
11:00-11:30 Coffee break
11:30-12:30 Lecture 6: Category theory (Peter Lumsdaine)
12:30-14:00 Lunch
14:00-17:00 Lab session (incl. coffee break)
17:15-18:00 How to implement type theory in one hour (Andrej Bauer)
19:00- Dinner at Pasta di Piazza (Google map, Set menu)
Friday, 15 December
10:00-11:00 Lecture 7: UniMath - its origins, present, and future (Benedikt Ahrens)
11:00-11:30 Coffee break
11:30-12:30 Lecture 8: Presentation of the project work
12:30-14:00 Lunch
14:00-17:00 Lab session (incl. coffee break)

UniMath install party

The UniMath install party aims to help those participants who experience difficulties installing UniMath on their laptops. It takes place on Sunday, 10 December, from 16:00 to 19:00, in the Sloman Lounge of the School of Computer Science - opposite of the Learning Centre (see section "Location").

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

Accommodation

We ask participants to arrange their own accommodation. Below we give some information and list a few hotels - you might use a search engine or hotel booking website to find others.

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:

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

You can prepare for the school by studying some of the material listed below.

Installing UniMath

Please install UniMath on your laptop before coming to Birmingham. To this end, read the installation instructions. In case of problems or questions, contact the UniMath mailing list. You can also attend the UniMath install party on Sunday afternoon for help with the installation - see Section "Schedule" for more information.

Tourism

See the dedicated tourism website.

Organisers

For any questions, contact Benedikt Ahrens (email) or Chris Kapulkin (email).

Sponsors