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

The feedback given by the participants can be viewed here.

Emergency contact information


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.


We will have two tracks:

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.


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.


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




Lecture material

See the UniMath/Schools Github repository.


We ask participants to arrange their own accommodation.

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.



For any questions, contact Benedikt Ahrens (email).