Learning Material for Univalent Mathematics and the UniMath library

August 4, 2024 · View on GitHub

School on Univalent Mathematics, Minneapolis, 2024

Lecture 1: Type Theory (by Paige Randall North)

Lecture 2: Type Theory (by Niels van der Weide)

Lecture 3: Univalent Foundations (by Paige Randall North)

Lecture 4: Tactics in Coq (by Benedikt Ahrens)

Lecture 5: Set-Level Mathematics (by Carlo Angiuli)

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

Lecture 7: Synthetic Homotopy Theory (by Favonia)

School on Univalent Mathematics, Cortona, 2022

Lecture 1: Type Theory (by Gianluca Amato)

Lecture 2: Fundamentals of Coq (by Marco Maggesi)

Lecture 3: Univalent foundations (by Paige Randall North)

Lecture 4: Tactics in UniMath (by Ralph Matthes)

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

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

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

School and Workshop on Univalent Mathematics, Birmingham, 2019

Coq and UniMath Installation Instructions

Lecture 1: Spartan Type Theory by Andrej Bauer

Lecture 2: Fundamentals of Coq by Anders Mörtberg

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

Lecture 4: Tactics by Ralph Matthes

Lecture 5: Set-Level Mathematics by Joj Helfer

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

Lecture 7: Paradoxes by Thorsten Altenkirch

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