Skip to content

Commit

Permalink
Update the website
Browse files Browse the repository at this point in the history
  • Loading branch information
@favonia
favonia committed May 12, 2024
1 parent 0ebf176 commit e84dac2
Showing 1 changed file with 45 additions and 45 deletions.
90 changes: 45 additions & 45 deletions minneapolis2024/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,33 +15,34 @@
</head>
<body>
<h1>School on Univalent Mathematics</h1>
<h2></h2>
<p>July 28 - August 02, 2024, Minneapolis, USA</p>

<p>July 29 - August 02, 2024, Minneapolis, USA<br>
<em>(Install party on July 28, 2024)</em>
</p>

<!--
<h2>Emergency contact information</h2>
<ul>
<li>For any emergency, call XYZ.
<li>For any emergency, call XYZ.
<li>In less serious cases, Benedikt Ahrens can be reached on <a href="tel:+447482799962">+44 7482 799962</a> or by <a href="mailto:B.Ahrens@cs.bham.ac.uk">email</a>.
</ul>
-->


<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.
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>
The <a href="https://github.com/UniMath/UniMath">UniMath library</a>
is a large repository of computer-checked
mathematics, developed from the univalent viewpoint.
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
Expand All @@ -50,56 +51,55 @@ <h2>Overview</h2>
</p>



<h2>Format</h2>

<p>
Participants will receive an introduction to
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
In the accompanying problem sessions, participants will formalize pieces of Univalent Mathematics in the
UniMath library.
</p>
<h2>Speakers</h2>

<h2>Speakers</h2>
<h3>Lecturers</h3>
TBA

<h3>Guest Speakers</h3>

TBA

<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>Application and funding</h2>

<p>
TBA
Please <a href="https://forms.gle/9PTB2V19hVuJsidz8">fill out the application form.</a> We accept applicants on a rolling basis.
</p>

<h2>Location</h2>
TBA

University of Minnesota (Twin Cities), Minneapolis, MN, United States

<h2>Social</h2>

We will have a Zulip server for communication between all participants. Details tba.
We will have a Zulip server for communication between all participants. Details TBA.


<h2>Schedule</h2>

<ul>
<li> UniMath install party planned for the afternoon of Sunday July 28, 2024. </li>
<li> School Monday July 29 - Friday August 2024.</li>
<li> School Monday July 29 - Friday August 2, 2024.</li>
</ul>




<!--
<h3>(Tentative) Program</h3>
<ul>
Expand All @@ -108,7 +108,7 @@ <h3>(Tentative) Program</h3>
<li>am: Introduction to type theory + exercises</li>
<li>pm: Fundamentals of Coq + exercises</li>
<li>Evening lecture: Kevin Buzzard</li>
</ul>
</ul>
</li>
<li>Tuesday
<ul>
Expand Down Expand Up @@ -136,47 +136,47 @@ <h3>(Tentative) Program</h3>
<li>pm: Paradoxes</li>
</ul>
</li>
-->
-->

<h2>Lecture material</h2>

See the <a href="https://unimath.github.io/Schools/">UniMath/Schools Github repository</a>.


<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://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, contact the <a href="mailto:univalent-mathematics@googlegroups.com">UniMath mailing list</a>.

You can also attend the UniMath install party on Sunday afternoon for help with the installation - see Section "Schedule" for more information.


<h2>Organisers</h2>
<ul>
<li>Benedikt Ahrens</li>
<li>Kuen-Bang Hou (Favonia)</li>
</ul>


</body>
</html>

0 comments on commit e84dac2

Please sign in to comment.