Skip to content

Commit

Permalink
add umn stub
Browse files Browse the repository at this point in the history
  • Loading branch information
@benediktahrens
benediktahrens committed Jan 15, 2024
1 parent 13bee46 commit 107bef4
Showing 1 changed file with 182 additions and 0 deletions.
182 changes: 182 additions & 0 deletions minneapolis2024/index.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,182 @@
<!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">
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>
<h2></h2>
<p>July 28 - August 02, 2024, Minneapolis, USA</p>

<!--
<h2>Emergency contact information</h2>
<ul>
<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:[email protected]">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.
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>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
</p>

<h2>Location</h2>

TBA

<h2>Social</h2>

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>
</ul>




<!--
<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>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://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 Cortona.
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:[email protected]">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 107bef4

Please sign in to comment.