School and Workshop on Univalent Mathematics

sponsored by the John Templeton Foundation

December 11-15, 2017, Birmingham, United Kingdom.


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.


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.

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.





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