coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] School on Univalent Mathematics, Minneapolis (MN, USA), July 29-Aug 2, 2024

From: Favonia <kbh AT umn.edu>
To: agda AT lists.chalmers.se, coq-club AT inria.fr, univalent-mathematics AT googlegroups.com, Homotopy Type Theory <homotopytypetheory AT googlegroups.com>, types-announce AT lists.seas.upenn.edu, ProofTheory AT lists.bath.ac.uk, categories AT mq.edu.au
Cc: Benedikt Ahrens <benedikt.ahrens AT gmail.com>, Benedikt Ahrens <B.Ahrens AT cs.bham.ac.uk>
Subject: [Coq-Club] School on Univalent Mathematics, Minneapolis (MN, USA), July 29-Aug 2, 2024
Date: Mon, 22 Apr 2024 10:06:31 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kbh AT umn.edu; spf=Pass smtp.mailfrom=kbh AT umn.edu; spf=Pass smtp.helo=postmaster AT mta-p7.oit.umn.edu
Dkim-filter: OpenDKIM Filter v2.11.0 mta-p7.oit.umn.edu 4VNTB63N1Bz9vLGp
Dmarc-filter: OpenDMARC Filter v1.3.2 mta-p7.oit.umn.edu 4VNTB63N1Bz9vLGp
Ironport-data: A9a23:33Plsaj+uUcrKumfhb2GIa1GX161oRQKZh0ujC45NGQN5FlHY01je htvX2GFaanbZGqnfdsnatjgpkIBvJ7dzN5rS1FvrXxgEypjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqieUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYqdDpLg06/gEk35qiq5GlC5gVWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGUn4dBrY8wfZME2wJ7 ONGCSICcg7SrrfjqF67YrEEasULKdXieZtA/HZh0XfECPBgTJzeK0nIzYYDgHFg2oYXTKiYP ZJGAdZsREyojxlnOV0XII87mqGlimSXnzhw+A/J/vJpvTa7IApZzqr/NuTPJZu2VOZop2Sht E/b1WX4HURPXDCY4WPUqyr03YcjhxjTU4ULUba86/RCm0yW3mVVCRsMVFL9r+PRt6Klc9dDI gkMpWwprLR06UmtCNTxQnVUvUJooDZCZPFrKMkB+Dqfx+3N/Fi4FGcYUG9oPYlOWNANeRQm0 VqAntXMDDNpsaGIRX/1yltyhW/tUcTyBTJbDRLoXTc4D8/fTJbfZy8jo/5mDKfwloKzHjDsh S2Pqm4zi6h7YS83O0eTogqvb9GE/8ahousJCuP/AjrNAuRRONTNWmBQwQKHhcus1a7AJrV7g FAKmtKF8McFBoyXmSqGTY0lRe7wvKneb2WN2AA0RvHNEghBHVb/Iui8BxkjfC9U3josIlcFn WeI41MItcU70IWCMPItC25ONyja5fGxTIy9DZg4n/JTZJlveRWc/T1/LUmel2Xslk4hiqYjM P+mnTWEUB4n5VBc5GPuHY81iOd1rghnnDO7bc6hk3yPj+HEDFbLEuhtDbd7RrtkhE9yiF6Jq Ik32grj40k3bdASlQGHrNZMdQxWcChT6FKfg5U/S9Nv6zFOQAkJY8I9C5t8E2C8t/ULzLX77 TumV1VGyVHyo3TCJE/YIjpgcb7jF9I3534yISVmbx7i1mkBcLSfyv4VV6I2Wr07q81l7/p/F Mced+u6X/9gdzXg+hYmV6fbkrBMThqQqDi1D3KXWwRnJ59EbC7Vy+DgZTrqpXUvDDLolM4Qo I+A9wL8QLhaTTs+EfTpUquOzkywj1cZiuldT0vFGfgNWUTOoaxBCT39se8zGO4IcS78/zq90 x2HJysYqc3mgZ4HwPOQiY+q946WQvZDRGxEFGzl3JOKHCj9/Fv757RfUeyNLAvvZEmt9IqMP exqnuzBatsZl1N3sq15IbZh7YQ6w/DN/7Z67ABVLE/nXmSRKIFLAye5hJFUl6h32LVmlxO8W RuP9vlkKLy5Ap7ZP2BLFjU1TNao9K8yoSbT38QXMU+hxS5Q/Zi7a2twESSIqhRgKOpSDNt47 8Yn4NUb+i6uuCoMa9ymtB1Zx06ID34HUpgkiK0kPZ/WulIr5G1vMZ34IQ3q0a6LcORJYxULI CfLpa/shIZ850vlclgvGVfgweFxjokE4hQS6Fk8O16Ix973psI2+DZz8j0HaBtf4Tsa8uB0O 0ltb1ZUI4fX9RhWpcFzZUKeMCAfOw+85Wrw1EovqG3Va2KKR179BjQxFsjV9X9I7l8GWCZQ+ Y+p7VrMUBHoTZnX5TQzU0s0kM7TZ4V92SOakf/2AvnfOYcxZAfkpaqcZWAojR/DKuFpjW3lo dhaxspBWZfZBwUx/ZJiU5K70I4OQi+qPGZBGPFt3J0YFFHmJQ2d52K8FFCTSOhsedrx7k6KO +5/LJluVjO/9hq0gBI1OKouG4JwzdkVvIcsW7WzPmMXkaqtnhwwurLqyyXOrmsKQdJvrMUDF r3sZw+ySlK3u38FtFLO/e9lO3W5a+YqfAfT/v6428RXGoMhsNNDS1AT0Ly1s0rMLS9iwRGYh yLYRqrs1+c5459dr4jtNaRiBguPNtL4UtqTwj2zq9hjadDuM9/EkgEo9mncIAVdOIUOV+RNl biitMD92GXHtu0UV1/1toagFa4Tw+mPR8tSb9zKKUdFkRu4WMPD5wUJ/0a6I8drlPJf/syWe BuqWvCvdNI6W8Zv+1MNUnJwSy0iMqXQarvsgQifrP7WUxgU7lHhHeOdrHTsaTlWSz8MN5jAE TTLgveJ5O1DjYFyFRQBVuBHAZh5HQfZYpEYVebN7BuWMmr5pWm5mOrSpUJ1o3WDQHyJC93z7 p/5VwDzPkb68r3ByNZC9Zd+pFsLBXJ6mvM9ZV8Z58UwsT2hEWoaNq4IBP3q0H2PfvDaj/kUp Q0hbVfOzQ34QT0BaUq659X/GBqaAKoDNsqRyvkB4RaPcynvbG+fKOIJy8uiyy4elvjfICWPN NQYvHD8I3BdB7l3EP0L6KXTbfhPn5vnK7Fhxaw5u9H3BVATDahiOLmN2uZSfXSvLvwhX3kn6 YT4qa6oja17pYPM/R5cRkNo
Ironport-hdrordr: A9a23:RdG6T6MFYCygjcBcTgujsMiBIKoaSvp037Dk7TEPdfU1SL3nqy jN9M506faQslYssJBMo7+90ca7MAjhHPJOkPEs1NSZLXDbUQmTXftfBOLZqlWKdkGeygc379 YcT0ERMqyNMXFKyen9+xexCNstzZ2q96qylf7Cw3oFd3AJV0ii1XYdNu9YKDwUeOCLP+tfKH NU3Lsi1lydkKssBPiGOg==
Ironport-phdr: A9a23:s3XPIx3D8MyD2bt5smDO9gwyDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaOo6w93RSZBs3y0LFttan/i+PaZSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNZwhEniexbLB2I Rm5rgjcuNQdjJd/JKo21hbGrXxEdvhMy29vOVydgQv36N2q/J5k/SRQuvYh+NBFXK7nYak2T qFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4 qx2RhLklDsLOjgk+2zMlMd+kLxUrw6gpxxnwo7bfoeVNOZlfqjAed8WXHdNUtpNWyBEBI6za JYBD/caPeZAsYbyu0cOoxW5BQmpHuzvyzlIjWLy0aA11+ktFAfL1xEiEd0TqnTZtNr6OqccX +620afG0yvOYO9N1Dfh9ITFaAwtre2QUb9yd8fa1EkhFxnCjlWVsYHrPyma1voKs2id7upvT /+khmkkqw5qojii3dosiozPho4P1F/L6Dh5zZ8zKNalR0F1fcSqH4FMtyGGKYR2WMUiTnlnt Ss+xLMLp5C1cDQUxJopyBDSaf6KfpSI7x/jVOicPCt1iG5mdb6hhRu/8kitxvHyWMe0zFpHr ShIn9jDuH0N0RHY98aJSvx4/ki72DaP0Rje6u5FIUAolarbNoUuzqQxlpoUqUjDECj2mF/zj K+NbEkk9eyo5Pr/brXpp5+cK490ihzlPag0hsO/BuE4Pw4TVGaY4eSxzKDv8EP2TblQjfA7n bPVvI3eKMkavKK1HRNZ34Q75xqhEzur1M4UkHoHIV5fZh6Lk4vkN0vTLP38CfqyhUmnnSlvx /DbJb3hHovCLmLenrfgfLdy9VZRxBY1wNtC/ZxbEKsBL+j2WkLptNzXEBs5MwuszubiFNVyz JoSWXqND6ODN6PSsEOI6vgyI+mJYo8ZoijyJOU45/L2jH85n0ESfbWx0JcKZn21Ee5qLkaWb Hb2n9sMFWYHshAgQOD2ilCOSTtTaGyzX6I46DE7EoWmDYLbS4Cum7OB3Dy2HoBTZmBAEFyDD 2rnd5icV/cKcy2dOtVhnSAcVbi9V48h0gmjuBLix7p9MuXU4jEYtY7k1NVt++LTkggy+SVoA MSZzmGCVHp5nngIRj8zxKBwu1ZxylaF0ahigvxXD8Zf5/1TUlRyCZmJxuN2Avj2WxndZZGCS F+iR9i8GncqQ5Z5yNgXJk15Bt+KjxbZ3iPsDaVR36GNBYI99q/awz30Ltp9xnPPyKgqlHEpR cxAMWCpnKli7xOVDInM1w25kKOtaaMEzWbx5X+OhVaOsUZCQUYkUaLAWmwYflrKvMz0+kPPS KW/IbsgNQRFxMGYLbZScZviilAQAL//KczTeCe4nWG3GBCDy5uIbZH2YCMG0SzGTlUcngYVu 3uKKEx2Pj2mpGziDDFpD0PHZ0L37fI4onqnTgk9xEeXbAkp3LOp9xESn/2RUNsWx/QJtDpno ignMky62of4AsSHoQtoNPFfa9MV/VJBk2/VqloubdSbM6l+iwtGIExMtET02kAyV9woeakCq XoryFE3MqeEyBZacCve25nsO7rRI220/Ra1aqeQ1EuNmM2O9PIp7/I1407moBnvDlArpnZt0 /FI1n3a65nXX0IJSZykak8s7FBhoq3CJCw05ofaz3ppZKq+shff3tRvCec4mV67Z9kKCKqfD 0fpFtECQcijLOt/g1+ychcNJ/xf7oYxI8rjb6TA36+3evtlmnSrgXkvDJlV9EWK+mI8T+fJ2 81A2PSExk6cUC+6il69s8fxkIQCZDcIH2P5xzK2TIhWLrZ/e4oGEwLMa4W+28l+ipjxWnVZ6 E/rBlUI39WscAaTaFq11BNZ1EAeq3iq0SWiyDk8nzYsp6uZlCvApoaqPBkNOkZWQW8kgFvxY MC1g90cQEm0fl0xjhL2rU3+xqVduOF+NzyKGhsOL3SwdjA8FPHo6ennAYYH8p4jvCRJXf7pZ FmbTuW4uB4Gy2b4GHMYwjkndjass5G/nhpgiWvbImwgyRiRMcx22xrb48TRAPBL2T9TDipyi RHKA176MtW0t4bch9LYv+ayWnj0HJ5ZcQH2yIXGuSemrz4PY1X3j7W4ndvpFhI/2Cnw2oxxV CnGmx37Z5Hiy6WwNe8PklBAPFbn8II6H4h/ltB1n5QMwT0BgY3T+3MbkGD1ONEd2KTkbXNLS yRZi9LS5QHk3gVkIBfrj8r6XHW1385nIdS2fysa1zk84MZDFKqPpOUfwW0l/hzh/FyXO6Ai1 j4GgeMj8nsbn/0EtEI2wyORD6pTeCsQdS3gmhKU7syv+aBeZWKha7+1hwJ1mdGsCq3HoxkJA S2lPMd+W3YhsIMlaA2ftR+7opvpc9TRc98J4xidkhObyvNQNIp0jf0SwyxuJWP6u3Qhje89l x1nm5+g7+3lYy1g+ry0BhlAO3j7fcQWr3vuh6Z2g8OQmY2jA98yUiVOR5buQf+yRXgRv/TPK gOIVjAwtz3IfNiXVR/a40BgoXXVFpmtPHzCP3gVw+JpQxyFLVBeigQZD30q24Q0HQewyIn9Y V90s3oPs0XgpEIGmYcKf1HvF33SrwCyZnIoRYiDeVBIuxpa6R6dMNTCvLsoQ2cIotv4/VLLc z3BIF4XaANBEk2cWwK6ZOnovIGZtbHHV6zndKWGYK3S+7UPB7HSmc/pg9cgpmvWcZ7XWxsqR /wjhhgcATYjQ5yfwm9JEXZL0HiSJ8+D+EXlpXMx9Zn5qai2HliyucOOE+cAaIQ/vUnu3OHab KjIw3wlTFQQnpIUmS2XlP5FhAVU0nEzMWP1TfwBrXKfFfOB3PQPSURANmUpbJcA7rpgjFMVZ IiB0Iuzj+4hyKRuVjInHRTggp37P5RXZTvnbBWeWhfNbu/YbWrCx8W9CU+lYYVZl/4c9xi5u DLAVlTmIizGjD7xERamLeBLiiifeh1YooC0NBh3WyDvS9fvaxvzN9ES73V+2bovmnbDLnIRK xB5b0oItuLW6iJExOh6HSpM4mctIeSfmimf5vXVMd5P6qctUngyzrMEpi5ilPNc90QmDLRtl THXr8Jyrl3uieSJxjd9EVJPpjtNmIOXrBBiNKHepdFLXXfJ+g5I7H3FUk9W4Ys5TIS+5eYKk oec8cC7YC1P+N/V48YGUs3dKcbcdWEkLQKsAznMSg0MUT+sM2jbwU1bivCbsHOP/f1Y4tDhn oQDTrhDWRk7DPQfXw5mFtwqPZJxGD4ojPTI6axArWr7txTXSMhA69rfUemOBPz0NDuDpbxYb l4QnvX/LJhVK4j9nUFudxMp+eaCU1qVVtdLrCp7awYyq0gY63lyQFo43Ef9Yx+s6nseRrak2 wQ7gQxkbaEx5S/hth0pc0HSqnJ6wyxT0Z31xCqceznrIOKsUJFKXmDq4lMpPMqzQh4pP1Tpw Qo0aHGdFuwX1uo6Mjo07W2U8ZpXRawFF/0COUdJg6jINrNxigoUqz37lxYWta2fVcYkxVdsK MP26CkYvmArJN8tef6PeOwTlgAW3/jI5HX0kbpuiA4GexRUrz3UI3dO4RBVcON7e2Kp5rA+s F3S3WIbJS5VDLxy5ag2kyF1c+WYk3C/j/gZchv3brzCafnB5yDBjZLaGwJhkBhQ0RMeoP4si ZtrclLIBRp3kf3LTUxPbJqbb1sOMq8wvDDSZXrc672Qh8gvZ8PkSLGuF7TQ/PEdhkbudO7IN 4EQ54EZQd+r0V2eMMLharMJ1Ed0jOwEDEiACrJEdA/ZyV/vRumiyZkx0IVAdGl1PA==
Ironport-sdr: 66267d22_LYTJ1Av4SKdXRwcO8Fpf+nF5+4bQeVmoZHSOMlDRzX4WWpr u9lWhdXRvnPpWWI17WcEOjfLNSgMEQQNIoQhYjw==

We are pleased to announce the

School on Univalent Mathematics 2024

to be held at the University of Minnesota (Twin Cities),
Minneapolis, MN, United States, July 29-August 2, 2024
(https://unimath.github.io/minneapolis2024)

If you are interested, please fill out the application form
(https://forms.gle/9PTB2V19hVuJsidz8). We will start the reviewing
on *May 6, 2024* and accept applicants on a rolling basis.

Overview
========
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.

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.

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 (https://github.com/UniMath/UniMath).

This is our first school in the United States in the hope that students
in North America can participate more easily.

Format
=======
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.

Prerequisites
==========
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.

Application and funding
=======================
Please fill out the form (https://forms.gle/9PTB2V19hVuJsidz8).
For information on how to participate, please visit
https://unimath.github.io/minneapolis2024

Best regards,
The organizers Benedikt Ahrens and Favonia

[Coq-Club] School on Univalent Mathematics, Minneapolis (MN, USA), July 29-Aug 2, 2024, Favonia, 04/22/2024