<div dir="ltr">We are pleased to announce the<br><br>School on Univalent Mathematics 2022,<br><br>to be held at the Palazzone di Cortona<br>(<a href="https://urldefense.com/v3/__https://www.sns.it/en/palazzone-di-cortona__;!!IBzWLUs!Gmye0y5Af6orRF47PSIIOEv58vLAxiLhrVEeg9zDMeByR4F0imZNRKbJPuKQ0BMMGa4AWedtjZgw9A$">https://www.sns.it/en/palazzone-di-cortona</a>),<br>Cortona, Italy, July 17-23, 2022<br>(<a href="https://urldefense.com/v3/__https://unimath.github.io/cortona2022/__;!!IBzWLUs!Gmye0y5Af6orRF47PSIIOEv58vLAxiLhrVEeg9zDMeByR4F0imZNRKbJPuKQ0BMMGa4AWefqhSsZrA$">https://unimath.github.io/cortona2022/</a>)<br><br>Overview<br>========<br>Homotopy 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.<br><br>The UniMath library is a large repository of computer-checked mathematics, developed from the univalent viewpoint. It is based on the computer proof assistant Coq.<br><br>In this school, we aim to introduce newcomers to the ideas of Univalent Foundations and mathematics therein, and to the formalization of mathematics in UniMath (<a href="https://urldefense.com/v3/__https://github.com/UniMath/UniMath__;!!IBzWLUs!Gmye0y5Af6orRF47PSIIOEv58vLAxiLhrVEeg9zDMeByR4F0imZNRKbJPuKQ0BMMGa4AWecr1ktJyQ$">https://github.com/UniMath/UniMath</a>), a library of Univalent Mathematics based on the Coq proof assistant.<br><br>Format<br>=======<br>Participants will receive an introduction to Univalent Foundations and to mathematics in those foundations. In the accompanying problem sessions, they will formalize pieces of univalent mathematics in the UniMath library.<br><br>Prerequisites<br>==========<br>Participants should be interested in mathematics and the use of computers for mathematical reasoning. Participants do not need to have prior knowledge of logic, Coq, or Univalent Foundations.<br><br>Application and funding<br>=======================<br>For information on how to participate, please visit <a href="https://urldefense.com/v3/__https://unimath.github.io/cortona2022__;!!IBzWLUs!Gmye0y5Af6orRF47PSIIOEv58vLAxiLhrVEeg9zDMeByR4F0imZNRKbJPuKQ0BMMGa4AWeeKwNMTyA$">https://unimath.github.io/cortona2022</a>.<br>The application deadline is 15 April 2022.<br><br>Best regards,<br>The organizers Benedikt Ahrens and Marco Maggesi<br><div><br></div></div>