Learning Material for Univalent Mathematics and the UniMath library

School on Univalent Mathematics, Cortona, 2022

Lecture 1: Type Theory (by Gianluca Amato)

• Lecture

Lecture 2: Fundamentals of Coq (by Marco Maggesi)

• Lecture

Lecture 3: Univalent foundations (by Paige Randall North)

• Lecture

Lecture 4: Tactics in UniMath (by Ralph Matthes)

• Lecture (HTML for easier reading)
• Lecture (Coq file presented in class)
• Extended Lecture (HTML)
• Extended Lecture (Coq file)
• Exercises
• Advanced exercises
• Solutions
• Advanced solutions

Lecture 5: Set-Level Mathematics (by Benedikt Ahrens)

• Lecture
• Exercises
• Solutions

Lecture 6: Univalent Category Theory (by Niels van der Weide)

• Lecture
• Code
• Exercises
• Exercises with solutions

Lecture 7: Synthetic Homotopy Theory (by Peter LeFanu Lumsdaine)

• Exercises

School and Workshop on Univalent Mathematics, Birmingham, 2019

Coq and UniMath Installation Instructions

• See Installation Instructions

Lecture 1: Spartan Type Theory by Andrej Bauer

• Lecture
• Exercises (HTML file)
• Exercises (Coq file)
• Solutions

Lecture 2: Fundamentals of Coq by Anders Mörtberg

• Lecture
• Exercises
• Solutions

Lecture 3: Univalent Foundations by Martín Hötzel Escardó

• Lecture
• Exercises

Lecture 4: Tactics by Ralph Matthes

• Lecture (short version)
• Lecture (long version)
• Exercises
• Advanced exercises
• Solutions
• Advanced solutions

Lecture 5: Set-Level Mathematics by Joj Helfer

• Lecture
• Exercises
• Solutions

Lecture 6: Category Theory in UniMath by Niels van der Weide

• Lecture
• Exercises
• Solutions

Lecture 7: Paradoxes by Thorsten Altenkirch

• Lecture
• Solutions
• Russel’s Paradox

Lecture 8: UniMath: its origins, present, and future by Benedikt Ahrens

• Lecture