coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ulrik Buchholtz <ulrikbuchholtz AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] HoTTEST Summer School July+August 2022
- Date: Thu, 28 Apr 2022 21:34:05 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ulrikbuchholtz AT gmail.com; spf=Pass smtp.mailfrom=ulrikbuchholtz AT gmail.com; spf=None smtp.helo=postmaster AT mail-pj1-f47.google.com
- Ironport-data: A9a23:0X10wa5f3eeLuz0PRVlZuQxRtArBchMFZxGqfqrLsTDasY5as4F+v jYeWD3TMqzYZGenco90bonk8BgEuJODyIQ3GwBkrSlmZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOK6UoYoAwgpLeNeYH5JZSlLxqho2+aEvfDjW1nX4 Y+o85WFULOY82cc3lw8u/rrRCxH56yaVAMw5jTSstgW1LN2vyB94KM3fcldHVOgKmVnNrLSq 9L48V2M1jixEyHBpT+Suu2TnkUiGtY+NOUV45Zcc/DKbhNq/kTe3kunXRYRQR8/ttmHozx+4 MtBvK6KWFgCBY7VvcY9TUhoDxNfOJQTrdcrIVDn2SCS50jPcn+p2/c3SU9qYssX/eF4BWwI/ vsdQNwPRkrb1qTmnfThE7cq2ptLwMrDZOvzvll9ySvYDvw7SpDDRKHW9/dX2T4xgoZFGvO2i 88xMmE/ME6dPkIn1lE/FqkCltyqtFLFLjR3t16I+5BuznTZ01kkuFTqGIONJobiqd9utk2fv yfN+3nzKgoLMcSWjzuD6HOlwOHV9R4XQ6oXHby8s+Zo2RidmjNVBxoRWl+25/K+jyZSRu6zN WQK9iMcl7lt33eIV/zffwPpkGK2nxslDo84//IB1CmBza/d4gC8D2cCTyJcZNFOiCPQbWx6v rNut4O5bQGDoIF5WlrGqejJ9WLa1Tw9aD5dNXVdHGPp9vG6+Nlr5i8jWOqPB0JcszEYMTT5w jTPtCpnwrtP0ogE0KK0+V2BiDWpznQocuLXzlWJNo5GxlkhDGJAW2BOwQaAhRqnBNjDJmRtR FBex6CjABkmVPlhbhClTuQXB62O7P2YKjDailMHN8B/qm30oyfyIt8Kum4WyKJV3iAsKW+Bj Kj76VM52XOvFCbCgVJfONLqVZV2k8AM6/y8DquOMIAmjmdNmP+vpXkyPyZ8Lkjil08jlaxXB HtoWZfEMJruMow+lGDeb75Fj9cDn3lirUuOG82T50n4idK2OS/NIZ9YYQDmRr1ovMus/l+Jm /4BbJDi40sEAIXDjtz/q9F7waYidihlW/gbaqV/Koa+H+aRMDx/W6KJneN9KuSIXc19z4/1w 510YWcAoHKXuJENAVzihqlLZOy9UJBhg2g8OCBwb1+k12JyM4mq5aYbMZAweOB/puBkyPd1S dgDetmBUqwfEGSZp2xFYMmvtpFmeTSqmRmKYHiobT05SJhqGF7E99riSQ3w+XRcFSGwr8Y// +at21qDE5oOTghvFujMb/erww/jtHQRgrMgUE7BI90Vc0LpqdA4Jyv0h/4xAscNNRSTnmvAh 1jKWU8V/LCfrZU0/d/FgbG/g72oS+YuTFBHG2T77KqtMXaI82emx7hGWrnacD3YUlTy5/z+N +hYyvfLMMoHkkxPhIxyHus51qk5/dbu++ZXwwk4TnXGa1OnVuFpLnWch5Ids6RMwvpBu1LzV B7QvNZdPrqNNYXuF1tIfFgpaeGK1Pc1nDjO7KRqfB+runcvpLfXA19POxSsiTBGKOcnOo0Sx +p86tUd7Bayi0Z3P9va3DpY8X+Aci4JX6k97MpIBYbqjk8zyAgHb8CDTCDx556LZpNHNUxze m2Yg6/LhrJ9wEvecipsSSKcg7IF3Zle6gpXyFIiJkiSnoaXjPEA2hAMoy88SR5Yz0ka3u9+U oSx25aZ+UlTE/ZUaMl/s6SEHghAAFiB+BW0xQdW0mLeSEasWyrGK2hV1SNhOqwG2zo0Q9SZ1 OjwJKXZvfLCc8T43y90UklgwxAmZcIk7RXMwahLAOzcd6TXolPZbmuGam8Bqh+hCsQ07KECS S+G484oAZDG2eUsT2HXxmVUOXn8iPxJGYCafcxcwQ==
- Ironport-hdrordr: A9a23:hsRvn6qQ8L3l+7TRyb5hDiEaV5omeYIsimQD101hICG9E/bo8P xG+c5w6faaskdzZJhNo7C90cq7IE80l6QFg7X5VI3KNGLbUQCTXeRfBOXZslnd8u7FmtK1F5 0MT0GzMrLN5JFB4/rH3A==
- Ironport-phdr: A9a23:6+q6RBS3148Mpv63hd15xCVl5tpsohWVAWYlg6HPa5pwe6iut67vI FbYra00ygOTBsOCtLkd0Lue8/i5HzBau9DZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHG t9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oI xi6swvcutMLjYZgJao91xXEr39VcOhS2W9kOEifkhni6suu5pJv7zhct/c8/MNcTKv2eLg1Q 6ZFBzo8KWA148PrtRjHTQSR43YXT3sbnBlVDQXb9R/2Rpj+vDf0uep7wymaINb5TasoVjS47 qdkUwHnhSEaPDMk6m7Xi8hwjKVGoBK9ohF03oDZbJ2JOPd4Y6jQe84RS2hcUcZLTyFODYOyY YUMAeQcI+hXs5LwqEESoRakHwSgGP/jxz1Oi3Tr3aM6yeMhEQTe0QMuG9IOqnXUrNboP6oPT OC60KnIzTXEb/NSxTf86ZXDfxc8ofGIR7JwcMnRxlIyFwzZjlWQqYvlPzeJ1uUMqGWb4O9gW viui24jsQ1+vj+vxsI1h4TPm4kaxUzK+z9jz4YpOd23VlR7Ydi8HZZMqyyWKYV4T988T2xqp io21KMLtIC7ciQU1Jkq2QPTZ+KFfoWK7R/uVumfLDl3in55eL+ymha//0e9x+DiWMe51ktBo CRCktnJrH8N1hrT59CaSvpz+UetwyqA2BrL5u5ZIEA0jrbUK5k7wrEtjJYTvkvDEynrk0v1l K+bblso9vSs5uj9YbjrpoWQO5Fphgz/KKgjlc6yDOIlOQYURWeb4/6z1Lj78E35XrpKivo2n 7HcsJ/AJMQbore1AxdX0oo+8hq/ATir3dYCkXkIK1JFfx2Hj4z3NF3UPP/4CvK/j0ytkDdt2 f/GIqXsDovRInXHirvsfrZw51RCxAYuzN1T/Z1ZB7MZLPL2QEDxtdjYDhEjMwyzxubqEMh91 ocEWWKOAa+WK77SvkOI5uIvJOmMYJMVuTfmJvgq4v7hl345mVsHcaa12psXbWi0HvJ9LEqBe 3rjns8BEXsWvgo5VOHmlUWOUSRPaHaqQ6I8+jY7BZq6AofEX4ChmaCO3COmHpJNfW1GEVCNE XLwd4qeQfsMaSSSItVgkjMeT7ShRZUhhlmSs1rxzKMiJe7J8AUZs4ji3Z57/b79jxY3oAFwF cWem0uQRGF0mWcUVXdiwaRloE9311yD0a98n+5wGtla5vcPWQA/Y82Ph9dmAsz/D1qSNuyCT 0yrF43O6VAZS9swx4VLeENhA5C4iRuF2SO2ArgTnrjNBZou86ua0WKib91lxSPg068sx0IjX tMJLXev07N77QnQDZPCk0Wek7q4XasZ1S/JsmyEyDnGp1lWBTZ5Sr6NRnUDfg3TpNX96FnFS uqzDa4mMQFcws6CLa9WePXmiFxHQLHoP9GNK3mplTKWAhCFjqiJcJKse2gZ23DFD1MYlgkI4 XucHQ03ByPku2CHSTIyShTgZETj9eQ4o3S+JqMt5yeNaUApl7+8+xpPwOeZV+tWxLUP/iEot zRzGl+5mdPQEduJ4QR7Lu1aZpsm7VFL2Hi81UQ1N4G8L61kml8Vchhm90Lo2RJtD4xckM8s5 Ho0xQt2IKic3RtPbTSdlZz3P7TWLCH18nXNI+bL3kvf09yL8acP7/AkuX3suQioEgwp9HAmm 9hZ3n2A54nbWRIIWMGUMA5//Bx7qrfGJyglstmMhDs8bO/u62GEh416YYltggytdNpeLq6eQ Qr7EslAQtOrNPRvgV+iKBQNIOFV8qcwecKgbfqPnqCxb4MC1Hqri3pK5Idl3weC7S15H6TV2 4wEwPuF1QuHUDPgnn+ut8n2ncZPYjRYTQ/dgWD0QZVcYKF/Z9NBFGO0Is69295+h5npR2xw+ 1uqBldA08isM0n3DRS1zUhb0kIZpmaikC2zwmlvkj0nmaGY2TTH3+XocBdv1ndjfGB5lh+sJ IG1i4pfR020d00zkxDj40/mxq9draA5Lm/JQE4OcTKkZ21lV6KxsPKFbastoNs1tT9WU+6ha lCaTbrhsTMV1iriGy1VwzVzezyxu5r/lgB3kyrHdCc1/CefI5gug0uArNXHIJwZliILXix5l SXaChCnMt+l8M/V35bPv+aiVn6wA5hacC3l14SF52Ow4WxnBwH6nujmwIW2V1hnl3WiiZ82C natzl60eITg2qWkPPgye0BpAAW58M9mAsRklYB2gpgM2H8cj5HT/HwdkG61P88IvMC2JHcLW zMPxMbYpQb/30g2ZG+N3YP6XGiWwstmY8WoSmwT0yM5qctNDe3Hid4M1TswuVe+oQ/LNLJgm i0cyvEz434ahOUVqiIiyyycBvYZGkwSbkmO31yYqtu5qqtQfmOmd7O9gVF/kd6WB7aHughAW Xz9d8RqDWpq4854Kl6JzGzr59SuZozLddxK/E7x8V+In61PJZk2jPZPmSd3JTe3oyg+0+Bix R12gcPh4c7eej0rpv7mREYfbGG9ZttPqG+xy/wFxYDPgdjpRtI4S1BpFNPpVa76TmxU7Ky9c V7ISHpm8j+aAeaNQ1HZshs36SKXVcjsbSnfJWFFn4o4AkDBYhUO2kZMG2xq+/xxXgGymJ6+L AEgvG1Xvhig7UISguNwa0umCjeZ/Vj3LGdyEN/FdVJX9l0QvhiOd5XPsqQrWXkfp8PEzkTFK 3THNV4QXCdZBwrdXQClZv73upHB67TKXLPgaaaeJ+zf86oGEK7ZjZO3jtk8pmjKbJ7eeCI4S aV8gxsmPzgxDc3dn39npzU/sSXLYobboR69/ncytcWj6LHxXwmp44KTCrxUONEp+hasgK7FO fTCzCB+YS1V0J8B3xqqgPAWwUIShidydjKsDaVItCjDS7jVk7NWCBhTYj16Nc9B5aYxlgdXP suThtTw379+xvk7bjUNHUTmgd2sbNcWLnuVMVrGAAOTNu3DK2GUhc7wZqy4RPtbi+AV/xy8t DCHElPyazSOkz66MnLneepIjSydIFlfoNTnKkcrWTWlFou4LEHkY7oVxXUszLY5h23HLzsZO Dl4KQZWq6GIqDlfibN5EnBA6XxsKa+FnTyY5q/WMMVz07MjDyJqmuZd+Hl/xaFS6XQOWfhvm SjYs9Vuo1aijvunxT9uUR4IoTFOztHu3w0qKeDC+59MVGyRtgoK9nmVAg8WqsFND9Tuv+VIy IGKmv6sbjhF9N3Q8I0XAM2ee6fleDIxdBHuHjDTFg4MSzWmYHrei0Jqm/aX7nSJr5I+p/AEe bILQ75fEUQ3T7YUVhsjE9sFL5N6GDgjlOzD5CbnzXW7pRjVAs5du8KePhp3KfrqITedy7JDY klQqY4=
- Ironport-sdr: GAKb+sAoleH0wjcQfcaEoeGemihNeF8NnEU+9QOsMWRk33x0hpjwSGEeKroKOqJldJiOkjnrwt 6vwSth/F8kf+OnnfZJKnuIqxBCF9eHpvNqwXHWxzOFy6T5LR0uA2q3KiNTo27t6orAVmPi+N4T N6CNAwZ3BExgR7s6igY1lyLuITRrDzeNmglUo8BETbvHzUf8G1h7MiFGVCGeJKi4fciQdyVQra ka/6NoKaxGNe1S58d/Q+G3TljrmwiyCdBWUyABWgbHSYkBex4C9812jljxZD99vF6eDZnA3Dr5 8NVpgCGJB7KsL0EvmUzasQsy
We're delighted to announce the HoTTEST Summer School, part of the
Homotopy Type Theory Electronic Seminar Talks, which will take
place online everywhere in the world during the months of July and
August 2022.
The school will run both synchronously and asynchronously. The lectures
will be delivered live (between 2:30-4pm UTC) and paired with various
tutorial sessions run by teaching assistants. The course will also
feature a discord-based all-hours Q&A and an online archive of all
course materials so that participants can follow along on their own
schedule.
This school is for everyone and anyone with some familiarity with
abstract mathematics or theoretical computer science and an itching to
learn about homotopy type theory. Our goal is to make homotopy type
theory accessible to, and inclusive of, everyone who is interested,
regardless of cultural background, age, ability, formal education,
ethnicity, gender identity, or _expression_. We believe HoTT is for
everyone, and are committed to fostering a kind, inclusive environment.
The first part of the course will include parallel introductions to
homotopy type theory and formalization given by Ulrik Buchholtz, Martín
Hötzel Escardó, Dan Licata, Anders Mörtberg, Paige North, Emily Riehl,
and Egbert Rijke. The summer school will then close with a series of
colloquia introducing more advanced topics and exciting areas for
further study delivered by Pierre Cagne, Favonia, Jonas Frey, Jon
Sterling, and Chaitanya Leena Subramaniam. A team of teaching
assistants which includes Elisabeth Bonnevier, Tom de Jong, Jarl G.
Taxerås Flaten, Artem Gureev, Perry Hart, Astra Kolomatskaia, Amélia
Liao, Jacob Neumann, Johannes Schipp von Branitz, and Christopher
Stough-Brown among others, will lead problem sessions and assist
students with exercises.
A central aim of the summer school is to build community among all of
the participants, irrespective of geography. To further this, we will
hold some online social events (e.g. game nights) for the summer school
staff and participants.
More details about the course logistics and the scientific program will
be announced soon on the summer school website:
https://uwo.ca/math/faculty/kapulkin/seminars/hottest_summer_school_2022.html
In the meanwhile, we invite everyone to join us on the summer school
Discord group to hang out and get to know one another:
https://discord.gg/tkhJ9zCGs9
If you would like to participate in some background surveys that will
shape the design of the curriculum, please register for the Discord by
May 15th, but students are also welcome to join in at any time.
Please also forward to students at your institution.
On behalf of the organizers,
Carlo Angiuli, Dan Christensen, Martín Hötzel Escardó, Chris Kapulkin,
Dan Licata, Emily Riehl, Egbert Rijke
Homotopy Type Theory Electronic Seminar Talks, which will take
place online everywhere in the world during the months of July and
August 2022.
The school will run both synchronously and asynchronously. The lectures
will be delivered live (between 2:30-4pm UTC) and paired with various
tutorial sessions run by teaching assistants. The course will also
feature a discord-based all-hours Q&A and an online archive of all
course materials so that participants can follow along on their own
schedule.
This school is for everyone and anyone with some familiarity with
abstract mathematics or theoretical computer science and an itching to
learn about homotopy type theory. Our goal is to make homotopy type
theory accessible to, and inclusive of, everyone who is interested,
regardless of cultural background, age, ability, formal education,
ethnicity, gender identity, or _expression_. We believe HoTT is for
everyone, and are committed to fostering a kind, inclusive environment.
The first part of the course will include parallel introductions to
homotopy type theory and formalization given by Ulrik Buchholtz, Martín
Hötzel Escardó, Dan Licata, Anders Mörtberg, Paige North, Emily Riehl,
and Egbert Rijke. The summer school will then close with a series of
colloquia introducing more advanced topics and exciting areas for
further study delivered by Pierre Cagne, Favonia, Jonas Frey, Jon
Sterling, and Chaitanya Leena Subramaniam. A team of teaching
assistants which includes Elisabeth Bonnevier, Tom de Jong, Jarl G.
Taxerås Flaten, Artem Gureev, Perry Hart, Astra Kolomatskaia, Amélia
Liao, Jacob Neumann, Johannes Schipp von Branitz, and Christopher
Stough-Brown among others, will lead problem sessions and assist
students with exercises.
A central aim of the summer school is to build community among all of
the participants, irrespective of geography. To further this, we will
hold some online social events (e.g. game nights) for the summer school
staff and participants.
More details about the course logistics and the scientific program will
be announced soon on the summer school website:
https://uwo.ca/math/faculty/kapulkin/seminars/hottest_summer_school_2022.html
In the meanwhile, we invite everyone to join us on the summer school
Discord group to hang out and get to know one another:
https://discord.gg/tkhJ9zCGs9
If you would like to participate in some background surveys that will
shape the design of the curriculum, please register for the Discord by
May 15th, but students are also welcome to join in at any time.
Please also forward to students at your institution.
On behalf of the organizers,
Carlo Angiuli, Dan Christensen, Martín Hötzel Escardó, Chris Kapulkin,
Dan Licata, Emily Riehl, Egbert Rijke
- [Coq-Club] HoTTEST Summer School July+August 2022, Ulrik Buchholtz, 04/28/2022
Archive powered by MHonArc 2.6.19+.