Learning Material for Univalent Mathematics and the UniMath library

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