# Learning Material for Univalent Mathematics and the UniMath library ## [School on Univalent Mathematics, Minneapolis, 2024](https://unimath.github.io/minneapolis2024/) ### Lecture 1: Type Theory (by [Paige Randall North](https://paigenorth.github.io/)) - [Lecture](2024-07-Minneapolis/1_Type-Theory/minneapolis_lecture_1.pdf) ### Lecture 2: Type Theory (by [Niels van der Weide](https://nmvdw.github.io)) - [Lecture](2024-07-Minneapolis/2_Coq/Fundamentals_Coq.pdf) - [Coq file](2024-07-Minneapolis/2_Coq/fundamentals_lecture.v) - [Exercises](2024-07-Minneapolis/2_Coq/coq_exercises.v) - [Solutions](2024-07-Minneapolis/2_Coq/coq_solutions.v) ### Lecture 3: Univalent Foundations (by [Paige Randall North](https://paigenorth.github.io/)) - [Lecture](2024-07-Minneapolis/3_Univalent-Foundations/minneapolis_lecture_3.pdf) ### Lecture 4: Tactics in Coq (by [Benedikt Ahrens](https://benediktahrens.gitlab.io)) - [Lecture](2024-07-Minneapolis/4_Tactics/tactics_lecture.v) - [Lecture (extended)](2024-07-Minneapolis/4_Tactics/tactics_lecture_extended.v) - [Exercises](2024-07-Minneapolis/4_Tactics/exercises_tactics.v) - [Solutions](2024-07-Minneapolis/4_Tactics/exercises_tactics_with_solutions.v) ### Lecture 5: Set-Level Mathematics (by [Carlo Angiuli](https://carloangiuli.com/)) - [Lecture](2024-07-Minneapolis/5_Set-level-mathematics/lecture5.pdf) - [Exercises](2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v) - [Solutions](2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v) ### Lecture 6: Univalent Category Theory (by [Niels van der Weide](https://nmvdw.github.io)) - [Lecture](2024-07-Minneapolis/6_Category-theory-in-UF/lecture.pdf) - [Code](2024-07-Minneapolis/6_Category-theory-in-UF/category_theory.v) - [Exercises](2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_exercises.v) - [Exercises with solutions](2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_solutions.v) ### Lecture 7: Synthetic Homotopy Theory (by [Favonia](https://favonia.org/)) - [Exercises](2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_exercises.v) - [Solutions](2024-07-Minneapolis/7_Synthetic-Homotopy-Theory/circle_solutions.v) ## [School on Univalent Mathematics, Cortona, 2022](https://unimath.github.io/cortona2022/) ### Lecture 1: Type Theory (by [Gianluca Amato](https://www.sci.unich.it/~amato/)) - [Lecture](2022-07-Cortona/1_Type-Theory/Lecture_Type-Theory.pdf) ### Lecture 2: Fundamentals of Coq (by [Marco Maggesi](https://sites.google.com/unifi.it/maggesi/)) - [Lecture](https://github.com/UniMath/Schools/tree/master/2022-07-Cortona/2_Fundamentals-Coq) ### Lecture 3: Univalent foundations (by [Paige Randall North](https://paigenorth.github.io/)) - [Lecture](https://github.com/UniMath/Schools/tree/master/2022-07-Cortona/3_Univalent-foundations.pdf) ### Lecture 4: Tactics in UniMath (by [Ralph Matthes](https://www.irit.fr/~/Ralph.Matthes/)) - [Lecture](2022-07-Cortona/4_Tactics-UniMath/lecture_tactics.html) (HTML for easier reading) - [Lecture](2022-07-Cortona/4_Tactics-UniMath/lecture_tactics.v) (Coq file presented in class) - [Extended Lecture](2022-07-Cortona/4_Tactics-UniMath/lecture_tactics_long_version.html) (HTML) - [Extended Lecture](2022-07-Cortona/4_Tactics-UniMath/lecture_tactics_long_version.v) (Coq file) - [Exercises](2022-07-Cortona/4_Tactics-UniMath/exercises_tactics.v) - [Advanced exercises](2022-07-Cortona/4_Tactics-UniMath/weq_exercises.v) - [Solutions](2022-07-Cortona/4_Tactics-UniMath/exercises_tactics_with_solutions.v) - [Advanced solutions](2022-07-Cortona/4_Tactics-UniMath/weq_exercises_with_solutions.v) ### Lecture 5: Set-Level Mathematics (by [Benedikt Ahrens](https://benediktahrens.gitlab.io)) - [Lecture](2022-07-Cortona/5_Set-level-mathematics/5_set_level_mathematics_lecture.pdf) - [Exercises](2022-07-Cortona/5_Set-level-mathematics/set_level_mathematics_exercises.v) - [Solutions](2022-07-Cortona/5_Set-level-mathematics/set_level_mathematics_solutions.v) ### Lecture 6: Univalent Category Theory (by [Niels van der Weide](https://nmvdw.github.io)) - [Lecture](2022-07-Cortona/6_Category_Theory/lecture.pdf) - [Code](2022-07-Cortona/6_Category_Theory/category_theory.v) - [Exercises](2022-07-Cortona/6_Category_Theory/category_theory_exercises.v) - [Exercises with solutions](2022-07-Cortona/6_Category_Theory/category_theory_solutions.v) ### Lecture 7: Synthetic Homotopy Theory (by [Peter LeFanu Lumsdaine](http://peterlefanulumsdaine.com/)) - [Exercises](2022-07-Cortona/7_Synthetic-Homotopy-Theory/Synthetic_Homotopy_Theory.v) ## [School and Workshop on Univalent Mathematics, Birmingham, 2019](https://unimath.github.io/bham2019/) ### Coq and UniMath Installation Instructions - See [Installation Instructions](installation.md) ### Lecture 1: *Spartan Type Theory* by [Andrej Bauer](http://www.andrej.com) - [Lecture](2019-04-Birmingham/Part1_Spartan_Type_Theory/Spartan-Type-Theory.pdf) - [Exercises](2019-04-Birmingham/Part1_Spartan_Type_Theory/Spartan_exercises.html) (HTML file) - [Exercises](2019-04-Birmingham/Part1_Spartan_Type_Theory/Spartan_exercises.v) (Coq file) - [Solutions](2019-04-Birmingham/Part1_Spartan_Type_Theory/Spartan_solutions.v) ### Lecture 2: *Fundamentals of Coq* by [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) - [Lecture](2019-04-Birmingham/Part2_Fundamentals_Coq/fundamentals_lecture.v) - [Exercises](2019-04-Birmingham/Part2_Fundamentals_Coq/coq_exercises.v) - [Solutions](2019-04-Birmingham/Part2_Fundamentals_Coq/coq_solutions.v) ### Lecture 3: *Univalent Foundations* by [Martín Hötzel Escardó](https://www.cs.bham.ac.uk/~mhe/) - [Lecture](2019-04-Birmingham/Part3_Univalent_Foundations/uf.pdf) - [Exercises](2019-04-Birmingham/Part3_Univalent_Foundations/truncation_exercices.v) ### Lecture 4: *Tactics* by [Ralph Matthes](https://www.irit.fr/~/Ralph.Matthes/) - [Lecture](2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics.v) (short version) - [Lecture](2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics_long_version.v) (long version) - [Exercises](2019-04-Birmingham/Part4_Tactics_UniMath/exercises_tactics.v) - [Advanced exercises](2019-04-Birmingham/Part4_Tactics_UniMath/weq_exercises.v) - [Solutions](2019-04-Birmingham/Part4_Tactics_UniMath/exercises_tactics_with_solutions.v) - [Advanced solutions](2019-04-Birmingham/Part4_Tactics_UniMath/weq_exercises_with_solutions.v) ### Lecture 5: *Set-Level Mathematics* by [Joj Helfer](http://web.stanford.edu/~joj/) - [Lecture](2019-04-Birmingham/Part5_Set_Level_Mathematics/5_set_level_mathematics_lecture.pdf) - [Exercises](2019-04-Birmingham/Part5_Set_Level_Mathematics/set_level_mathematics_exercises.v) - [Solutions](2019-04-Birmingham/Part5_Set_Level_Mathematics/set_level_mathematics_solutions.v) ### Lecture 6: *Category Theory in UniMath* by [Niels van der Weide](https://cs.ru.nl/~nweide/) - [Lecture](2019-04-Birmingham/Part6_Category_Theory/lecture.pdf) - [Exercises](2019-04-Birmingham/Part6_Category_Theory/category_theory_exercises.v) - [Solutions](2019-04-Birmingham/Part6_Category_Theory/category_theory_solutions.v) ### Lecture 7: *Paradoxes* by [Thorsten Altenkirch](http://www.cs.nott.ac.uk/~psztxa/) - [Lecture](2019-04-Birmingham/Part7_Paradoxes/GirardsParadox.v) - [Solutions](2019-04-Birmingham/Part7_Paradoxes/GirardsParadox_solutions.v) - [Russel's Paradox](2019-04-Birmingham/Part7_Paradoxes/RussellsParadox.v) ### Lecture 8: *UniMath: its origins, present, and future* by [Benedikt Ahrens](https://benediktahrens.net/) - [Lecture](2019-04-Birmingham/Part8_UniMath_future/UniMath_past_present_future.pdf)