-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Tidy up the HTML and add alternative texts to all images
- Loading branch information
Showing
1 changed file
with
65 additions
and
182 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,193 +1,76 @@ | ||
| <!DOCTYPE HTML> | ||
| <html> | ||
| <head> | ||
| <meta http-equiv="Content-type" content="text/html;charset=UTF-8" /> | ||
| <title>School on Univalent Mathematics 2024</title> | ||
| <style type="text/css"> | ||
| <head> | ||
| <meta http-equiv="Content-type" content="text/html; charset=utf-8"> | ||
| <title>School on Univalent Mathematics 2024</title> | ||
| <style type="text/css"> | ||
| body { | ||
| margin: 1em auto; | ||
| padding: 0em 1em; | ||
| max-width: 50em; | ||
| } | ||
| a {text-decoration: none; color: red; } | ||
| a:hover { background-color: yellow; } | ||
| </style> | ||
| </head> | ||
| <body> | ||
| <h1>School on Univalent Mathematics</h1> | ||
| <p>July 29 - August 02, 2024, Minneapolis, USA<br> | ||
| <em>(Install party on July 28, 2024)</em> | ||
| </p> | ||
|
|
||
| <img src="group.jpg" alt="A group photo of some participants attending the School on Univalent Mathematics" title="Group photo" width="70%"/> | ||
|
|
||
| <h2>Overview</h2> | ||
|
|
||
| <p> | ||
| Homotopy Type Theory and Univalent Mathematics are emerging fields of mathematics that study | ||
| 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. | ||
| </p> | ||
| <p> | ||
| The <a href="https://github.com/UniMath/UniMath">UniMath library</a> | ||
| is a large repository of computer-checked | ||
| mathematics, developed from the univalent viewpoint. | ||
| It is freely available for everyone, as an open-source project, | ||
| <a href="https://github.com/UniMath/UniMath">from the web</a>. | ||
| The School will | ||
| give many young researchers an opportunity to familiarize themselves | ||
| with the UniMath library and become contributors. | ||
| </p> | ||
|
|
||
|
|
||
|
|
||
| <h2>Format</h2> | ||
|
|
||
| <p> | ||
| Participants will receive an introduction to | ||
| Univalent Foundations and to Mathematics in those foundations, by leading experts in the field. | ||
| In the accompanying problem sessions, participants will formalize pieces of Univalent Mathematics in the | ||
| UniMath library. | ||
| </p> | ||
|
|
||
| <h2>Learning Materials</h2> | ||
| The learning materials for the school are located <a href="https://unimath.github.io/Schools/#school-on-univalent-mathematics-minneapolis-2024">here</a>. | ||
|
|
||
| <h2>Lecturers</h2> | ||
| <ul> | ||
| <li>Benedikt Ahrens (Delft University of Technology)</li> | ||
| <li>Carlo Angiuli (Indiana University)</li> | ||
| <li>Kuen-Bang Hou (Favonia) (University of Minnesota)</li> | ||
| <li>Paige Randall North (Utrecht University)</li> | ||
| <li>Niels van der Weide (Radboud University Nijmegen)</li> | ||
| </ul> | ||
|
|
||
| <h2>Prerequisites</h2> | ||
| <p> | ||
| 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. | ||
| </p> | ||
|
|
||
| <!-- | ||
| </style> | ||
| </head> | ||
| <body> | ||
| <h1>School on Univalent Mathematics</h1> | ||
| <p>July 29 - August 02, 2024, Minneapolis, USA<br> | ||
| <em>(Install party on July 28, 2024)</em></p><img src="group.jpg" alt="A group photo of some participants attending the School on Univalent Mathematics" title="Group photo" width="70%"> | ||
| <h2>Overview</h2> | ||
| <p>Homotopy Type Theory and Univalent Mathematics are emerging fields of mathematics that study 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.</p> | ||
| <p>The <a href="https://github.com/UniMath/UniMath">UniMath library</a> is a large repository of computer-checked mathematics, developed from the univalent viewpoint. It is freely available for everyone, as an open-source project, <a href="https://github.com/UniMath/UniMath">from the web</a>. The School will give many young researchers an opportunity to familiarize themselves with the UniMath library and become contributors.</p> | ||
| <h2>Format</h2> | ||
| <p>Participants will receive an introduction to Univalent Foundations and to Mathematics in those foundations, by leading experts in the field. In the accompanying problem sessions, participants will formalize pieces of Univalent Mathematics in the UniMath library.</p> | ||
| <h2>Learning Materials</h2>The learning materials for the school are located <a href="https://unimath.github.io/Schools/#school-on-univalent-mathematics-minneapolis-2024">here</a>. | ||
| <h2>Lecturers</h2> | ||
| <ul> | ||
| <li>Benedikt Ahrens (Delft University of Technology)</li> | ||
| <li>Carlo Angiuli (Indiana University)</li> | ||
| <li>Kuen-Bang Hou (Favonia) (University of Minnesota)</li> | ||
| <li>Paige Randall North (Utrecht University)</li> | ||
| <li>Niels van der Weide (Radboud University Nijmegen)</li> | ||
| </ul> | ||
| <h2>Prerequisites</h2> | ||
| <p>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.</p><!-- | ||
| <h2>Registration</h2> | ||
| <p> | ||
| Registration is closed. | ||
| </p> | ||
| --> | ||
|
|
||
| <h2>Location</h2> | ||
|
|
||
| Lind Hall, University of Minnesota (Twin Cities campus), Minneapolis, MN, United States | ||
|
|
||
| <h2>Social</h2> | ||
|
|
||
| We use the <a href="https://unimath.zulipchat.com">UniMath Zulip server</a> for communication between all participants. | ||
| Feel free to ask any questions related to univalent mathematics and the installation of UniMath there. | ||
| For any communication directly related to the School on Univalent Mathematics, please use the dedicated channel <a href="https://unimath.zulipchat.com/#narrow/stream/444827-Minneapolis-2024.3A-School-on-Univalent-Mathematics">Minnesota 2024</a>. | ||
| You can use this channel to meet other participants even before the school, to organize travel together and plan activities. | ||
|
|
||
| <h2>Schedule</h2> | ||
|
|
||
| <iframe src="https://calendar.google.com/calendar/embed?height=600&wkst=1&ctz=America%2FChicago&bgcolor=%234285F4&src=YzgzMGVhY2FmYzEzMmIyOGNhMjI0N2UyODkwOTk5NzhhYmY5NmY4YmNkMDdiZGMwNGM3ZTY1ZGNhODk3NWEzYUBncm91cC5jYWxlbmRhci5nb29nbGUuY29t&color=%23C0CA33&mode=WEEK&dates=20240728%2F20240802" style="border:solid 1px #777" width="800" height="600" frameborder="0" scrolling="no"></iframe> | ||
|
|
||
|
|
||
|
|
||
| <!-- | ||
| <h3>(Tentative) Program</h3> | ||
| <ul> | ||
| <li>Monday | ||
| <ul> | ||
| <li>am: Introduction to type theory + exercises</li> | ||
| <li>pm: Fundamentals of Coq + exercises</li> | ||
| <li>Evening lecture: Kevin Buzzard</li> | ||
| </ul> | ||
| </li> | ||
| <li>Tuesday | ||
| <ul> | ||
| <li>am: Univalent foundations + exercises</li> | ||
| <li>pm: Tactics + exercises</li> | ||
| </ul> | ||
| </li> | ||
| <li>Wednesday | ||
| <ul> | ||
| <li>am: More exercises</li> | ||
| <li>Late morning lecture: Thierry Coquand</li> | ||
| <li></li> | ||
| </ul> | ||
| </li> | ||
| <li>Thursday | ||
| <ul> | ||
| <li>am: Set-level mathematics + exercises</li> | ||
| <li>pm: Category theory + exercises</li> | ||
| <li>Evening lecture: Daniel R. Grayson</li> | ||
| </ul> | ||
| </li> | ||
| <li>Friday | ||
| <ul> | ||
| <li>am: Synthetic homotopy theory</li> | ||
| <li>pm: Paradoxes</li> | ||
| </ul> | ||
| </li> | ||
| --> | ||
|
|
||
| <h2>Before the event</h2> | ||
|
|
||
| <ul> | ||
| <li>Check recommended reading | ||
| <li>Install UniMath on your laptop | ||
| </ul> | ||
|
|
||
| <h3>Recommended reading</h3> | ||
| You can prepare for the school by studying some of the material listed below. | ||
|
|
||
| <ul> | ||
| <li><a href="https://hal.inria.fr/inria-00001173v6/document">Coq in a hurry (by Yves Bertot)</a> An introduction to vanilla Coq. It does not cover the univalent point of view, but gives a gentle introduction to Coq, the underlying proof assistant of UniMath. | ||
| <li><a href="https://www.lri.fr/~paulin/LASER/course-notes.pdf">Introduction to the Coq proof-assistant for practical software verification (by Christine Paulin-Mohring)</a> Another introduction with Coq, including screenshots. It is a bit outdated, but might still be useful. | ||
| <li><a href="https://homotopytypetheory.org/book/">HoTT book</a> Comprehensive overview of univalent foundations. | ||
| <li><a href="https://faculty.math.illinois.edu/~dan/Papers/ium.pdf">An introduction to univalent foundations for mathematicians (by Dan Grayson)</a> An gentle introduction to univalent foundations. | ||
| <li><a href="https://github.com/martinescardo/HoTTEST-Summer-School/blob/main/HoTT/hott-intro.pdf">Introduction to Homotopy Type Theory (by Egbert Rijke)</a> A comprehensive textbook. | ||
| </ul> | ||
|
|
||
| <h3>Installing UniMath</h3> | ||
|
|
||
| Please install <a href="https://github.com/UniMath/UniMath">UniMath</a> on your laptop before coming to Minneapolis. | ||
| To this end, read the <a href="https://github.com/UniMath/UniMath/blob/master/INSTALL.md">installation instructions</a>. | ||
| In case of problems or questions, please ask on the <a href="https://unimath.zulipchat.com">UniMath Zulip server</a>. | ||
|
|
||
| You can also attend the UniMath install party on Sunday afternoon for help with the installation - see Section "Schedule" for more information. | ||
|
|
||
|
|
||
| <h2>Sponsors</h2> | ||
|
|
||
| <p> | ||
| We thank the National Science Foundation, | ||
| the University of Minnesota's Department of Computer Science & Engineering, | ||
| and the University of Minnesota's Institute for Mathematics and its Applications | ||
| for their generous support of this event. | ||
| </p> | ||
|
|
||
| <div style="margin-bottom:20px; text-align:center"> | ||
| <img src="nsf.png" width="150" style="margin-right:20px" | ||
| title="National Science Foundation"> | ||
| <img src="umn-ima.png" width="300" | ||
| title="University of Minnesota, Institute for Mathematics & its Applications"> | ||
| </div> | ||
| <div style="text-align:center"> | ||
| <img src="umn-cse.png" width="600" height="73" | ||
| title="University of Minnesota, Department of Computer Science & Engineering"> | ||
| </div> | ||
|
|
||
| <h2>Organisers</h2> | ||
| <ul> | ||
| <li>Benedikt Ahrens</li> | ||
| <li>Kuen-Bang Hou (Favonia)</li> | ||
| </ul> | ||
|
|
||
|
|
||
| </body> | ||
| <p>Registration is closed.</p> | ||
| --> | ||
| <h2>Location</h2>Lind Hall, University of Minnesota (Twin Cities campus), Minneapolis, MN, United States | ||
| <h2>Social</h2>We use the <a href="https://unimath.zulipchat.com">UniMath Zulip server</a> for communication between all participants. Feel free to ask any questions related to univalent mathematics and the installation of UniMath there. For any communication directly related to the School on Univalent Mathematics, please use the dedicated channel <a href="https://unimath.zulipchat.com/#narrow/stream/444827-Minneapolis-2024.3A-School-on-Univalent-Mathematics">Minnesota 2024</a>. You can use this channel to meet other participants even before the school, to organize travel together and plan activities. | ||
| <h2>Schedule</h2><iframe src="https://calendar.google.com/calendar/embed?height=600&wkst=1&ctz=America%2FChicago&bgcolor=%234285F4&src=YzgzMGVhY2FmYzEzMmIyOGNhMjI0N2UyODkwOTk5NzhhYmY5NmY4YmNkMDdiZGMwNGM3ZTY1ZGNhODk3NWEzYUBncm91cC5jYWxlbmRhci5nb29nbGUuY29t&color=%23C0CA33&mode=WEEK&dates=20240728%2F20240802" style="border:solid 1px #777" width="800" height="600" frameborder="0" scrolling="no"></iframe> | ||
| <h2>Before the event</h2> | ||
| <ul> | ||
| <li>Check recommended reading</li> | ||
| <li>Install UniMath on your laptop</li> | ||
| </ul> | ||
| <h3>Recommended reading</h3>You can prepare for the school by studying some of the material listed below. | ||
| <ul> | ||
| <li> | ||
| <a href="https://hal.inria.fr/inria-00001173v6/document">Coq in a hurry (by Yves Bertot)</a> An introduction to vanilla Coq. It does not cover the univalent point of view, but gives a gentle introduction to Coq, the underlying proof assistant of UniMath. | ||
| </li> | ||
| <li> | ||
| <a href="https://www.lri.fr/~paulin/LASER/course-notes.pdf">Introduction to the Coq proof-assistant for practical software verification (by Christine Paulin-Mohring)</a> Another introduction with Coq, including screenshots. It is a bit outdated, but might still be useful. | ||
| </li> | ||
| <li> | ||
| <a href="https://homotopytypetheory.org/book/">HoTT book</a> Comprehensive overview of univalent foundations. | ||
| </li> | ||
| <li> | ||
| <a href="https://faculty.math.illinois.edu/~dan/Papers/ium.pdf">An introduction to univalent foundations for mathematicians (by Dan Grayson)</a> An gentle introduction to univalent foundations. | ||
| </li> | ||
| <li> | ||
| <a href="https://github.com/martinescardo/HoTTEST-Summer-School/blob/main/HoTT/hott-intro.pdf">Introduction to Homotopy Type Theory (by Egbert Rijke)</a> A comprehensive textbook. | ||
| </li> | ||
| </ul> | ||
| <h3>Installing UniMath</h3>Please install <a href="https://github.com/UniMath/UniMath">UniMath</a> on your laptop before coming to Minneapolis. To this end, read the <a href="https://github.com/UniMath/UniMath/blob/master/INSTALL.md">installation instructions</a>. In case of problems or questions, please ask on the <a href="https://unimath.zulipchat.com">UniMath Zulip server</a>. You can also attend the UniMath install party on Sunday afternoon for help with the installation - see Section "Schedule" for more information. | ||
| <h2>Sponsors</h2> | ||
| <p>We thank the National Science Foundation, the University of Minnesota's Department of Computer Science & Engineering, and the University of Minnesota's Institute for Mathematics and its Applications for their generous support of this event.</p> | ||
| <div style="margin-bottom:20px; text-align:center"><img src="nsf.png" width="150" style="margin-right:20px" title="National Science Foundation" alt="Logo of National Science Foundation"> <img src="umn-ima.png" width="300" title="University of Minnesota, Institute for Mathematics & its Applications" alt="Logo of Institute for Mathematics and its Applications"></div> | ||
| <div style="text-align:center"><img src="umn-cse.png" width="600" height="73" title="University of Minnesota, Department of Computer Science & Engineering" alt="Logo of Department of Computer Science and Engineering"></div> | ||
| <h2>Organisers</h2> | ||
| <ul> | ||
| <li>Benedikt Ahrens</li> | ||
| <li>Kuen-Bang Hou (Favonia)</li> | ||
| </ul> | ||
| </body> | ||
| </html> |